Rechnergestütztes Beweisen (Hofmann, WS 2005/06)

2005-11-03

Satz (Vollständigkeit):
Gilt eine Sequenz G ==>L D in allen Interpretationen, so ist sie
beweisbar.

Beweis: wir zeigen: Hat G ==>L D keinen Beweis, so existiert eine
(Gegen-)interpretation II von L, so dass [|AND G|]_II = tt und 
[|OR D|]_II = ff.

Ein Herleitungsversuch (x,y:tau).  Sei c:tau in L.
phi = FORALL x EXISTS y R(x,y)
psi = EXISTS y FORALL x R(x,y)

...
-------------------------------------------
phi, R(c,e) ==>L,d,e:tau  R(d,c), psi
----------------------------------------------------- FORALL-R, EXISTS-L
phi, EXISTS y R(c,y) ==>L  FORALL x R(x,c), psi
------------------------------------------------------- FORALL-L,EXISTS-R,CONTR
FORALL x EXISTS y R(x,y) ==>L  EXISTS y FORALL x R(x,y)

Dabei werden immer mehr neue Konstanten in die Sprache eingeführt und
immer mehr atomare Aussagen produziert.

Zwei neue Regeln:

  G ==>L D, EXISTS x:tau.phi, phi(x:=t)
  ------------------------------------- (EXISTS-R') wobei >L t : tau  
  G ==>L D, EXISTS x:tau.phi

und eine entsprechende (FORALL-L').

Ein generischer Beweisbaum ist ein i.a. unendlicher Baum mit
folgenden Eigenschaften:

1. Knoten und Blätter sind mit Sequenzen beschriftet.

2. Jede Knotenbeschriftung ist Konklusion einer Regel (Ax, AND-L/R,
OR-L/R, IMPLIES-L/R, NOT-L/R, FORALL-R, EXISTS-L, FORALL-L',
EXISTS-R') [Permutation ist implizit]; die Kinder sind mit den
Prämissen beschriftet.

3. Blätter sind mit Axiomen oder atomaren Sequenzen beschriftet
(=Sequenzen aus atomaren Formeln P(ts)).  Kein innerer Knoten ist ein
Axiom. 

4. Regel EXISTS-R', FORALL-L' werden nur benutzt, wenn keine andere
Regel möglich ist.

5. Auf jedem unendlichen Pfad beginnend bei G ==>L D muss EXISTS-R',
FORALL-L' auf jeder passenden Formel mit allen typkorrekten Termen aus
L verwendet werden.

Hat Gamma ==>L Delta keinen Beweis, dann hat "der" generische
Beweisbaum entweder ein mit atomarem Nichtaxiom beschriftetes Blatt
(1. Fall) oder einen unendlichen Pfad (2. Fall).  Im ersten Fall
findet man ein Gegenmodell wie bei der Aussagenlogik.

Bemerkung: Die propositionalen Regeln und FORALL-R und EXISTS-R
reflektieren Wahrheit im folgenden Sinne: Hat

  Gamma ==>L,c:tau Delta, phi(x:=c) 

ein Gegenmodell II, so ist die Einschränkung II|L ein Gegenmodell zu

  Gamma ==>L Delta, FORALL x:tau.phi.

Im zweiten Fall sei
 
  G0 ==>L0 D0, G1 ==>L1 D1, ...

ein unendlicher Pfad im generischen Beweisbaum.

Es gilt: 
1) L0 <= L1 <= L2 ...
2) Enthält Di eine Formel EXISTS x:tau.phi, so ist diese Formel
Bestandteil von Dj für j>=i und EXISTS-R' wird auf diese Formel mit
allen Teiltermen angewandt.

Def: Sei L_oo = UNION L_i.  Wir konstruieren II wie folgt:

  [|tau|]_II = { t | 0 >L_oo t : tau }
 
  [|f|]_II(t1..tn) = f(t1..tn) falls f:[tau_1..tau_n -> tau]

  [|P|]_II(t1..tn) = tt, falls P(t1..tn) in einem Gi auftritt
                   = ff, sonst

     (wobei P:[tau1..taun -> boolean])

Bem: Falls P(ts) in Dj, so gilt [|P|](ts)=ff.

Beh: Kommt ein phi in Gi vor, so gilt [|phi|]_II = tt.  
     Kommt ein phi in Gi vor, so gilt [|phi|]_II = ff.  
Bew: Durch Induktion über den Aufbau von phi.

Fall: phi atomar: Beh folgt aus Def + Bem.

Fall: phi = phi1 AND phi2:  
* Sei phi in Gi, dann gibt es j>=i mit phi1,phi2 in Gj.  Nach IH ist
[|phi1|] = [|phi2|] = tt, also [|phi1 AND phi2|]=tt.
* Sei psi in Di, dann gibt es j>=i mit phi1 in Dj (oder phi2 in Dj).
Nach IH ist [|phi1|] = ff, also [|phi|]=ff.

Fall: phi = FORALL x:tau.phi1:  
* Wenn phi in Di, dann gibt es ein j>=i
mit phi1(x:=c) in Dj für ein frisches c.  Nach IH ist
[|phi1(x:=c)|]_II=ff, also [|phi1|]_II,x->c=ff, also 
[|FORALL x:tau.phi1|]_II = ff.
* Wenn phi in Gi, dann gilt [|FORALL x:tau.phi1|]_II = tt, falls für
alle >L_oo t : tau gilt [|phi1|]_II,x->t = [|phi1(x:=t)|]_II = tt.
Sei solch ein t beliebig vorgegeben.  Nach Konstruktion des
generischen Beweisbaums gibt es ein j>=i mit phi1(x:=t) in Gj.  Nach
IH gilt [|phi1(x:=t)|]=tt.

Q.E.D. 

Satz von Herbrand: 

Sei Phi Menge von geschlossenen Formeln (über einer Sprache L) der
Gestalt FORALL (xs:taus). phi(xs) mit phi(xs) quantorenfrei.  Phi hat
genau dann ein Modell (Interpretation, die alle Formeln in Phi wahr
macht), wenn folgende Menge von aussagenlogischen Formeln erfüllbar
ist:

 Pi_Phi = { phi(ts) | FORALL xs:taus.phi in Phi, 0 >L ti : taui }

(Hierbei werden die geschlossenen atomaren Formeln als
Aussagenvariablen verstanden.)

Beispiel: Phi = { FORALL x. R(x,f(x)), NOT R(f(c),f(f(c))) }

Pi_Phi = { NOT R(f(c),f(f(c))), R(c,f(c)), R(f(c),f(f(c))), ... }