Ich beschäftige mich mit dem Hilbert-Kalkül und stoße ständig auf folgendes Problem:
Zum Bsp. in diesem pdf ("http://jannissauer.de/files/prosem_ausarbeitung.pdf") p. 7:
leite aus ¬ ab, dass
(1) ¬ Voraussetzung
(2) A 0 (Axiom: ( ) ) im pdf p.5
(3) ¬ ∨ O1 1 , 2 (O1 Regel: ( , ⇒Hilbert ∨ ) ) im pdf p.6
(4) ¬ ∨ A1 (Axiom: ¬ ∨ )
(5) Kettenschluss 4 , 3
(6) MP 2 , 5
Mein Problem beginnt gleich in der zweiten Zeile. Wenn nur '(¬ )' gegeben ist, wie kommt der Autor dann dazu, mit '' im Axiom '' zu ersetzen.
Anders gewendet: Darf man eine gegebene Formel auseinandernehmen? In diesem Fall: darf ich aus dem Ausdruck '¬ ' den Ausdruck '' einfach herauslösen (und ihn in einem Axiom einsetzen).
In der dritten Zeile dasselbe: Der Autor substituiert in O1 '' mit '¬', '' mit '' und '' mit '' und das obwohl er nur Konditionalausdrücke zur Verfügung hat. Sowohl '' als auch '¬' müssten doch erst mit Schlussregeln gefolgert werden bevor sie für die weitere Ableitung zur Verfügung stehen?
p.s.: Im Falle dessen, dass es der einen oder dem anderen übel aufstößt, dass es sich hierbei um kein "klassisches" mathematisches Problem handelt, bitte ich um Entschuldigung.
