Not logged in. · Lost password · Register

Page:  previous  1  2 
F.W.
Member since Oct 2018
4 posts
In reply to post ID 159457
+2 lu60ruhy, tyr
For natural deduction I found these examples very helpful:

http://logicmanual.philosophy.ox.ac.uk/carr/NDpack.pdf
lu60ruhy
Member since Apr 2018
15 posts
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 :-)
Jazzpirate
Member since Oct 2016
781 posts
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.
rappatoni
Member since Nov 2018
25 posts
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: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Page:  previous  1  2 
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen