Kalkül des natürlich Schliessens
2006-09-06 22:13
Fred
Ich versuche die Formel "X -> (Y -> X)" im Kalkül des natürlich Schliessens abzuleiten.
Also nehme ich an, dass X gilt, und versuche dann im selben Kasten zu Y -> X zu gelangen, damit ich den Kasten abschliessen und die zu beweisende Formel drunterschreiben kann:
Jetzt bin ich mir aber nicht im Klaren, wie ich von der Annahme X auf Y -> X kommen soll. Ein Versuch:
Frage: darf ich die Annahme X einfach so nochmal in den inneren Kasten schreiben? Ich finde weder im Skript noch im Fitting eine Antwort darauf.
Ausserdem: warum gibt es keine Ableitungsregel der folgenden Art?
Also nehme ich an, dass X gilt, und versuche dann im selben Kasten zu Y -> X zu gelangen, damit ich den Kasten abschliessen und die zu beweisende Formel drunterschreiben kann:
+--------+
| X |
| . |
| . |
| . |
| Y -> X |
+--------+
X -> (Y -> X)
Jetzt bin ich mir aber nicht im Klaren, wie ich von der Annahme X auf Y -> X kommen soll. Ein Versuch:
+--------+
| X |
| +----+ |
| | Y + |
| | X + | <-- Wiederholung der Annahme X
| +----+ |
| Y -> X |
+--------+
X -> (Y -> X)
Frage: darf ich die Annahme X einfach so nochmal in den inneren Kasten schreiben? Ich finde weder im Skript noch im Fitting eine Antwort darauf.
Ausserdem: warum gibt es keine Ableitungsregel der folgenden Art?
ß1
--
ß
Sprich, wenn A gilt dann doch auch AvB… das würde die Sache erheblich vereinfachen!