Nicht angemeldet. · Kennwort vergessen · Registrieren

Seite:  vorherige  1  2 
F.W.
Mitglied seit 10/2018
4 Beiträge
Antwort auf Beitrag ID 159457
+2 lu60ruhy, tyr
For natural deduction I found these examples very helpful:

http://logicmanual.philosophy.ox.ac.uk/carr/NDpack.pdf
lu60ruhy
Mitglied seit 04/2018
15 Beiträge
Zitat von F.W.:
For natural deduction I found these examples very helpful:

http://logicmanual.philosophy.ox.ac.uk/carr/NDpack.pdf

That looks awesome :-)
Jazzpirate
Mitglied seit 10/2016
743 Beiträge
Antwort auf Beitrag 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
Mitglied seit 11/2018
23 Beiträge
Antwort auf Beitrag 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.
Schließen Kleiner – Größer + Auf diesen Beitrag antworten:
Prüfcode: VeriCode Gib bitte das Wort aus dem Bild ins folgende Textfeld ein. (Nur die Buchstaben eingeben, Kleinschreibung ist in Ordnung.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Weitere Zeichen:
Seite:  vorherige  1  2 
Gehe zu Forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen