Rechnergestütztes Beweisen (Hofmann, WS05/06)

2005-11-02 VL 5

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

Semantik: Sei L eine Sprache L = (TT, PP, FF, ar).  Eine
Interpretation II von TT ist gegeben durch

1. Eine Menge II(tau) für jedes tau in TT.
2. Eine Teilmenge II(P) <= II(tau1) x ... x II(taun) für jedes
   P : [tau1,...,taun->boolean] in PP.
3. Eine Funktion  II(f) : II(tau1) x ... x II(taun) -> II(tau) für
   jedes f : [tau1,...,taun -> tau] in FF.

Falls 0 >L phi : boolean, so lässt sich phi unter II ein Wahrheitswert
[|phi|]_II zuordnen.

Gegeben sei eine Interpretation II.  Eine Bewertung rho eines Kontexts

  K = x1:tau1, ..., xn:taun

ist eine partielle Funktion auf Variablen, so dass

  rho(xi) in [|taui|]_II  (das ist dasselbe wie II(taui)).

Durch Induktion über Term & Formelaufbau ordnen wir jedem Term  

  K > t : tau

und Bewertung rho von K einen Wert

  [[t]]_II,rho  in  [|tau|]_II

und jeder Formel  K > phi : boolean  einen Wahrheitswert

  [|phi|]_II,rho in {tt,ff}

zu.  (Ich lasse den Subskript II im Folgenden weg.)

  [|x|]_rho                = rho(x)

  [|f(t1,...,tn)|]_rho     = [[f]]_II ([|t1|]_rho, ..., [|tn|]_rho)

  [|FORALL x:tau.phi|]_rho = tt  gdw.  [|phi|]_rho[x->v] = tt 
                                       für alle Werte v in [|tau|]

  etc. (EXISTS, AND, OR, NOT)



Bemerkung:  Für Formeln unterscheiden wir

* wohlgeformt   (K > phi : boolean) [darf auch falsch sein]
* wahr          ([|phi|]_II,rho)
* und beweisbar (G ==> phi)

Definition.  Eine geschlossene Formel  phi  (0 > phi : boolean)
  ist Tautologie, wenn [|phi|]_II = tt (Abkürzung für [|phi|]_II,0)
  für alle I.

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"

(Exkurs: Brower-Heyting-Kolmogorov-Interpretation)


"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 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)

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