2005-10-20

Sequenzenkalkül

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)

Regeln:

  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, A ==> D   G, B ==> D
  ------------------- (OR-R)  ----------------------- (OR-L)
  G ==> D, phi OR psi          G, A OR B ==> 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

Bedeutung von G ==> D

  AND G ==> OR D

  AND {} = tt
  OR  {} = ff

Bsp:
  
  ------- (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)
                A ==> B, A
  ------- (ax)  ------------- (IMP-R)
  A ==> A       ==> A => B, A
  --------------------------- (IMP-L)
  (A => B) => A ==> A
  ------------------------ (IMP-R)
  ==> ((A => B) => A) => A

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

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.

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

Fall: 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.