Logic - Fitch-style Natural Deduction Proofs #11-17

Logic - Rose - MBHS - Blair - Natural deduction proofs in propositional logic via a Fitch-style system. In this video, I do proofs #11-17 of the packet, including proof by contradiction (negation intro), the principle of explosion, two of the four DeMorgan's laws, and the law of the excluded middle. Extensive discussion of how to approach these proofs. - 9/19/2020

[dodecahedra]

@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

[mihaisimtion]

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 !

[dddd-cizm]

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

[andredejager]

"The destiny of any negation is to be used in a contradiction" :)

[csperi-peri]

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?

[pjt]

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.

[viktormos]

Love your videos!! keep up the amazing work!!

[EhsanAmini]

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

[nark]

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?

[dewaldsmit]

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

[EhsanAmini]

Also for #16, how about rewriting the disjunction as a material implication (P ∨ Q ≡ ~P → Q) and then using modus ponens?

[joanamarques]

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!

[pjt]

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.

[MTRK]

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)?

[Kojaten]

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? 😊

[patrickwithee]

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?

[thekalinka]

Does the contradiction sign mean the same as the absurdity?

[oxygen]

In example 14 why don’t we only use the previous proof to prove it