Das deduktive System F0

Das deduktive System F₀ ist ein Kalkül. Es erlaubt durch eine reine Betrachtung des „wörtlichen“ (syntaktischen) Aufbaus einer Aussage Folgerungen zu treffen. Dies beutet außerdem, dass automatisiert Beweise für Aussagen gefunden werden können.

Wie jeder Kalkül gibt auch F₀ eine Menge von Axiomen (eigentlich: Axiomschemata) und Regeln vor. F₀ verwendet „Modus Ponens“ als einzige Regel. „Modus Ponens“ besagt, dass die rechte Seite einer Implikation bewiesen ist, wenn schon die Implikation selbst und die linke Seite bewiesen wurden. Gibt es also einen Beweis für A → B und A, so kann auch B als bewiesen angenommen werden. Die Axionsschemata in F₀ sind drei Formen Tautolgien, die nur die Negation (¬) und die Implikation (→) verwenden. Durch Einsetzen beliebiger Formlen (die nur → und ¬ verwenden) in diese Schemata, lassen sich bewiesene Aussagen generieren.

Neben den Axiomen gibt es außerdem noch eine Reihe von Theoremem, die schon bewiesen sind und wie die Axiomschemata verwendet werden dürfen. Auf der Webseite zur Logik im Sommersemester 2011 (Madlener) ist eine Zusammenfassung der Kalküle zu finden. Diese beinhaltet elf Theoreme und die drei Axiome aus F₀

Beispiel: z.Z. ⊢_F0 B → (¬C → ¬(B → C))

Wie wird ein Beweis in F₀ nun aufgeschrieben? Ich werde dies nun vorführen, indem ich Beweise, dass B → (¬C → ¬(B → C)) eine Tautologie ist. Die bedeutet, dass ich nur die Axiome (und nach Belieben die bewiesenen Theoreme) verwenden darf, um die Aussage herzuleiten. Es bietet sich an, das Deduktionstheorem anzuwenden:

• z.Z. ⊢_F0 B → (¬C → ¬(B → C))
• z.Z. B ⊢_F0 ¬C → ¬(B → C)

Es genügt also B als bewiesen anzunehmen und ¬C → ¬(B → C) herzuleiten.

1. B (als bewiesen angenommen)
2. ((B → C) → C) → (¬C → ¬(B → C)) (Theorem 8)
3. B → ((B → C) → C) (Theorem 5)
4. (B → C) → C (Modus Ponens 1. und 3.)
5. ¬C → ¬(B → C) (Modus Ponens 3. und 2.)

Das war es auch schon. Wichtig ist hierbei, immer die verwendeten Axiome (beziehungsweise Theoreme) und die mit Modus Ponens resultierenden Folgerungen getrennt voneinander auszuschreiben. Hier etwa hätte es nicht genügt 4. aufzuschreiben, ohne vorher 3. zu kennzeichnen!

Beispiel: z.Z. ⊢_F0 (A → B) → (¬B → ¬A)

Im vorigen Beispiel wurde das Theorem 8 verwendet. Als weiteres Beispiel werde ich dieses nun herleiten. Es erinnert stark an Axiom 3 ((¬A → ¬B) → (B → A)). Durch Einsetzen von ¬A und ¬B in Axiom 3 lässt sich auch etwa sehr Ähnliches bekommen: (¬¬A → ¬¬B) → (¬B → ¬A) In der semantischen Welt könnte einfach ¬¬A durch A und ¬¬B durch B ersetzt werden. Da in F₀ jedoch alles syntaktisch ist, geht das nicht. Es ist insbesondere auch nicht erlaubt die Negationen wegzulassen und „siehe Theorem 3 (¬¬A → A)“ zu schreiben. Sinnvoll ist hier ein Zwischenbeweis.

Zwischenbeweis: z.Z. ⊢_F0 (A → B) → (¬¬A → ¬¬B)

Zweifache Anwendung des Deduktionstheorems

• z.Z. ⊢_F0 (A → B) → (¬¬A → ¬¬B)
• z.Z. (A → B) ⊢_F0 ¬¬A → ¬¬B
• z.Z. (A → B), ¬¬A ⊢_F0 ¬¬B

(A → B) und ¬¬A werden also als gegeben angenommen und ¬¬B ist herzuleiten.

1. A → B (als bewiesen angenommen)
2. ¬¬A (als bewiesen angenommen)
3. ¬¬A → A (Theorem 3)
4. A (Modus Ponens 2. und 3.)
5. B (Modus Ponens 4. und 1.)
6. B → ¬¬B (Theorem 7)
7. ¬¬B (Modus Ponens 5. und 6.)

Anwendung des Zwischenbeweises

Der Zwischenbeweis ist nun ungemein hilfreich. Zunächst wird das Deduktionstheorem benutzt.

• ⊢_F0 (A → B) → (¬B → ¬A)
• (A → B) ⊢_F0 (¬B → ¬A)

Nun kann der Zwischenbeweis leicht eingesetzt werden:

1. A → B (als bewiesen angenommen)
2. (A → B) → (¬¬A → ¬¬B) (Aus dem Zwischenbeweis)
3. ¬¬A → ¬¬B (Modus Ponens 1. und 2.)
4. (¬¬A → ¬¬B) → (¬B → ¬A) (Axiom 3)
5. ¬B → ¬A (Modus Ponens 3. und 4.)

Weitere Beispiele finden sich in den Übungsaufgaben vom Sommersemester 2011.