You're doing Natural Deduction wrong!

What I don't like about the bottom up reasoning approach is that it sometimes leads to dead ends which require more creativity to avoid. for example

P v R, P ~> Q, R ~> S |- Q v S

One might think of trying to prove Q from the premises and then use vI to get Q v S, or they might try to prove S and then use vI similarly.

But that leads to a dead end since it's impossible.

Instead one must use vE by first assuming P and proving Q v S and also assuming R and proving Q v S

I came across this problem while trying to find an algorithm automated way to create a natural deduction proof and it simply seemed tedious to search through all possible rules that could be applied at a given time. Luckily I found out about the Sequent Calculus which provides a more straight-forward approach.

Great video as always... btw do you think our universe is metaphysically Necessary?

Just tried this on [](P->Q) |- []P->[]Q and it worked beautifully. I could have spent hours banging my head against a wall after taking [] instead of []P as my first assumption.

lamso this is common sense in theorem provers: you just go "intros intros intros"

I would usually just prove it by using truth tables that the argument is always true under every evaluation. But since you put in the argument four different propositions this would mean that I have to make 16 different evaluations.

I am not really verse in philosophy or all that good stuff. And maybe that's why I am not really good at dealing with formal logic. But the way the bottom up strategy works makes me feel uncomfortable. If I were to do the prove myself, I would have done it this way.
Argument: q → (p→r) |- (s→p)→(q→(s→r))

my "proof" LOL:
1. q → (p→r) Assuming the premise
2. (s→p) ∧ ~(q→(s→r)) negating the conclusion
3. (s→p) by simplification from 2
4. ~(q→(s→r)) by simplification from 2
5. (q ∧ ~ (s→r)) by distribution of the negative sign from 4
6. q by simplification from 5
7. ~ (s→r) by simplification from 5
8. (s ∧ ~r) by distribution of the negative sign from 7
9. s by simplification from 8
10. ~r by simplification from 8
11. (p→r) by modus ponendo ponens from 1,6
12. p by modus ponendo ponens from 3, 9
13. r by modus ponendo ponens from 11,12
14. ~r ∧ r by conjunction from 10, 13
15. ⊥ contradiction from 14
16. ~[(s→p) ∧ ~(q→(s→r))] proof by contradiction from 2-15
17. ~(s→p) v (q→(s→r)) by distribution of the negative sign from 16
18. (s→p)→(q→(s→r)) by equivalence of or from 17

I am sure that the proof is wrong in the way that I set it up and even the way I use the rules of deduction. But I feel more comfortable knowing that the premise and the negation of the conclusion leads to a contraction and so I can accept the conclusion given the premise being true. I can more or less see someone objecting on the grounds that just because two propositions are inconsistent with each other, does not mean that one is the proper premise for the other.

Attic philosophy is an awesome channel. Thank you so much for your videos. Cheers mate.

Ok, where were you when I had a logic course last semester? Lmao, Thanks for the content anyways. Hope to see more of you, Mark!

would u consider making a video on gentzen style proof for PL?

I feel like for proofs involving conditionals, although the bottom-up approach does work, it's just as easy to repeat the mantra 'assume the antecedent with a view to deriving the consequent' to yourself. Sure, it might be a bit tricky when you've multiple nested conditionals like in this case, but I think it's still simpler than having to switch from the usual top-down approach

Wow thank you!!! Could u please provide the corresponding citations for each line in the comments?

This is also how proof assistance like Coq work. Sometimes to an annoying extent.

Thanx so much! This video really helped me to understand, after being frustrated not knowing what and how to do the next step - exactly the way you described 👏

Thx a lot🌱🌱🌹🌸🌱🌱🌱🍄🌸

Thank you, thank you, thank you so much for this video. I knew this already, but somehow I hadn't really grasped it. I usually start my proofs the way the video started - by trying to prove the premises.

Hi, professor. I am curious as a math student why exactly is natrual derivation still relavent in philosophy in the context of classical logic. In my mathmatical logic class we were told to simply check the truth value of the sentence(propositional consequence) and it's a lot faster in general. Hence, I am curious in my logic class in philosophy why is this simpler way not tought. Help you can answer me. Thanks !

This really helps. Thanks💯

I wish my techer explained like that before my first midterm.

thank you!

Sir could you please give an overview, how can we use proposition logic and natural deduction argument in real life ... In very Practical way

Hello, professor, you just earned a new subscriber, kudos to all the videos of yours that I've thus far seen, quality content, I wish your channel be noticed by more learners!

Brilliant!

Took me a while to figure out what he was saying. I’ve never heard ‘antecedent’ pronounced an-TESS-suh-dent. I’ve always thought it was an-tub-SEE-dent. ChatGPT agrees with me accent on the third syllable

But why can we assume S -> P, and given that we have assumed that what have we proven?