Rechnergestütztes Beweisen (Hofmann, WS07/08)

2005-11-02 VL 5
2007-10-31

Logik erster Stufe (Forts.)
==================

Spezielle Sprachen L:

Aussagenlogik: TT leer, FF leer, PP = Atome, ar(A) = [->boolean].
Mengenlehre:  TT={set}, FF leer, PP = {in},  ar(in) = [set,set->boolean].

Beispiele: Tautologien sind

1. FORALL x:tau. P(x) => EXISTS y:tau. P(y)
   Klammern:    (       (                  ))
   Sprache L: mindestens TT = { tau }, PP = { P:[tau -> boolean] }

2. (FORALL x:tau1. R(x,f(x))) => FORALL x:tau1. EXISTS y:t2. R(x,y)
   f : [tau1 -> tau2]
   R : [tau1,tau2 -> boolean]

3. (FORALL x:tau1. FORALL y:tau2. P(x) OR Q(y)) =>
     (FORALL x:tau1. P(x)) OR (FORALL y:tau2. Q(y)) 

   Bew: entweder P gilt für alle x, oder es gibt ein x0 für das P
   nicht gilt.  Dann aber gilt nach Voraussetzung P(x0) OR Q(y) für
   alle y, also FORALL y:tau2. Q(y).

4. (Q OR EXISTS x:tau1.P(x)) => EXISTS x:tau1. Q OR P(x)
   Q:[->boolean]
   P:[tau1->boolean]

   Nur dann Tautologie, wenn tau1 nicht leer ist.
   Z.B. falls c:[->tau1] in der Sprache ist.

5. Trinkerparadoxon:  Sei tau1 nicht leer.
   EXISTS x:tau1. P(x) => FORALL x:tau1. P(x)

   Bew (wie oben): Fallunterscheidung über P immer wahr oder P falsch
   für ein x0.

Bemerkung zu 3.: Keine Tautologie ist
   (FORALL x:tau1. P(x) OR Q(x)) =>
     (FORALL x:tau1. P(x)) OR (FORALL x:tau1. Q(x)) 
Z.B. tau1=N,P="gerade", Q="ungerade"


"Tautologie" ist für Logik erster Stufe unentscheidbar (auch wenn es
nur endlich viele Axiome gibt und nicht Axiomenschemata, wie z.B. in
der Axiomatisierung der Mengenlehre).

Seien x,y,z:tau.  Die Formel

  (FORALL x,y,z. R(x,y) AND R(y,z) IMPLIES R(x,z)) AND 
  (FORALL x. EXISTS y. R(x,y))
  IMPLIES EXISTS x. R(x,x)

gilt in allen endlichen Modellen (für alle II mit II(tau) endlich),
aber nicht z.B. im Modell tau=N und R(x,y)<==> x<y.


Sequenzenkalkül für Prädikatenlogik:

Sequenzen:  G ==>L D
- L ist eine Sprache.
- G(amma) und D(elta) sind Listen von geschlossenen wohlgeformten
  Formeln phi (für die also gilt: >L phi : boolean).

Bedeutung einer Sequenz:

  phi_1,...,phi_n ==>L psi_1,...,psi_m

bedeuted

  [|phi_1 AND ... AND phi_n IMPLIES psi_1 OR ... OR psi_m|]_II,rho = tt
  für alle Interpretationen II der Sprache L und alle Belegungen rho.

Regeln: Alle Regeln des Seq.kalküls für die Aussagenlogik plus die
Folgenden.


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

    (phi(x:=t) ist die Substitution von t für x in phi.)

  G, phi(x:=t) ==>L D
  -------------------------- (FORALL-L)
  G, FORALL x:tau.phi ==>L D

    (Diese Regel ist motiviert durch NOT EXISTS NOT = FORALL
                                 und NOT FORALL NOT = EXISTS)

  G ==>L,c:tau  D, phi(x:=c)
  -------------------------- (FORALL-R)
  G ==>L D, FORALL x:tau.phi

    (L,c:tau bezeichnet die Sprache L erweitert um eine neues
     Konstantensymbol c:[->tau])

  G, phi(x:=c) ==>L,c:tau  D
  -------------------------- (EXISTS-L)
  G, EXISTS x:tau.phi ==>L D

Beispiel:

  --------------------------- AX
  P(c) ==>L,c:tau  P(c), Q(c)
  -------------------------------------------- FORALL-L
  (FORALL x:tau.P(x)) ==>L,c:tau  P(c), Q(c)
  -------------------------------------------- OR-R
  (FORALL x:tau.P(x)) ==>L,c:tau  P(c) OR Q(c)
  --------------------------------------------------- FORALL-R
  (FORALL x:tau.P(x)) ==>L FORALL x:tau. P(x) OR Q(x)

Herleitung zu Beispiel 2.: FORALL-R, FORALL-L, EXISTS-R

Herleitung zu Beispiel 4.:  Es gibt c:tau in L. L':=L union {d:tau}
  
  ------------- AX            -------------------- OR-R + AX
  Q ==>L Q,P(c)               P(d) ==>L' Q OR P(d)
  ---------------- OR-R       -------------------------- EX-R
  Q ==>L Q OR P(c)            P(d) ==>L' EX x. Q OR P(x)
  --------------------- EX-R  ----------------------------- EX-L
  Q ==>L EX x.Q OR P(x)       EX x.P(x) ==>L EX x.Q OR P(x)
  --------------------------------------------------------- OR-L
  Q OR EXISTS x:tau.P(x) ==>L EXISTS x:tau. Q OR P(x)

Herleitung zu Beispiel 5.: In L gibt es ein c.

  gescheitert, da keine Tautologie
  ==>L P(c) => FORALL x:tau. P(x)
  --------------------------------------------- EXISTS-R
  ==>L EXISTS x:tau. P(x) => FORALL x:tau. P(x)

  sei phi = EXISTS x:tau. P(x) => FORALL x:tau. P(x)
  
  ----------------------------------------------- AXIOM
  P(c), P(d) ==>L,d:tau  P(d), FORALL x:tau. P(x)
  ------------------------------------------------- IMPLIES-R
  P(c) ==>L,d:tau  P(d), P(d) => FORALL x:tau. P(x)
  ------------------------------------------------- EXISTS-R
  P(c) ==>L,d:tau  phi, P(d)
  --------------------------------- FORALL-R
  P(c) ==>L phi, FORALL x:tau. P(x)
  ------------------------------------ IMPLIES-R
  ==>L phi, P(c) => FORALL x:tau. P(x)
  -------------------------------------------------- EXISTS-R
  ==>L phi, EXISTS x:tau. P(x) => FORALL x:tau. P(x)
  -------------------------------------------------- CONTR
  ==>L EXISTS x:tau. P(x) => FORALL x:tau. P(x)

Weiteres Beispiel: Quantorentausch

  (EX x:tau. FORALL y:tau'. R(x,y)) => FORALL y:tau'. EX x:tau. R(x,y)


PVS: (skolem ...) (skolem!) FORALL-R, EXISTS-L
     (inst ...)   (inst?)   FORALL-L, EXISTS-R
     (copy)                 CONTR
     M-x show-skolem-constants

     FORALL (x:tau): phi
     EXISTS (x:tau): phi


Turing bewies, dass die Praedikatenlogik auch ohne Funktionssymbole
unentscheidbar ist.  Obwohl sie fast, die Subformula-Property hat: Es
treten fast immer wieder diesselben Formeln auf, aber die
Substitutionsinstanzen sind unterschiedlich.

2005-11-03

Lemma (Alle Regeln erhalten die Allg.gueltigkeit):
Ist
     S1 ... Sn
     ---------
         S
Instanz einer Regel und sind S1...Sn allgemeingueltig, dann auch S.

Bsp:

  G  ==>L,c:tau  D, phi(x:=c)
  ---------------------------- (FORALL-R)
  G  ==>L  D, FORALL x:tau.phi

Sei G => D, phi(x:=c) eine Tautologie. (*)
Zu zeigen: In allen Interpretationen II von L gilt:

   G ==>L D, FORALL x:tau.phi

Sei [|AND G|]_II = tt und [|OR D|]_II = ff.  Zu zeigen:
[|FORALL x:tau.phi|]_II = tt, also zu zeigen [|phi|]_II,x->v = tt für
alle v in [|tau|]_II.  Sei so ein v fest, aber beliebig vorgegeben.
Erweitere II zu Interpretation II' von L,c:tau durch [|c|]_II' = v.
Aus (*) folgt jetzt [|phi(x:=c)|]_II' = [|phi|]_II,x->v = tt.
(NB: [|G|]_II' = [|G|]_II.)


Satz (Korrektheit des Sequenzenkalküls für Logik erster Stufe).
Ist eine Sequenz  phi_1,...,phi_n ==>L psi_1,...,psi_m
im Sequenzenkalkül beweisbar, so ist

  AND_{i=1..m} phi_i => OR_{j=1..m} psi_j

eine Tautologie.

Beweis: Induktion über Beweisbäume under Benutzung des Lemmas.


Vollstaendigkeit
----------------

Ersetze FORALL-L, EXISTS-R durch die folgenden, die Kontraktion
eingebaut haben:

Benutze nun WEAK, CONTR nicht mehr.  Wir zeigen: der neue Kalkuel ist
immer noch vollstaendig.

  G, FORALL x:tau.phi, phi[t/x]  ==>L  D
  -------------------------------------- FORALL-L'
  G, FORALL x:tau.phi            ==>L  D

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

Lemma: Alle Regeln des so entstandenen Beweissystems erhalten und
reflektieren Allgemeingueltigkeit.
Ist
     S1 ... Sn
     ---------
         S
Instanz einer Regel, dann sind S1...Sn allgemeingueltig gdw. S all.guelt.



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.

Wir konstruieren einen (i.A. unendlichen) Beweis"versuch" fuer S durch
systematische Rueckwaertsanwendung der Regeln.

1. Aggressive Rueckwaertsanwendung der Regeln ausser FORALL-L', EXISTS-R'.
   Danach stehen auf der linken Seite nur noch Atome und allq. Formeln,
   und auf der rechten Seite nur noch Atome und existentiellq. Formeln.

2. Rueckwaertsanwendung von FORALL-L', EXISTS-R', so dass auf jedem
   unendlichen Pfad jedes FORALL links und jedes EXISTS rechts irgendwann
   mit jedem Term instantiiert wird.  (Dafuer braucht es eine faire
   Strategie (round-robin)).