Not logged in. · Lost password · Register

Page:  previous  1  2
 Member since Oct 2018 4 posts 2019-02-07, 16:58   #16   In reply to post ID 159457 +2 tyr, lu60ruhy For natural deduction I found these examples very helpful: http://logicmanual.philosophy.ox.ac.uk/carr/NDpack.pdf
 Member since Apr 2018 15 posts 2019-02-07, 20:07   #17   Quote by F.W.:For natural deduction I found these examples very helpful: http://logicmanual.philosophy.ox.ac.uk/carr/NDpack.pdf That looks awesome
 Member since Oct 2016 806 posts 2019-02-08, 10:29   #18   In reply to post ID 159457 One more comment on my hand-scribbled solution for 5.2: Note that since I instantiated X with b in the left branch of the tableau-proof, I *have to* instantiate X in the right branch by the same value b (it's not really made clear in my proof, sorry about that). That's because a substitution applies to all formulas resulting from an elimination of a quantifier, which in this case is right in the first step of the proof, whereas the quantifier binding Y is eliminated separately in each branch (hence I may substitute Y by different values in both branches). If I wanted to instantiate X by a *different* value in the right branch, I would have to reliminate the \exists X *again* in the right branch, forcing me to redo all of the steps above the branching step, which wouldn't help me in this particular proof.
 Member since Nov 2018 53 posts 2019-02-08, 12:05   #19   In reply to post ID 159437 Have you seen the examples here (PL): https://leanprover.github.io/logic_and_proof/natural_deduc… and here (FOL): https://leanprover.github.io/logic_and_proof/natural_deduc… ? The calculus is slightly different (No TND but a few more rules) but the notation is very similar.
Close Smaller – Larger + Reply to this post:
Verification code: Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys:
Special characters:
Page:  previous  1  2
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen