Frage zum Hilbert-Kalkül
-
Hallo,
ich verstehe da etwas bei einem Beispiel zum Hilbert-Kalkül in der Wikipedia nicht ganz:
http://de.wikipedia.org/wiki/Hilbert-Kalkül#Modus_.28ponendo.29_ponens
(Das URL-Tag scheint kaputt zu sein?!)Im ersten Schritt wird eine Instanz von Axiom 1 erstellt. Dabei wird G durch (B\rightarrow A) ersetzt. Ich verstehe nicht ganz, warum man das darf. Schließlich ist doch (B -> A) keine Instanz eines Axioms und innerhalb des Kalküls auch noch nicht bewiesen. Wäre super, wenn mir das jemand erklären könnte.
Grüße,
Michael
-
So funktioniert Substitution nunmal: Jedes Vorkommen eines Aussagensymbols wird durch die gleiche Formel ersetzt.
Warum macht das Sinn? Seien F eine Tautologie, sub eine Substitution, dann ist sub(F) wieder eine Tautologie. Falls wir also einen korrekten Kalkül haben, sind auch sämtliche Substitutionen von Axiomen und abgeleiteten Formeln wieder Tautologien.
-
Ah, ok, so ergibt das mehr Sinn. Danke für die Erklärung!
Grüße,
Michael