Love your tutorials. Really great and useful. For Proof #14, what do you think of the following proof? 1. ~(A ∧ B) : Premise 2. ~(~A ∨ ~B) : Assumption of PBC 3. ~(~(A∧B)) : 2, DM for ∨ (proven before) 4. A ∧ B : ~~ Elim. 5. ⊥ : 1, 4 6. ※ : 5 7. ~A ∨ ~B : ~2
Proof 15 - 11. DisjunktionElim: should include Line 2 aswell, right? Lines 4 and 7 use Line 2 so its mandatory to include it or not? Really appreciate the videos. Greetings from Germany.
Yeah, you're understanding it correctly. In other natural deduction formats, one avoids the indentations and simply lists for every line the previous assumptions that that line depends on. But in the Fitch system, the indentations do the work, so you don't have to explicitly mention that line 11 depends on line 2 because line 11 is orthographically inside the subproof with line 2 as an assumption. It's what I like most about the Fitch-style system, the bookkeeping about assumptions is handled visually.
Thanks This helped me a lot. I have an easier solution to proof16, tested on the Fitch tool and it works 1. PvQ 2. ~P 3. P 4. ⊥ ⊥ intro : 2,3 5. Q ⊥ elim : 4 6. Q 7. Q reit : 6 8. Q v elim : 1, 3-5, 6-7
Yeah, you must be working in a variant system with an extra rule "⊥ elim" that lets you conclude anything directly from a ⊥. We don't have that rule in my system. I essentially prove that rule in Proof #12 in this same video.
Thank you so much for your videos! They are really helpful! I only had one doubt, in Proof 17, how did yiu went from step 3 to step 4? You have a disjunc in line 3, and then you have only conjuncts in line 4. Many thanks in advance!
48:54 Hi, if you chose Q for the assumption, surely the proof would have failed? I understand why you chose ~Q, but it just seems counter-intuitive using variables independent of Q (P, ~P) to show a contradiction about Q?
It is somewhat counterintuitive, at least at first. This is a property of “classical logic”. From contradictory propositions, we can prove anything. (P ⋀ ~P) ⊨ Q is valid because whenever the premise is true (never), the conclusion is true.
@@dodecahedra I think I see now, thanks! Since the premise can never be true, it doesn't matter what the conclusion is since you can never reach that far anyway.
Sorry for being a nuisance but why do we say that its naive to go from NotP to NotP or NotR (around 31:15) and then do exactly that around minute 40:00? Thanks for the first reply btw, very cool.
It is logically valid to go from X to X∨Y. It is a strange kind of argument, but whenever X is true, X∨Y is true, so that's the definition of validity. In our system, we call this "disjunctive introduction" -- if you have P already, you can conclude P∨X for any X. It's built into the system. It's a rule that can be justified by making a truth table and applying the definition of validity. Hoping to prove ~P "directly" from ~(P∧R) and then finish by concluding ~P ∨ ~R is naïve because ~P simply doesn't follow logically from ~(P∧R) -- that's an invalid argument. After assuming line 1 AND line 2 (which are contradictory), it should be possible to prove anything since contradictory premises can be used to prove anything. P does follow from line 1 and line 2 together, as we show in the proof.
Why do you require that a contradiction is written on a line and that students derive falsum? Isn’t it just easier to write falsum whenever you have a formula and it’s negation on two lines in open sub-proofs not of the same depth?
@@patrickwithee7625 No deep and principled reason. It's just the syntax of the Fitch system I inherited from the Barwise and Etchemendy Tarski's World. Many variants are possible, of course.
For proof #14 is it possible to introduce a tautology like (P v ~P) as a conclusion and then conduct a proof by cases to show that for both P and ~P we get our desired outcome (~R v ~P)?
One could do that, but the strength of the system is in its minimalism. There are exactly two rules for every connective, one for introduction and one for elimination. So there is no need to "add tautologies" because every tautology like this can be proved from the rules. There is a proof of P v ~P that appears at the end of this video. Proof #17
@0:39 Proof #11
**** @6:17 Proof #12 **** @15:41 Proof #13 **** @20:49 Proof #15 **** @28:12 Proof #14 **** @46:30 Proof #16 **** @50:56 Proof #17
You are a legend ; after a day of studying the rules; they finally started to click in my head after watching you explain everything once again !
Great video! This cleared up some ideas that other videos gloss over like the idea that we really have ~(~a) and the bottom Symbol for contradiction
Love your videos!! keep up the amazing work!!
Love your tutorials. Really great and useful. For Proof #14, what do you think of the following proof?
1. ~(A ∧ B) : Premise
2. ~(~A ∨ ~B) : Assumption of PBC
3. ~(~(A∧B)) : 2, DM for ∨ (proven before)
4. A ∧ B : ~~ Elim.
5. ⊥ : 1, 4
6. ※ : 5
7. ~A ∨ ~B : ~2
Proof 15 - 11. DisjunktionElim: should include Line 2 aswell, right? Lines 4 and 7 use Line 2 so its mandatory to include it or not?
Really appreciate the videos. Greetings from Germany.
Yeah, you're understanding it correctly. In other natural deduction formats, one avoids the indentations and simply lists for every line the previous assumptions that that line depends on. But in the Fitch system, the indentations do the work, so you don't have to explicitly mention that line 11 depends on line 2 because line 11 is orthographically inside the subproof with line 2 as an assumption. It's what I like most about the Fitch-style system, the bookkeeping about assumptions is handled visually.
Great video, keep up the good work!
Thank you very much for the awesome explanations. Is there a possibility to get something like a pdf document with the exercises and your solutions? 😊
Yes. Email me @mrrose31@gmail.com
Could I also get an pdf file with exercises and solutions? It would help me tremendously in studying for my logic exam :)@@dodecahedra
Thanks
This helped me a lot.
I have an easier solution to proof16, tested on the Fitch tool and it works
1. PvQ
2. ~P
3. P
4. ⊥ ⊥ intro : 2,3
5. Q ⊥ elim : 4
6. Q
7. Q reit : 6
8. Q v elim : 1, 3-5, 6-7
Yeah, you must be working in a variant system with an extra rule "⊥ elim" that lets you conclude anything directly from a ⊥. We don't have that rule in my system. I essentially prove that rule in Proof #12 in this same video.
I have seen in other examples similar to yours in #11, where they would usually skip line 3 & instead just insert line 4. Is that technically correct?
Yeah, that's a very common minor variant. Same thing basically, just slight more efficient that way, I guess.
Thank you so much for your videos! They are really helpful! I only had one doubt, in Proof 17, how did yiu went from step 3 to step 4? You have a disjunc in line 3, and then you have only conjuncts in line 4. Many thanks in advance!
Oh yeah. Oops. That's just a little typo there. Sorry. Should be 4. (P⋁~P) ⋀ ~(P⋁~P) of course.
@@dodecahedra thank you for taking the time to reply! really appreciate it
48:54
Hi, if you chose Q for the assumption, surely the proof would have failed? I understand why you chose ~Q, but it just seems counter-intuitive using variables independent of Q (P, ~P) to show a contradiction about Q?
It is somewhat counterintuitive, at least at first. This is a property of “classical logic”. From contradictory propositions, we can prove anything.
(P ⋀ ~P) ⊨ Q is valid because whenever the premise is true (never), the conclusion is true.
@@dodecahedra I think I see now, thanks! Since the premise can never be true, it doesn't matter what the conclusion is since you can never reach that far anyway.
very helpful
Sorry for being a nuisance but why do we say that its naive to go from NotP to NotP or NotR (around 31:15) and then do exactly that around minute 40:00? Thanks for the first reply btw, very cool.
It is logically valid to go from X to X∨Y. It is a strange kind of argument, but whenever X is true, X∨Y is true, so that's the definition of validity. In our system, we call this "disjunctive introduction" -- if you have P already, you can conclude P∨X for any X. It's built into the system. It's a rule that can be justified by making a truth table and applying the definition of validity.
Hoping to prove ~P "directly" from ~(P∧R) and then finish by concluding ~P ∨ ~R is naïve because ~P simply doesn't follow logically from ~(P∧R) -- that's an invalid argument.
After assuming line 1 AND line 2 (which are contradictory), it should be possible to prove anything since contradictory premises can be used to prove anything. P does follow from line 1 and line 2 together, as we show in the proof.
Also for #16, how about rewriting the disjunction as a material implication (P ∨ Q ≡ ~P → Q) and then using modus ponens?
can't we use proof by cases?
Why do you require that a contradiction is written on a line and that students derive falsum? Isn’t it just easier to write falsum whenever you have a formula and it’s negation on two lines in open sub-proofs not of the same depth?
@@patrickwithee7625 No deep and principled reason. It's just the syntax of the Fitch system I inherited from the Barwise and Etchemendy Tarski's World. Many variants are possible, of course.
For proof #14 is it possible to introduce a tautology like (P v ~P) as a conclusion and then conduct a proof by cases to show that for both P and ~P we get our desired outcome (~R v ~P)?
One could do that, but the strength of the system is in its minimalism. There are exactly two rules for every connective, one for introduction and one for elimination. So there is no need to "add tautologies" because every tautology like this can be proved from the rules. There is a proof of P v ~P that appears at the end of this video. Proof #17
@@dodecahedra Thanks for the clarification!
Does the contradiction sign mean the same as the absurdity?
In example 14 why don’t we only use the previous proof to prove it
We're just... not doing that. These are exercises, so we don't use any previous results.
I love you
a Feup me fez estar aqui pela 2 vez
Thx
Help me
que rei
és o rei o filho
sim
O MATRIX VAI TIRAR 20 AMANHA (KAPPA)
@@efseesfesfsefse2124 vocês tão em q curso?
@@lovedzhd JCL TURTLE