📐 Beweise der Aussagenlogik mit Lean 4: Ein praktischer Leitfaden 🔗

Dieser Beitrag bietet eine technische Einführung in grundlegende Konzepte der Aussagenlogik und deren formale Implementierung mit der Programmiersprache und dem Theorembeweiser Lean 4.

Egal, ob Sie als Mathematiker Beweise formalisieren möchten oder als Programmierer in die Typentheorie eintauchen: Dieser Leitfaden rekonstruiert die Logik von Grund auf. Wir beginnen mit einfachen logischen Konstanten und untersuchen, wie Lean 4 logische Konstrukte elegant mithilfe des Curry-Howard-Isomorphismus modelliert – dem Prinzip, dass Aussagen Typen und Beweise Programme sind.

📑 Inhaltsverzeichnis 🔗

⚙️ Die Präambel: Die Umgebung einrichten 🔗

Bevor wir unsere logischen Junktoren definieren, müssen wir eine grundlegende Umgebung einrichten. In Lean 4 geschieht dies typischerweise mit zwei spezifischen Befehlen, um den Gültigkeitsbereich (Scope) und das Berechnungsverhalten zu steuern.

namespace Basic

noncomputable section

• namespace Basic: Dieser Befehl gruppiert unsere Definitionen und verhindert Namenskonflikte mit der integrierten Standardbibliothek von Lean (der Prelude). Dadurch können wir grundlegende Strukturen wie True, False und And zu Lernzwecken von Grund auf neu definieren.
• noncomputable section: Lean 4 ist sowohl ein Theorembeweiser als auch eine funktionale Programmiersprache. Standardmäßig versucht Lean, für jede Definition ausführbaren Bytecode zu generieren. Das Markieren eines Abschnitts als noncomputable weist den Compiler an, diesen Schritt zu überspringen – was in der formalen Logik üblich ist, da uns dort mathematische Eigenschaften statt der Laufzeitausführung interessieren.

🧩 Grundlegende logische Junktoren 🔗

In diesem Abschnitt definieren wir die Grundbausteine der Logik und übertragen die mathematische Standardnotation in Lean-4-Code.

✅ 1. Wahr (True, ⊤) 🔗

Die einfachste Aussage ist eine, die universell logisch gültig ist. In Begriffen der Programmierung verhält sich $\top$ wie ein Unit-Typ – er besitzt genau einen Zustand und trägt keine zusätzlichen Daten.

Definition:

inductive True : Prop where
  | intro : True

Da er mit einem einzigen Konstruktor (intro) definiert ist, besteht der einzige Weg, True zu „beweisen“, darin, genau diesen Konstruktor bereitzustellen.

Beispiele:

-- True bedingungslos beweisen
example : True := True.intro

-- Jede Aussage 'a' impliziert trivialerweise True
example {a : Prop} : a → True := fun _ => True.intro

❌ 2. Falsch (False, ⊥) 🔗

Während True durch die triviale Existenz eines Beweises definiert ist, wird False durch das völlige Fehlen eines Beweises definiert. Es handelt sich um einen leeren Typ (Empty Type oder Void-Typ).

Definition:

inductive False : Prop

Da False keine Konstruktoren besitzt, kann es niemals aus dem Nichts instanziiert werden. Es repräsentiert einen logischen Widerspruch.

Das Explosionsprinzip (Ex Falso Quodlibet): Wenn Sie jemals einen Beweis für False in den Händen halten, bricht die Logik zusammen und Sie können alles beweisen. Lean setzt dies über den Rekursor False.elim um.

-- Aus einer Falschaussage folgt jede beliebige Aussage 'a' (⊥ → a)
def False.elim {a : Prop} (false_proof : False) : a := 
  false_proof.rec

🔄 3. Negation (¬) 🔗

In Lean 4 ist die Negation kein primitives, fest eingebautes Konzept. Stattdessen wird sie funktional über die Implikation und False definiert. Um zu beweisen, dass eine Aussage $a$ falsch ist (notiert als $\neg a$), müssen Sie eine Funktion angeben, bei der die Annahme von $a$ direkt zu einem Widerspruch ($\bot$) führt.

Definition:

def Not (a : Prop) : Prop := a → False

Wichtige Theoreme:

-- Negation beweisen: Wenn die Annahme von 'a' False beweist, dann gilt Not 'a'.
theorem Not.intro {a : Prop} (h : a → False) : Not a := 
  fun ha => h ha

-- Einführung der doppelten Negation (a → ¬¬a)
theorem not_not_intro {a : Prop} (ha : a) : Not (Not a) := 
  fun na => na ha  -- 'na' hat den Typ (a → False), die Übergabe von 'ha' liefert also False.

-- Modus Tollens: Wenn (a → b) und (¬b) gelten, dann gilt (¬a)
theorem Not.imp {a b : Prop} (nb : Not b) (ab : a → b) : Not a := 
  fun ha => 
    have hb : b := ab ha
    nb hb

➡️ 4. Implikation (→) 🔗

Da Lean auf der Typentheorie basiert, wird die logische Implikation ($a \to b$) buchstäblich als Funktion behandelt. Um zu beweisen, dass $a$ die Aussage $b$ impliziert, müssen Sie eine Funktion schreiben, die einen beliebigen Beweis von $a$ entgegennimmt und einen Beweis von $b$ zurückgibt.

Beispiel für verkettete Implikation: Wenn Sie $c$ in $a$ und $b$ in $d$ überführen können, lassen sich damit auch Funktionen von $a \to b$ in Funktionen von $c \to d$ transformieren.

theorem imp_imp_imp {a b c d : Prop} 
  (ca : c → a) (bd : b → d) : (a → b) → (c → d) := 
  fun ab => fun hc => 
    have ha : a := ca hc
    have hb : b := ab ha
    bd hb

🔗 5. Konjunktion (∧) 🔗

Die logische Konjunktion, die verlangt, dass sowohl $a$ als auch $b$ wahr sind, wird als structure modelliert. Aus Programmiersicht ist dies ein Produkttyp (ein Struct oder Tupel), der zwei separate Beweise (Evidenzen) enthält.

Definition:

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

Wichtige Beweismuster:

-- Einführung: Ein And erzeugen
example {a b : Prop} (ha : a) (hb : b) : And a b := 
  And.intro ha hb

-- Symmetrie: a ∧ b → b ∧ a
theorem And.symm {a b : Prop} (h : And a b) : And b a := 
  And.intro h.right h.left

🔀 6. Disjunktion (∨) 🔗

Die logische Disjunktion setzt voraus, dass mindestens eine der Aussagen wahr ist. Im Gegensatz zu And ist Or ein induktiver Summentyp (eine Tagged Union), da es zwei verschiedene, alternative Wege gibt, einen Beweis zu konstruieren.

Definition:

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

Um $a \lor b$ zu beweisen, verpacken Sie entweder einen Beweis von $a$ im Konstruktor inl (inject-left) oder einen Beweis von $b$ im Konstruktor inr (inject-right).

Beispiel:

-- Symmetrie: a ∨ b → b ∨ a
theorem Or.symm {a b : Prop} (h : Or a b) : Or b a :=
  match h with
  | Or.inl ha => Or.inr ha
  | Or.inr hb => Or.inl hb

↔️ 7. Logische Äquivalenz (↔) 🔗

Die Biimplikation bzw. „genau dann, wenn“ (Iff) drückt aus, dass zwei Aussagen logisch äquivalent sind. Sie ist als Struktur definiert, die Implikationen in beide Richtungen enthält.

Definition:

structure Iff (a b : Prop) : Prop where
  intro ::
  mp : a → b
  mpr : b → a

Beispiel für Reflexivität:

-- Jede Aussage ist äquivalent zu sich selbst (a ↔ a)
theorem Iff.refl {a : Prop} : Iff a a :=
  Iff.intro (fun ha => ha) (fun ha => ha)

🎯 Fazit und wichtigste Erkenntnisse 🔗

Indem wir die Aussagenlogik in Lean 4 von Grund auf neu aufbauen, wird die mechanische Eleganz formaler Systeme sichtbar:

1. Standardmäßig konstruktiv: Wir definieren, was es bedeutet, einen Beleg (Evidenz) für eine Wahrheit vorzuweisen, anstatt lediglich zu behaupten, dass etwas wahr ist.
2. Aussagen als Typen: Durch die Curry-Howard-Korrespondenz entsprechen logische Junktoren direkt gängigen Programmierstrukturen: Die Implikation ist eine Funktion, And ist ein Struct, Or ist ein Enum, True ist ein Unit-Typ und False ist ein Void-Typ.
3. Beweise als Programme: Das Schreiben eines mathematischen Beweises in Lean ist identisch mit dem Schreiben einer typsicheren Funktion, die eine bestimmte Signatur erfüllt.

Das Beherrschen dieser Grundbausteine bildet das entscheidende Fundament, um komplexere mathematische Theoreme, die Prädikatenlogik und die formale Verifikation komplexer Softwaresysteme zu meistern.