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 👏

@AtticPhilosophy

Жыл бұрын

Great, glad it helped!

This really helps. Thanks💯

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.

@AtticPhilosophy

8 ай бұрын

Glad it was helpful! Good luck.

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!

@AtticPhilosophy

Жыл бұрын

haha, sorry it came too late! there's plenty more logic tutorials on this channel if you're continuing you logic studies.

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

@AtticPhilosophy

Жыл бұрын

That’s the right approach to proving a conditional, for sure. But first, you have to know that a conditional is your target, so you’re looking at the bottom, not the top.

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

thank you!

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.

@AtticPhilosophy

Жыл бұрын

Right, it won’t work for every example, but it’s still a good approach when you’re starting out. As a general rule, you rarely prove AvB directly through proving one of the disjuncts. Sequent calculus or proof trees definitely better for automated strategies!

@STXHC

Жыл бұрын

I think this solves it: "apply every possible rule on the premises, else work with the conclusion", but if you ignore this and got disjunction to prove, then trying to prove a disjunct could set us astray, as in the proof of commutativity of disjunction.

@edwardgonzalez6331

Жыл бұрын

I am sure that I am wrong. But I still feel that indirect proof are the best way to go. In your argument I feel like doing this: Argument: (P v R), (P → Q), (R → S) |- Q v S 1. P v R ASS 2. P → Q ASS 3. R → S ASS 4. ~(Q v S ) Negating Conclusion 5. ~Q ∧ ~S distribution of negative sign from 4 6. ~Q simplification from 5 7. ~S simplification from 5 8. ~P Modus tollendo tollens from 2, 6 9. ~R Modus tollendo tollens from 3, 7 10. P Disjunctive syllogism from 1, 9 11. ~P ∧ P conjunction from 8,10 12. ⊥ contradiction from 11 13. ~~(Q v S) proof by contradiction from 4-12 14. Q v S double negation from 13

@AtticPhilosophy

Жыл бұрын

@@STXHC you really don’t want to try every rule on the premises, because you can always apply v-intro, infinitely many times, and never get anywhere! v-elim is different, in that it tells you what assumptions to make based on the disjunction you’re working with.

@STXHC

Жыл бұрын

@@AtticPhilosophy my bad, every possible elimination rule.

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

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

@AtticPhilosophy

Жыл бұрын

Thanks! I’ve got a video on exactly this question coming next week, stick around for it!

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

@AtticPhilosophy

Жыл бұрын

Absolutely. That's why the sub-formula property is important in proof search - it tells you where you need to go

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

@AtticPhilosophy

Жыл бұрын

Yes! I've got a video on Gentzen sequent calculus planned for the new year.

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

@AtticPhilosophy

Жыл бұрын

The only rules used are -> intro and elim (aka modus ponens). See if you can work out which order they go in! If you get stuck, let me know & I’ll add the rules here.

@chachiiiii99

Жыл бұрын

Sounds good! 1-4 seem to be assumptions 5 -> E 1,3 6 -> E 2,4 7 -> E 5,6 8 -> I 3-7 9 -> I 1-8 (Another question. Does this strategy only apply if the conclusion has a conditional as a connective factor?)

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.

@AtticPhilosophy

Жыл бұрын

Exactly - in this case, a natural deduction proof is simpler. And often students *have* to prove it a certain way to pass the test!

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

@AtticPhilosophy

2 ай бұрын

To use logic in real life: take any practical argument you're interested in, translate it into logical notation, then test the argument using natural deduction. That tells you (i) whether the argument is valid and (ii) if not, what's gone wrong, and what premises would need to be added to make it valid.

@nitishgautam5728

2 ай бұрын

@@AtticPhilosophy You are right ... I did some thought experiments and argument... I felt like I give very less premeses for the big conclusion I want to prove ... I need to work on that . Thank you for replying 🙏

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.

@AtticPhilosophy

Жыл бұрын

Thanks! OK, so 'negating the conclusion' is basically how tree proofs work - not natural deduction. (That approach is good for classical logic, terrible for intuitionistic, where a contradiction from negated conclusion doesn't imply the conclusion!) Your approach also assumes ~(A->B) is equivalent to A&~B, which again won't always hold in non-classical logics. Natural deduction systems have an intro & elimination rule for each connective, and this gives them some nice properties. A nice thing about your proof, however, is you've got q, s, ~r etc, so effectively can work out what any valuation must look like - that's what a tree proof does. In case you're interested, I've got a comparison of proof trees vs natural deduction here: kzread.info/dash/bejne/aYegpq-Besi7nNo.html

@edwardgonzalez6331

Жыл бұрын

@@AtticPhilosophy Okay. I think I get it. The only thing that I am not sure is the equivalent thing you mention. ~ (A→B) equivalent to (A ∧ ~B). I just didn't write the steps to get from one to the other. I got (A ∧ ~B) from applying De Morgan's laws and the implication equivalence to the disjunction to ~ (A→B). I did it this way: 1. ~ (A→B) Starting statement 2. ~(~A v B) implication to disjunction equivalence from 1 3. ~~A ∧ ~B De Morgan's law from 2 4. A ∧ ~B double negation from 3 De Morgan's laws do apply to intuitionistic logic and Fuzzy logic. But I completely get your point. #2 does not apply in non classical logics. In other words "(A→B) is equivalent to (~A v B)" does not hold in non classical logics. Again, thank you so much for responding to my message. And thank you so much for your channel. I am learning so much from you.

@AtticPhilosophy

Жыл бұрын

@@edwardgonzalez6331 Great, that's good to hear!

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 !

@AtticPhilosophy

8 ай бұрын

There's several reasons. One is that it isn't always more efficient to check through truth-values (I assume you mean by using truth-tables). Consider the argument p1->(p2->(p3->(p4->(p5->p6)))), p1, so p6. The truth-table is huge, with 64 lines. The natural deduction proof (essentially, modus ponens x 5) has 7 lines. Another reason is to have proof systems which can generalise (e.g. for quantifiers, for modal logics). Truth-tables don't. Another (more philosophical) reason is to have proof systems which are separate from the semantics (ie, don't mention truth). You need some separation for soundness/completeness proofs to be meaningful. Some logicians think that meaning comes through proof rules, not through semantics.

@isssxx7761

8 ай бұрын

@@AtticPhilosophy Thanks for your response. So i guess the moral is to lay down a solid ground for students if they want to go beyond classical propositional logic? I find that most of the time if not all in writing an essay, I dont use natrual derivation as complex as it is taught. Most of time it would just be moduls ponen and repeat. Please correct me if I am wrong. And just to add to the conversation for a bit, I use more effective ways, if you have that conditional you just assume one by one that every premise is true because if the premise is false you get the whole sentence to be true automatically. It ends up with p6 can be assign as F so the whole sentence is not tautology therefore not true.( To simple the notation a bit, rewrite p1->(p2->(p3->(p4->(p5->p6)))) as p1 -> B. If p1 is false, the whole sentence is true regradless of B. And for B=p2->(p3->(p4->(p5->p6)))= p2->C we do the same to exhaust the sentence.) And similar way exists for other forms so lengthy truth table is really not need here.

@AtticPhilosophy

8 ай бұрын

@@isssxx7761Not just that. In learning any logic, it's good to learn a proof system, and also how to reason about it (eg soundness & completeness, which you can't meaningfully do with truth-tables). Natural deduction is much easier to use than axiomatic reasoning, simpler than sequent calculus. Proof trees are another good system. A nice thing about learning natural deduction is that it teaches good reasoning skills: eg to establish a conditional conclusion, you assume the antecedent & reason to the consequent. Rarely would you use a proof system of any kind in an essay (that isn't a logic test).

@isssxx7761

8 ай бұрын

@AtticPhilosophy Thank you professor!

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

@AtticPhilosophy

Жыл бұрын

Except for when you don’t, e.g. prove Av~A

@freddyfozzyfilms2688

Жыл бұрын

@@AtticPhilosophy rip

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.

@edwardgonzalez6331

Жыл бұрын

Sorry to ask. Is that modal logic?

@frankavocado

Жыл бұрын

@@edwardgonzalez6331 I hope so. You need a couple of simple introduction and elimination rules for the box operator in addition to the standard predicate logic rules, but otherwise the principle on my example is the same. I happened to be working through 'Modal Logic for Philosophers' by James W Garson when this natural deduction strategy video dropped. I think the book is a great intro to the subject but, as ever, the @AtticPhilosophy approach of short, clear presentations brilliantly supplements all my attempts to get a handle on the topic. It's a great resource for those moments when a textbook just leaves me sitting in blank puzzlement. There's a series of @AtticPhilosophy vids on modal logic which are a solid foundation to build on if you're interested.

@edwardgonzalez6331

Жыл бұрын

@@frankavocado Thank you so much for your message. I have that book too. And I really like it. I also really like the atticPhilosophy videos on modal logic. Cheers mate!

@AtticPhilosophy

Жыл бұрын

Great! That’s a nice example.