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

2005-11-10

Beweis von stetig(f(-)) => stetig(f(f(-))

Klausifizierung von stetig(f(-)):

1. Schritt: Pränexform
   FORALL x:elt FORALL U:umg EXISTS V:umg FORALL y:elt.
   enth(f(x),U) => enth(x,V) AND (enth(y,V) => enth(f(y),U))

2. Schritt: Skolemisierung
   FORALL x:elt FORALL U:umg FORALL y:elt.
   enth(f(x),U) => enth(x,skf1(x,U)) AND enth(y,skf1(x,U)) => enth(f(y),U)
   
3. Schritt: Klauselform
   { NOT enth(f(x),U), enth(x,skf1(x,U)) },
   { NOT enth(y,skf1(x,U)), enth(f(y),U) }

oder:

2. Schritt: Skolemisierung
   FORALL x:elt FORALL U:umg FORALL y:elt.
   enth(f(x),U) => enth(x,c_V(x,U)) AND enth(y,c_V(x,U)) => enth(f(y),U)
   
3. Schritt: Klauselform
   K1 = { NOT enth(f(x),U), enth(x,c_V(x,U)) },
   K2 = { NOT enth(y,c_V(x,U)), enth(f(y),U) }

Klausifizierung von NOT stetig(f(f(-))):

1. Schritt: Pränexform
   EXISTS x:elt EXISTS U:umg FORALL V:umg EXISTS y:elt.
   (enth(f(f(x)),U) AND NOT enth(x,V)) OR (enth(y,V) AND NOT enth(f(f(y)),U))

2. Schritt: Skolemisierung
   FORALL V:umg.
   (enth(f(f(skf2)),skf3) AND NOT enth(skf2,V)) OR 
     (enth(skf4(V),V) AND NOT enth(f(f(skf4(V))),skf3))

oder:

2. Schritt: Skolemisierung
   FORALL V:umg.
   (enth(f(f(c_x)),c_U) AND NOT enth(c_x,V)) OR 
     (enth(c_y(V),V) AND NOT enth(f(c_y(V)),c_U))

3. Schritt: Klauselform
   K3 = { enth(f(f(c_x)),c_U), enth(c_y(V),V)             }, 
   K4 = { enth(f(f(c_x)),c_U), NOT enth(f(f(c_y(V))),c_U) }, 
   K5 = { NOT enth(c_x,V)    , enth(c_y(V),V)             }, 
   K6 = { NOT enth(c_x,V)    , NOT enth(f(f(c_y(V))),c_U) } 

K1,K3: { enth (f(c_x), c_V(f(c_x),c_U)),  enth (c_y(V), V) }
+  K2: { "                             ,  enth (f(c_y(c_V(x,U))), U) }
...

Kompaktheitssatz für die erststufige Logik:

Sei Phi beliebige Formelmenge.  Phi hat ein Modell genau dann, wenn
jede endliche Teilmenge von Phi ein Modell hat.

Beweisskizze:  Hat Phi kein Modell, so existiert Herleitung der
leeren Klausel aus (Klausifizierung von Phi).  Diese benutzt nur
endlich viele Klauseln, also nur eine endliche Teilmenge von Phi.


Sei NN die Menge aller wahren Formeln der Arithmetik, das heisst:

Sprache: TT = { nat }
         FF = { 0, 1, +, * }
         PP = { = }

Standard-Interpretation II: 
         [|nat|] = Menge der natürlichen Zahlen N
         [|0|]   = null
         ...
         [|+|]   = Addition
         ...
NN = { phi | >L phi : boolean  und  [|phi|]_II = tt }

Sei  x >= y :<==> EXISTS z. x=y+z

Erweitere Spache um Konstante c:nat.

NN' = NN UNION { c >= 1 + 1 + ... + 1 | n in N }
                       (n Summanden)

Jede endliche Teilmenge von NN' hat ein Modell, nämlich

  II + [|c|]_II genügend groß

Nach dem Kompaktheitssatz gibt es eine Interpretation der Arithmetik,
die genau diesselben Formeln erfüllt wie II und trotzdem eine
unendlich große Zahl enthält.

(Diese unendlich große Zahl c zieht natürlich einen Rattenschwanz von
neuen Zahlen hinter sich her:

c-1, c-2, c-3, c-4, ...
c div 2, c div 3, c div 4, ...
c+1, c+2, c+3, c+4, ...
2c, 3c, 4c, 5c, ...
c*c, c*c*c, c*c*c*c, ...
etc.)


Prädikatenlogik mit Gleichheit:

Fest eingebautes zweistelliges Prädikatensymbol "=", d.h. eine neue
Typisierungsregel: 

  K >L t1 : tau     K >L t2 : tau
  -------------------------------
  K >L t1 = t2 : boolean

Erweiterung der Semantik:
  
  [|t1=t2|]_II,rho = tt, wenn [|t1|]_II,rho = [|t2|]_II,rho
                     ff, sonst

Erweiterung des Sequenzenkalküls:

Ein neues Axiom:

  ------------- (Refl) oder (=R)
  G ==>L D, t=t

Eine neue Regel:

  G, t1=t2 ==>L D, phi(x:=t2)  
  --------------------------- (Subst) oder (=L)
  G, t1=t2 ==>L D, phi(x:=t1)

Beispiel (Symmetrie):

  ---------------- (=R)
  t1=t2 ==>L t2=t2
  ---------------- (=L) mit phi(x) = (t2=x)
  t1=t2 ==>L t2=t1

Schnittregel: Falls

  G1 ==>L D1, phi   beweisbar

und

  phi, G2 ==>L D2   beweisbar

dann auch

  G1, G2 ==>L D1, D2.

Abgeleitete Regeln:

Mit Schnittregel und Symmetrie kann man die Substitution auch in der
anderen Richtung verwenden:

  G, t1=t2 ==>L D, phi(x:=t1)  
  --------------------------- (Subst') 
  G, t1=t2 ==>L D, phi(x:=t2)

Oder eine Gleichheit auf der linken Seite zum Einsatz bringen.

  G, t1=t2, phi(x:=t_(3-i)) ==>L D  
  -------------------------------- 
  G, t1=t2, phi(x:=t_i)     ==>L D

Transitivität:

  ---------------------- (Ax)
  t1=t2, t2=t3 ==> t2=t3
  ---------------------- (=L)
  t1=t2, t2=t3 ==> t1=t3
  
Kongruenz:

  --------------------- (Ax)
  t1=t2 ==> f(t2)=f(t2)
  --------------------- (=L)
  t1=t2 ==> f(t1)=f(t2)

Gentzenkalkül mit Gleichheit ist korrekt und vollständig.

Resolutionskalkül lässt sich auf Gleichheit verallgemeinern.


PVS-Befehle

(lemma "assoc")
(inst ...)
(replace -1 1)

(rewrite-lemma "assoc" (x "x!1" y "y!1" z "z!1"))
(rewrite-lemma "assoc" (x "x!1" y "y!1" z "z!1") :dir RL)

(rewrite "assoc")

(auto-rewrite "assoc")

(stop-rewrite "assoc")