Beweisbegriff

Was ist ein Beweis?
Euklid: Formale Herleitung einer Aussage aus Regeln.

Axiome: z.B. Für je zwei ungleiche Punkte gibt es genau eine Gerade, die
diese Punkte verbindet.

Regeln: z.B. Falls "A dann B" und "A", dann auch "B". (modus ponens)

Grundlagenkrise (ca. 1900):  
  - zu viele Axiome
  - rein formales Rechnen kann zu falschen Ergebnissen führen, z.B.,
    wenn man die Gesetze von endlichen Summen auf unendliche überträgt:

  Bsp: Was ist der Wert von 1 - 1 + 1 - 1 + ...
  Euler: 0.5

Lösung der Krise: Mengenlehre

- möglichst wenig Axiome, möglichst viele Definitionen
- z.B. mengentheoretische Def der natürlichen Zahlen
- alles wird auf Begriffe und Axiome der Mengenlehre zurückgeführt

Axiome der Mengenlehre:
 
* Extensionalität: Zwei Mengen mit denselben Elementen sind gleich.

* Komprehension:  Teilmengen lassen sich durch Einschränkung bilden:

    forall x exists y. (forall z. z in y iff z in x and phi(z))

  für jede Eigenschaft phi.  Cantor's Fassung 

    exists y. (forall z. z in y iff phi(z))

  ist inkonsistent (Russel's Paradox). Wähle phi(z) = not (z in z)

"Startaxiome": Erzeugung von ersten Mengen.  Alle weiteren kann man
dann durch Einschränkung bilden.

* Potenzmenge:

   forall x exists y forall z. z in y iff z sub x

  z sub x == forall u. u in z implies u in x

* Vereinigungsmenge

* Unendlichkeit

Sei phi eine beliebige math. Aussage aufgeschrieben in der Sprache der
Mengenlehre (forall, exists, implies, in, =).

Ein formaler Beweis von phi ist eine Folge von Formeln phi_0, phi_1,
... phi_n mit phi = phi_n und für alle i <= n phi_i ist ein Axiom der
Mengenlehre order folgt aus den vorigen Formeln durch Schlussregel.

Prüfarbeit wird erleichtert wenn zu jeder Formel angegeben wird, ob
Axiom oder aus welchen früheren Formeln sie folgt.  Das ergibt einen
Beweisbaum oder Beweis-DAG (Baum mit sharing).


Ein Beweisprüfer (Beweisassistent, Theorembeweiser) ist eine Software,
die Beweise als solche identifizieren kann.  Der Komplexität wird
begegnet durch:

* Definitionen und Lemmas
* Entscheidungsverfahren

Motiviert durch Beweisaufgaben aus Verifikation (Hard-, Software).
Inzwischen auch für "mathematische" Beweise verwendet
(Vierfarbentheorem, Keplersche Vermutung).

Aufgaben eines Beweisprüfers:

* Beweisschritte überprüfen
* Verwalten von Hypothesen, Annahmen, zu zeigender Aussagen
* Entscheidungsverfahren
* Garantie (Beweisobjekt) erzeugen

Beispiele von Beweisprüfern:

* PVS (SRI, Menlo Park, US)
* Coq (Inria, F)
* Isabelle (Cambridge/TUM)



Aussagenlogik

Tarski-Semantik  [|phi|](eta) in { tt, ff }

Spiel-Semantik (Lorenzen, Erlangen): Beweis ist Gewinnstrategie

Problematisierung der Implikation

* Wenn MH in der VL Krawatte trägt, kann er Blei in Gold verwandeln.

* Beweisprinzip für Rekursion:

    m () Methode
    e    Rumpf

  Falsche Formalisierung: 

    (m korrekt => e korrekt) => m korrekt

  Damit wären alle m korrekt, denn

    ((A => B) => A) => A

  ist eine Tautologie (Peirce's Law).

Def: phi Tautologie, falls [|phi|](eta) = tt für alle Belegungen eta.
     phi erfüllbar,             -"-              eine Belegung eta  .
     phi unerfüllbar,           -"-              keine     -"-      .

Bem: phi Tautologie, falls (not phi) unerfüllbar.

Tautologie entscheidbar (ausprobieren aller Belegungen).

Es existieren effizientere Verfahren.