2005-10-19
2007-10-17

Sequenzenkalkül
===============

(Gerhard Gentzen, 1935)

Syntax der Aussagenlogik

  phi,psi ::= atome | phi AND psi | phi OR psi | NOT Phi | phi IMP psi

/\ (AND), \/ (OR), NOT, => (IMP) heissen Konnektive

Wahrheitstafeln fuer die Konnektive

Problematisierung der Implikation

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

Alternative Semantik a la Kripke: Eine Aussage ist gueltig in bezug
auf eine Welt.

Damit ist die Aussage "Wenn MH in der VL Krawatte trägt, kann er Blei
in Gold verwandeln." nicht mehr allgemeingueltig.  Denn es gibt eine
Welt in der MH eine Krawatte traegt, aber immer noch nicht Blei in
Gold verwandeln kann.

* Beweisprinzip für Rekursion:

    m () Methode
    e    Rumpf

  Falsche Formalisierung: 

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

  Waere dieses Prinzip allgemeingueltig, dann wären alle m korrekt, denn

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

  ist eine Tautologie (Peirce's Law).

Formale Semantik von aussagenlogischen Formeln. (Tarski)

Eine Umgebung ist eine Funktion

  eta : Atome -> {tt, ff}

Gegeben eine Umgebung eta, so ist die Semantik einer Formel phi ein
Wahrheitswert [[phi]]eta in {tt, ff}, rekursiv definiert durch:

  [[ A ]]eta          = eta(A)
  [[ phi op psi ]]eta = [[ phi ]]eta op [[ psi ]]eta
    fuer ein Konnektiv op

Kritik: Logik wird durch Logik erklaert.
Alternative: Spiel-Semantik (Lorenzen, Erlangen): Beweis ist Gewinnstrategie


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  gdw  (NOT phi) unerfüllbar.
     phi erfuellbar  gdw  (NOT phi) keine Tautologie

Tautologie entscheidbar (ausprobieren aller Belegungen).

Es existieren effizientere Verfahren.


2005-10-20

Def. Eine Sequenz ist ein Ausdruck der Form

       Gamma ==> Delta

wobei Gamma, Delta Listen von Formeln sind.  Namen:

  Gamma  Antezedens
  Delta  Sukzedens

Bedeutung von G ==> D

  AND G ==> OR D

  AND {} = tt
  OR  {} = ff

Am Ende interessiert man sich nur fuer Sequenzen der Form

  ==> phi       (d.h. phi ist Tautologie)

Im Verlauf des Beweises ergeben sich aber Sequenzen der allgemeinen Form.

[ NUR 2005
Motivation:

- nur 1-stellige rechte Seite, keine linke Seite 
  AND-R
  (ABER: Annahmen IMP-R)

- intuitionistischer Kalkül (fragmentarisch)
  OR-R, OR-L
  (ABER: Excl.Middle)

- klassischer Kalkül
]


Axiome:

  ---------------------------
  G1, phi, G2 ==> D1, phi, D2 (salopp: G ==> D mit G cap D not empty)

Bsp fuer Axiom:

  A, A AND B, NOT C ==> A AND B, D, E

Schlussregeln:

Haben die Form 

  S1 ... Sn
  ---------
      S

mit S,S1,...,Sn Sequenzen.  Dabei heissen die Si Praemissen und S
heisst Konklusion.

Regeln fuer die Konnektive:

  G ==> D, phi    G ==> D, psi          G, phi, psi ==> D
  ---------------------------- (AND-R)  -------------------- (AND-L)
  G ==> D, phi AND psi                  G, phi AND psi ==> D

  G ==> D, phi, psi            G, phi ==> D   G, psi ==> D
  ------------------- (OR-R)  ---------------------------- (OR-L)
  G ==> D, phi OR psi          G, phi OR psi ==> D

  G, phi ==> D                 G ==> D, phi
  ---------------- (NOT-R)     ---------------- (NOT-L)
  G ==> D, NOT phi             G, NOT phi ==> D

  G, phi ==> D, psi            G, psi ==> D   G ==> D, phi
  -------------------- (IMP-R) --------------------------- (IMP-L)
  G ==> D, phi IMP psi         G, phi IMP psi ==> D

Bsp fuer Herleitung:
  
  ------- (ax)
  A ==> A
  ------------ (NOT-R)
  ==> A, NOT A
  -------------- (OR-R)
  ==> A OR NOT A

Strukturelle Regeln:

  G ==> D, psi, phi            G, psi, phi ==> D       
  ----------------- (SWAP-R)   ----------------- (SWAP-L)
  G ==> D, phi, psi            G, phi, psi ==> D       

  G ==> D                      G ==> D
  ------------ (WEAK-R)        ------------ (WEAK-L)
  G ==> D, psi                 G, psi ==> D

  G ==> D, phi, phi            G, phi, phi ==> D          
  ----------------- (CONTR-R)  ----------------- (CONTR-R)
  G ==> D, phi                 G, phi ==> D               

Bsp:

  --------- ax   --------- ax
  A ==> B,A      B ==> B,A
  ------------------------ OR-L
  A OR B ==> B,A
  ----------------- OR-R
  A OR B ==> B OR A
  ------------------------- IMP-R
  ==> (A OR B) IMP (B OR A)

Bsp:

  ---------- ax  ---------- ax
  A, B ==> A     A, B ==> B
  ------------------------- AND-R
  A, B ==> A AND B
  ------------------------- WEAK-R
  A, B ==> A AND B, A AND C
  ------------------------------- OR-R        ...
  A, B ==> (A AND B) OR (A AND C)        A, C ==> ...
  --------------------------------------------------- OR-L
  A, B OR C ==> (A AND B) OR (A AND C) 
  ----------------------------------------- AND-L
  A AND (B OR C) ==> (A AND B) OR (A AND C)

[ NUR 2005
Bsp: 

                ---------- (ax)
                A ==> B, A
  ------- (ax)  ------------- (IMP-R)
  A ==> A       ==> A => B, A
  --------------------------- (IMP-L)
  (A => B) => A ==> A
  ------------------------ (IMP-R)
  ==> ((A => B) => A) => A
]

Def.: Ein Beweisbaum ist ein Baum, dessen Knoten mit Sequenzen
beschriftet sind, so dass fuer jeden inneren Knoten

   S1 ... Sn
     \ | /
       S

gilt, dass

   S1 ... Sn
   ---------
       S

Instanz einer Regel ist.

Bemerkung: Ein Beweisbaum, dessen Blaetter mit Axiomen beschriftet
sind, ist eine Herleitung.

Notation: Seien S1, ..., Sn, S Sequenzen

  S1, ..., Sn |- S    (|- ist Fregesches Ableitungssymbol "turnstile")

soll bedeuten, dass ein Beweisbaum exisitiert, an dessen Blättern
die Sequenzen S1, ..., Sn (oder Axiome) stehen und der S als Wurzel
hat.

Bsp:

  A ==> B, C
  --------------   -------
  A ==> (B OR C)   A ==> A
  ------------------------
  A ==> (B OR C) AND A

Also gilt   A ==> B,C |- A ==> (B OR C) AND A

Bsp 2:  A AND B => C, A AND B => D  |-  A AND B => C AND D

Satz (Korrektheit)
------------------

Falls S1, ..., Sn |- S, dann gilt: Für alle Belegungen eta, die
S1,...,Sn erfüllen, gilt: eta erfüllt S.

Insbesondere gilt: Sind S1,...,Sn Tautologien, so auch S.

Insbesondere: |- S, dann S ist Tautologie.

Beweis: Durch Induktion über Beweisbäume.


Motivation (Vollständigkeit):

Durch Rückwärtsanwendung einer Regel (Ausnahme: WEAK) vergibt man sich
nichts.

  S1, ..., Sn |-' S  bezeichne einen Beweisbaum ohne WEAK-Regeln 
                                            und ohne CONTR-Regeln

Lemma: Falls S1, ..., Sn |-' S und eta eine Belegung ist, die S
erfüllt, so erfüllt eta auch jedes Si.

Beweis: Induktion über Beweisbäume, z.B. letzte Regel: OR-L

 Ann:  Erfülle eta die Seq.  G, phi OR psi ==> D.
 Zz:   eta erfüllt G, phi ==> D.
 Wenn eta G und phi erfüllt, erfüllt eta erst recht G und (phi OR psi).
 Nach Voraussetzung also auch D
  

Satz (Vollständigkeit):  Ist S Tautologie, so gilt |-' S, also erst
recht |- S.

Bew: Durch systematische Rückwärtsanwendung der Regeln finden wir
atomare Sequenzen S1..Sn mit S1..Sn |-' S.

Nun unterscheiden wir die Faelle:

Fall: Alle S1..Sn sind Axiome. Dann |-' S.

Fall: S1 kein Axiom, also S1 = (G ==> D) und G, D disjunkt.  
      Dann gibt es eine Belegung, die S1 falsch macht.

      Bsp:  S1 = (A,B ==> C,D), dann setze A,B wahr, C,D falsch.

      Da S Tautologie, erfüllt eta S. Nach dem Lemma müsste S1 auch durch
      eta erfüllt werden.  Widerspruch.
     

Bsp.: Erzeugung eines Beweisbaums mit atomaren Sequenzen als Blaetter

  A,C ==> A   B,C ==> A        A,C => C   B,C ==> C
  --------------------- OR-L   -------------------- OR-L
  A OR B, C ==> A              A OR B, C ==> C
  -------------------------------------------- AND-R
  A OR B, C ==> A AND C

liefert das Gegenbeispiel  B,C = tt und A = ff.


Schnittregel, z.B.

  G ==> phi   G,phi ==> D
  ----------------------- CUT
  G ==> D

ist sicherlich korrekt.  Jede Tautologie kann aber auch ohne die
Schnittregel bewiesen werden.  (Konsequenz aus Vollstaendigkeit.)