Page: ‹ previous 1 2
Member since Oct 2018
4 posts

20190207, 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

20190207, 20:07 #17
That looks awesome 
Member since Oct 2016
806 posts

20190208, 10:29 #18
In reply to post ID 159457
One more comment on my handscribbled solution for 5.2:
Note that since I instantiated X with b in the left branch of the tableauproof, 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

20190208, 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. 
Page: ‹ previous 1 2
Datenschutz 
Kontakt
Powered by the Unclassified NewsBoard software, 20150713dev,
© 20032011 by Yves Goergen