Post on 05-Aug-2019
transcript
Grundbegri�e der InformatikKapitel 13: Prädikatenlogik erster Stufe
Thomas Worsch
KIT, Institut für Theoretische Informatik
Wintersemester 2015/2016
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 1 / 63
Überblick
Syntax prädikatenlogischer Formeln
Semantik prädikatenenlogischer Formeln
Freie und gebundene Variablenvorkommen und Substitutionen
Beweisbarkeit
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 2 / 63
Wo sind wir?
Syntax prädikatenlogischer Formeln
Semantik prädikatenenlogischer Formeln
Freie und gebundene Variablenvorkommen und Substitutionen
Beweisbarkeit
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 3 / 63
Prädikatenlogische Formelnkomplizierter aufgebaut als aussagenlogische
drei Schri�eTerme
Variablensymbole, Konstantensymbole, Funktionssymboleatomare Formeln
aus Termenmi�els Relationssymbolen
prädikatenlogische Formelnaus atomaren Formelnmi�els aussagenlogischer Konnektive undsogenannter �antoren
nicht nur die Syntax ist aufwändiger . . .
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 4 / 63
Prädikatenlogische Formeln — der Aufwand lohnt sichkompliziertere Syntax
aufwändigere Definitionen
aber (deswegen) viele benutztbeim „alltäglichen Formulieren“
Definitionen, Aussagen, Beweise
bei der Verifikation von Algorithmen
großzügige Benutzungnach Abschluss dieses Kapitels
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 5 / 63
Terme — benötigte AlphabeteVariablensymbole: Alphabet VarPL
xi (für endliche viele i ∈ N0)kurz x, y, z
Konstantensymbole: Alphabet ConstPLci (für endliche viele i ∈ N0)kurz c, d
Funktionsymbole: Alphabet FunPLfi (für endliche viele i ∈ N0)kurz f, g, hjedes fi ∈ FunPL hat Stelligkeit ar(fi ) ∈ N+
ATer = {(, ,, )} ∪ VarPL ∪ ConstPL ∪ FunPL
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 6 / 63
Terme — SyntaxGrammatik (NTer ,ATer ,T, PTer )
m maximale Stelligkeit von Funktions- bzw. Relationssymbolen
m + 1 Nich�erminalsymboleNTer = { T } ∪ { Li | i ∈ N+ und i ≤ m }
Produktionen
Li+1 → Li,T für jedes i ∈ N+ mit i < m
L1 → TT→ ci für jedes ci ∈ ConstPLT→ xi für jedes xi ∈ VarPLT→ fi(Lar(fi )) für jedes fi ∈ FunPL
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 7 / 63
Terme — BeispielBestandteile
VarPL = {x, y}ConstPL = {c}FunPL = {f, g} mit ar(f) = 2 und ar(g) = 1
DannNTer = {T,L1,L2}PTer = {L2 → L1,T , L1 → T
T→ c | x | y
T→ g(L1) | f(L2)}
BeispielableitungenL1 ⇒∗ c und T⇒∗ g(c)L2 ⇒∗ x,g(c)und T⇒∗ f(x,g(c))
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 8 / 63
Terme — BeispielBestandteile
VarPL = {x, y}ConstPL = {c}FunPL = {f, g} mit ar(f) = 2 und ar(g) = 1
DannNTer = {T,L1,L2}PTer = {L2 → L1,T , L1 → T
T→ c | x | y
T→ g(L1) | f(L2)}
nicht ableitbarxy c(x) f)x,y( g(c,c,c,x)
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 8 / 63
Atomare Formeln — SyntaxRelationsymbole: Alphabet RelPL=̇ immer dabeiRi (für endliche viele i ∈ N0)kurz als R, Sjedes Ri ∈ RelPL hat Stelligkeit ar(Ri ) ∈ N+
ARel = ATer ∪ RelPL
Grammatik (NRel,ARel,A, PRel )m maximale Stelligkeit von Funktions- bzw. RelationssymbolenNRel = { A,T } ∪ { Li | i ∈ N+ und i ≤ m }PRel = PTer ∪ {A→ Ri(Lar(Ri )) | für jedes Ri ∈ RelPL }
∪ { A→ T =̇T } .
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 9 / 63
Atomare Formeln — Beispielebei geeigneter Wahl von VarPL , ConstPL , FunPL sowie
RelPL = {R, S}mit ar(R) = 3 und ar(S) = 1
ableitbarg(x)=̇ f(x,g(z))S(c)R(y, c, g(x))
syntaktisch falschx =̇ y =̇ z R =̇ f S(x)=̇ S(x)
R(x,y) f(S(x)) R(S(x),x,x)
(S(S))(x) R)x,y(gRf() x R(zx < y
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 10 / 63
Prädikatenlogische Formeln — SyntaxAFor = ARel ∪ { , >, <, , , }
AllquantorExistenzquantor
Grammatik (NFor ,AFor ,F, PFor )NFor = { F } ∪ NRelPFor = PRel ∪ { F→ A }
∪ { F→( F), F→(F > F)}∪ { F→(F < F), F→(F F)}∪ { F→( xi F) | xi ∈ VarPL }
∪ { F→( xi F) | xi ∈ VarPL }
Klammereinsparungsregeln wie in Aussagenlogikzusätzlich: �antoren binden noch stärker als alle andere
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 11 / 63
Prädikatenlogische Formeln — Beispielex R(x,y) > S(x)
Kurzform von( x R(x,y)) > S(x)
( x x =̇ y) ( x x =̇ y)
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 12 / 63
Was ist wichtigDas sollten Sie mitnehmen:
Termeatomare FormelnFormeln
Das sollten Sie üben:Formeln analysieren
Syntaxfehler suchenFormeln schreiben
Syntaxfehler vermeiden ;-)
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 13 / 63
Wo sind wir?
Syntax prädikatenlogischer Formeln
Semantik prädikatenenlogischer Formeln
Freie und gebundene Variablenvorkommen und Substitutionen
Beweisbarkeit
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 14 / 63
InterpretationenAlphabete ConstPL , FunPL und RelPL gegeben
Interpretation (D, I )
nichtleere Menge D, das UniversumI (ci ) ∈ D für ci ∈ ConstPLI (fi ) : Dar(fi ) → D für fi ∈ FunPLI (Ri ) ⊆ Dar(Ri ) für Ri ∈ RelPL
BeispielD = N0I (c) = 0ar(f) = 2 und I (f) : N2
0 → N0 : (x ,y) 7→ x + yar(R) = 2 und I (R) = {(x ,y) | x ≤ y} ⊆ N2
0
Variablenbelegung β : VarPL → D
z. B. β (x) = 3 und β (y) = 42
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 15 / 63
valD,I ,β — ein Wert für jeden Termund ein Wahrheitswert für jede Formel
Alphabete ConstPL , FunPL und RelPL gegeben
Interpretation (D, I )
Variablenbelegung β : VarPL → D
definiere valD, I,β : LTer ∪ LFor → D ∪ Bfür jeden Term t : valD, I,β (t ) ∈ Dfür jede Formel G: valD, I,β (G ) ∈ B
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 16 / 63
valD,I ,β — ein Wert in D für jeden Term
Interpretation (D, I )Variablenbelegung β : VarPL → D
für Term t ∈ LTer drei MöglichkeitenvalD, I,β (xi ) = β (xi ) für xi ∈ VarPLvalD, I,β (ci ) = I (ci ) für ci ∈ ConstPLvalD, I,β (fi(t1, . . . ,tk)) = I (fi ) (valD, I,β (t1), . . . , valD, I,β (tk ))
erstes BeispielD = N0, I (c) = 0, I (f) Additionβ (x) = 3 und β (y) = 42valD, I,β (f(y,c)) = I (f) (valD, I,β (y), valD, I,β (c))
= I (f) (β (y), I (c))
= I (f) (42, 0)= 42 + 0 = 42
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 17 / 63
valD,I ,β — ein Wert in D für jeden Term
Interpretation (D, I )Variablenbelegung β : VarPL → D
für Term t ∈ LTer drei MöglichkeitenvalD, I,β (xi ) = β (xi ) für xi ∈ VarPLvalD, I,β (ci ) = I (ci ) für ci ∈ ConstPLvalD, I,β (fi(t1, . . . ,tk)) = I (fi ) (valD, I,β (t1), . . . , valD, I,β (tk ))
zweites BeispielD = {a,b}+, I (c) = bab, I (f) Konkatenationβ (x) = aaa und β (y) = bavalD, I,β (f(y,c)) = I (f) (valD, I,β (y), valD, I,β (c))
= I (f) (β (y), I (c))
= I (f) (ba,bab)= ba · bab = babab
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 17 / 63
valD,I ,β — ein Wahrheitswert für jede atomare Formel
Interpretation (D, I )Variablenbelegung β : VarPL → D
für atomare Formel A ∈ LRel zwei MöglichkeitenvalD, I,β (Ri(t1, . . . , tk)) =
w, falls (valD, I,β (t1), . . . , valD, I,β (tk )) ∈ I (Ri )
f, falls (valD, I,β (t1), . . . , valD, I,β (tk )) < I (Ri )
valD, I,β (t1 =̇ t2) =
w, falls valD, I,β (t1) = valD, I,β (t2)
f, falls valD, I,β (t1) , valD, I,β (t2)
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 18 / 63
valD,I ,β — Beispiel für atomare Formeln
valD, I,β (Ri(t1, . . . , tk)) =
w, falls (valD, I,β (t1), . . . , valD, I,β (tk )) ∈ I (Ri )
f, falls (valD, I,β (t1), . . . , valD, I,β (tk )) < I (Ri )
valD, I,β (t1 =̇ t2) =
w, falls valD, I,β (t1) = valD, I,β (t2)
f, falls valD, I,β (t1) , valD, I,β (t2)
BeispielD = N0, I (c) = 0, I (f) Addition, I (R) Kleiner-oder-gleichβ (x) = 3 und β (y) = 42
valD, I,β (R(y,c)) = wgdw. (valD, I,β (y), valD, I,β (c)) ∈ I (R)
gdw. (β (y), I (c)) ∈ I (R)
gdw. (42, 0) ∈ I (R)gdw. 42 ≤ 0 also ist valD, I,β (R(y,c)) = f
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 19 / 63
valD,I ,β — ein Wahrheitswert für jede Formel
Interpretation (D, I )Variablenbelegung β : VarPL → D
für Formel G ∈ LFor mehrere MöglichkeitenH , H1 > H2, H1 < H2, H1 H2
wie in der Aussagenlogikz. B. valD, I,β (H1 > H2) = b > (valD, I,β (H1), valD, I,β (H2))
xi H , xi Herfordert eine kleine Vorbereitung
für β : VarPL → D, xi ∈ VarPL und d ∈ D sei
βdxi : VarPL → D : xj 7→
β (xj ) falls j , i
d falls j = i
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 20 / 63
valD,I ,β — ein Wahrheitswert für jede Formel
Interpretation (D, I )Variablenbelegung β : VarPL → D
für Formel G ∈ LFor mehrere MöglichkeitenH , H1 > H2, H1 < H2, H1 H2
wie in der Aussagenlogikz. B. valD, I,β (H1 > H2) = b > (valD, I,β (H1), valD, I,β (H2))
xi H , xi Herfordert eine kleine Vorbereitung
für β : VarPL → D, xi ∈ VarPL und d ∈ D sei
βdxi : VarPL → D : xj 7→
β (xj ) falls j , i
d falls j = i
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 20 / 63
valD,I ,β — Wahrheitswert für quantifizierte Formeln
Interpretation (D, I )Variablenbelegung β : VarPL → D
valD, I,β ( xi H ) =
w, falls für jedes d ∈ D und β ′ = βdxi gilt:
valD, I,β ′ (H ) = wf, sonst
valD, I,β ( xi H ) =
w, falls für mind. ein d ∈ D und β ′ = βdxi gilt:
valD, I,β ′ (H ) = wf, sonst
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 21 / 63
valD,I ,β — Beispiel für quantifizierte Formeln
Interpretation (D, I ), Variablenbelegung β : VarPL → D
valD, I,β ( xi H ) =
w, falls für jedes d ∈ D und β ′ = βdxi gilt:
valD, I,β ′ (H ) = wf, sonst
BeispielD = N0, I (c) = 0, I (f) Addition, I (R) Kleiner-oder-gleichβ (x) = 3 und β (y) = 42
valD, I,β ( x R(c,x)) = w
gdw. für alle d ∈ D, β ′ = βdx : (valD, I,β ′ (c), valD, I,β ′ (x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (I (c), β ′(x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (0,d ) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : 0 ≤ d also ist valD, I,β ( x R(c,x)) = w
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 22 / 63
valD,I ,β — Beispiel für quantifizierte Formeln
Interpretation (D, I ), Variablenbelegung β : VarPL → D
valD, I,β ( xi H ) =
w, falls für jedes d ∈ D und β ′ = βdxi gilt:
valD, I,β ′ (H ) = wf, sonst
BeispielD = N0, I (c) = 0, I (f) Addition, I (R) Kleiner-oder-gleichβ (x) = 3 und β (y) = 42
valD, I,β ( x R(c,x)) = w
gdw. für alle d ∈ D, β ′ = βdx : (valD, I,β ′ (c), valD, I,β ′ (x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (I (c), β ′(x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (0,d ) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : 0 ≤ d also ist valD, I,β ( x R(c,x)) = w
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 22 / 63
valD,I ,β — Beispiel für quantifizierte Formeln
Interpretation (D, I ), Variablenbelegung β : VarPL → D
valD, I,β ( xi H ) =
w, falls für jedes d ∈ D und β ′ = βdxi gilt:
valD, I,β ′ (H ) = wf, sonst
BeispielD = N0, I (c) = 0, I (f) Addition, I (R) Kleiner-oder-gleichβ (x) = 3 und β (y) = 42
valD, I,β ( x R(c,x)) = w
gdw. für alle d ∈ D, β ′ = βdx : (valD, I,β ′ (c), valD, I,β ′ (x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (I (c), β ′(x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (0,d ) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : 0 ≤ d also ist valD, I,β ( x R(c,x)) = w
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 22 / 63
valD,I ,β — Beispiel für quantifizierte Formeln
Interpretation (D, I ), Variablenbelegung β : VarPL → D
valD, I,β ( xi H ) =
w, falls für jedes d ∈ D und β ′ = βdxi gilt:
valD, I,β ′ (H ) = wf, sonst
BeispielD = N0, I (c) = 0, I (f) Addition, I (R) Kleiner-oder-gleichβ (x) = 3 und β (y) = 42
valD, I,β ( x R(c,x)) = w
gdw. für alle d ∈ D, β ′ = βdx : (valD, I,β ′ (c), valD, I,β ′ (x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (I (c), β ′(x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (0,d ) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : 0 ≤ d also ist valD, I,β ( x R(c,x)) = w
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 22 / 63
valD,I ,β — Beispiel für quantifizierte Formeln
Interpretation (D, I ), Variablenbelegung β : VarPL → D
valD, I,β ( xi H ) =
w, falls für jedes d ∈ D und β ′ = βdxi gilt:
valD, I,β ′ (H ) = wf, sonst
BeispielD = N0, I (c) = 0, I (f) Addition, I (R) Kleiner-oder-gleichβ (x) = 3 und β (y) = 42
valD, I,β ( x R(c,x)) = w
gdw. für alle d ∈ D, β ′ = βdx : (valD, I,β ′ (c), valD, I,β ′ (x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (I (c), β ′(x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (0,d ) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : 0 ≤ d
also ist valD, I,β ( x R(c,x)) = w
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 22 / 63
valD,I ,β — Beispiel für quantifizierte Formeln
Interpretation (D, I ), Variablenbelegung β : VarPL → D
valD, I,β ( xi H ) =
w, falls für jedes d ∈ D und β ′ = βdxi gilt:
valD, I,β ′ (H ) = wf, sonst
BeispielD = N0, I (c) = 0, I (f) Addition, I (R) Kleiner-oder-gleichβ (x) = 3 und β (y) = 42
valD, I,β ( x R(c,x)) = w
gdw. für alle d ∈ D, β ′ = βdx : (valD, I,β ′ (c), valD, I,β ′ (x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (I (c), β ′(x)) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : (0,d ) ∈ I (R)
gdw. für alle d ∈ D, β ′ = βdx : 0 ≤ d also ist valD, I,β ( x R(c,x)) = wGBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 22 / 63
Allgemeingültige Formelnprädikatenlogische Formel F allgemeingültig, wenn
für jede passende Interpretation (D, I ) undjede passende Variablenbelegung β gilt:valD, I,β (F ) = w.
einfache Beispiele:aussagenlogischer Tautologie Gfür vorkommende Aussagevariable Pije eine beliebige prädikatenlogische Formel Giersetze in G jedes Pi syntaktisch durch Gi
prädikatenlogische Tautologien
Beispiel
R(x,y) (( x f(y)=̇ c) R(x,y))GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 23 / 63
Allgemeingültige Formeln — aber keine TautologienBeispiele (für t1, t2 ∈ LTer )
(t1 =̇ t2) (t2 =̇ t1)
Beispiele (für G,H ∈ LFor )
( xi (G H)) (( xi G) ( xi H))
Beispiele (für t ∈ LTer )
( x R(x)) R(t)
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 24 / 63
Modelle(D, I ) Modell für G ∈ LFor , wenn
(D, I ) Interpretation für G undfür jedes β ist valD, I,β (G ) = w.
(D, I ) Modell für Γ ⊆ LFor , wenn(D, I ) Modell für jedes G ∈ Γ
Γ |= G, wennjedes Modell von Γ auch Modell von G
H |= G, wenn {H } |= G
|= G, wenn {} |= G,d. h. wenn G allgemeingültig
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 25 / 63
Modelle — BeispielFormel: x f(x,c)=̇ x
Modell: D = N0, I (c) = 0, I (f) Additionanschaulich: für jede nichtnegative ganze Zahl x ist x + 0 = xgenauer: prüfe, ob für jedes β gilt: valD, I,β (G ) = wprüfe für d ∈ N0 und β ′ = βdx , obvalD, I,β ′ (f(x,c)=̇ x) = wgdw. valD, I,β ′ (f(x,c)) = valD, I,β ′ (x) ist.linke Seite I (f) (β ′(x), I (c)) = β ′(x) + 0 = β ′(x)gleich rechter Seite
anderes Modell von G:D = {a,b}∗, I (c) = ε , I (f) Konkatenation
kein Modell: D = N0, I (c) = 0, I (f) Multiplikation
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 26 / 63
Was ist wichtigDas sollten Sie mitnehmen:
InterpretationenWerte in D für jeden TermWahrheitswert für jede Formel
Modelle
Das sollten Sie üben:Terme und Formeln auswertenFormeln auf Allgemeingültigkeit prüfen
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 27 / 63
Wo sind wir?
Syntax prädikatenlogischer Formeln
Semantik prädikatenenlogischer Formeln
Freie und gebundene Variablenvorkommen und Substitutionen
Beweisbarkeit
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 28 / 63
Vorkommen von Variablensymbolen in Formelnnur Vorkommen in Termen
nicht die Symbole unmi�elbar hinter �antoren
gleiche Variable kann an mehreren Stellen vorkommen
unterscheide freie und gebundene Vorkommen
definiereMenge fv(G ) der frei vorkommenden Variablen unddie Menge bv(G ) der gebunden vorkommenden Variablen
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 29 / 63
freie und gebundene Vorkommen vonVariablensymbolen
atomare Formel Galle Vorkommen von Variablen sind freibv(G ) = {}fv(G ) Menge aller in G an mindestens einer Stellevorkommenden Variablen.
G = H
bv(G ) = bv(H ) und fv(G ) = fv(H )freies bzw. gebundenes Vorkommen in Hist ein freies bzw. gebundenes Vorkommen in G.
G ∈ { H1 > H2,H1 < H2,H1 H2}
bv(G ) = bv(H1) ∪ bv(H2) und fv(G ) = fv(H1) ∪ fv(H2)freies bzw. gebundenes Vorkommen in Hiist ein freies bzw. gebundenes Vorkommen in G.
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 30 / 63
freie und gebundene Vorkommen vonVariablensymbolen (2)
G von der Form( xi H)oder( xi H)
bv(G ) =
bv(H ) ∪ {xi } falls xi ∈ fv(H )
bv(H ) sonstfv(G ) = fv(H ) r {xi }in G alle Vorkommen der Variablen xi gebundenVorkommen anderer Variablen in G frei bzw. gebundenwie in H
Redeweisen: alle in H freien Vorkommen von xibefinden sich im Wirkungsbereich des �antors am Anfangwerden durch den �antor am Anfang von G gebunden
Formel G geschlossen, wenn fv(G ) = {}
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 31 / 63
freie und gebundene Vorkommen vonVariablensymbolen
Beispiel x( R(x,y) > y R(x,y))sechstes Zeichen
erstes Vorkommen von xVorkommen gebunden durch Allquantor am Anfang
fünfzehntes Zeichenzweites Vorkommen von xVorkommen gebunden durch Allquantor am Anfang
achtes Zeichenerstes Vorkommen von yfreies Vorkommen
siebzehntes Zeichenzweites Vorkommen von yVorkommen gebunden durch Existenzquantor
also bv(G ) = {x, y} und fv(G ) = {y}
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 32 / 63
freie und gebundene Vorkommen vonVariablensymbolen
Beispiel x( R(x,y) > y R(x,y))sechstes Zeichen
erstes Vorkommen von xVorkommen gebunden durch Allquantor am Anfang
fünfzehntes Zeichenzweites Vorkommen von xVorkommen gebunden durch Allquantor am Anfang
achtes Zeichenerstes Vorkommen von yfreies Vorkommen
siebzehntes Zeichenzweites Vorkommen von yVorkommen gebunden durch Existenzquantor
also bv(G ) = {x, y} und fv(G ) = {y}
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 32 / 63
freie und gebundene Vorkommen vonVariablensymbolen
Beispiel x( R(x,y) > y R(x,y))sechstes Zeichen
erstes Vorkommen von xVorkommen gebunden durch Allquantor am Anfang
fünfzehntes Zeichenzweites Vorkommen von xVorkommen gebunden durch Allquantor am Anfang
achtes Zeichenerstes Vorkommen von yfreies Vorkommen
siebzehntes Zeichenzweites Vorkommen von yVorkommen gebunden durch Existenzquantor
also bv(G ) = {x, y} und fv(G ) = {y}
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 32 / 63
freie und gebundene Vorkommen vonVariablensymbolen
Beispiel x( R(x,y) > y R(x,y))sechstes Zeichen
erstes Vorkommen von xVorkommen gebunden durch Allquantor am Anfang
fünfzehntes Zeichenzweites Vorkommen von xVorkommen gebunden durch Allquantor am Anfang
achtes Zeichenerstes Vorkommen von yfreies Vorkommen
siebzehntes Zeichenzweites Vorkommen von yVorkommen gebunden durch Existenzquantor
also bv(G ) = {x, y} und fv(G ) = {y}
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 32 / 63
freie und gebundene Vorkommen vonVariablensymbolen
Beispiel x( R(x,y) > y R(x,y))sechstes Zeichen
erstes Vorkommen von xVorkommen gebunden durch Allquantor am Anfang
fünfzehntes Zeichenzweites Vorkommen von xVorkommen gebunden durch Allquantor am Anfang
achtes Zeichenerstes Vorkommen von yfreies Vorkommen
siebzehntes Zeichenzweites Vorkommen von yVorkommen gebunden durch Existenzquantor
also bv(G ) = {x, y} und fv(G ) = {y}
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 32 / 63
SubstitutionenSubstitution: Abbildung σ : VarPL → LTer
falls σ durch Menge S der Paare S = { xi j /σ (xi j ) | 1 ≤ j ≤ k }eindeutig bestimmtalso insbesondere S rechtseindeutigschreibe σS = σ { xij /σ (xij ) | 1≤j≤k }.
Beispiel: σ {x/c,y/f(x)} Abbildung mit
σ (x) = c
σ (y) = f(x)
σ (z) = z für jedes z < {x, y}
Erweiterung auf Terme und Formeln
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 33 / 63
Substitutionen — erweitert auf Termeerweitere σS zu σ ′S : LTer → LTer ,
σ ′S (t ) =
σS (x ), falls t = x ∈ VarPLc, falls t = c ∈ ConstPLf(σ ′S (t1), . . . ,σ
′S (tk )) falls t = f(t1, . . . , tk)
mit f ∈ FunPL , t1, . . . , tk ∈ LTer
schreibe sta� σ ′S wieder σS
Beispiele: σ {x/c,y/f(x)} (x) = c
σ {x/c,y/f(x)} (y) = f(x)
σ {x/c,y/f(x)} (g(y,x)) = g(f(x),c)
σ {x/c,y/f(x)} (f(z,z)) = f(z,z)
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 34 / 63
Substitutionen — erweitert auf Termeerweitere σS zu σ ′S : LTer → LTer ,
σ ′S (t ) =
σS (x ), falls t = x ∈ VarPLc, falls t = c ∈ ConstPLf(σ ′S (t1), . . . ,σ
′S (tk )) falls t = f(t1, . . . , tk)
mit f ∈ FunPL , t1, . . . , tk ∈ LTer
schreibe sta� σ ′S wieder σS
Achtung:σ {x/y,y/x} (f(x, y)) = f(σ {x/y,y/x} (x),σ {x/y,y/x} (y))
= f(y, x)
aber σ {x/y} (σ {y/x} (f(x, y)) = f(y, y)
Alle Variablen werden „gleichzeitig substituiert“!GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 34 / 63
Substitutionen — erweitert auf nicht quantifizierteFormeln
erweitere σS zu σ ′′S : LFor → LFor ,
σ ′′S (G ) =
R(σ ′S (t1), . . . ,σ′S (tk )), falls G = R(t1, . . . , tk)∈ LRel
σ ′S (t1) =̇σ′S (t2), falls G = t1 =̇ t2 mit t1, t2 ∈ LTer
σ ′′S (H ), falls G = H
σ ′′S (H1) > σ ′′S (H2), falls G = H1 > H2
σ ′′S (H1) < σ ′′S (H2), falls G = H1 < H2
σ ′′S (H1) σ ′′S (H2), falls G = H1 H2
schreibe sta� σ ′′S wieder σS
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 35 / 63
Substitutionen — erweitert auf quantifizierte Formelnzu σS und x ∈ VarPL definiere Substitution σS−x :
σS−x (x ) = x
σS−x (y) = σS (y) für jedes y ∈ VarPL mit y , x
Beispielfür σ = σ {x/c,y/x}ist σ−x = σ {x/c,y/x}−x = σ {y/x}
definiere σ ′′S ( x H ) = x σ ′′S−x (H )
σ ′′S ( x H ) = x σ ′′S−x (H )
gebundene Variablenvorkommen werden nicht substituiert
schreibe sta� σ ′′S wieder σSGBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 36 / 63
Substitutionen — Beispiel für eine quantifizierte FormelBeispiel G = S(x) > x R(x,y).
für jedes σ ist σ (G ) = σ (S(x) > x R(x,y))
= σ (S(x)) > σ ( x R(x,y))
= S(σ (x)) > x σ−x (R(x,y))
= S(σ (x)) > x R(σ−x (x),σ−x (y))
konkret z. B. σ = σ {x/c,y/f(x)}, also σ−x = σ {y/f(x)}
alsoσ (G ) = S(σ (x)) > x R(σ−x (x),σ−x (y))
= S(σ {x/c,y/f(x)} (x)) > x R(σ {y/f(x)} (x),σ {y/f(x)} (y))
= S(c) > x R(x,f(x))
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 37 / 63
Kollisionsfreie Substitutionen für FormelnSubstitution σ für Formel G kollisionsfrei, wenn gilt:
wennσ (xi ) , xi undxj in σ (xi ) vorkommt,
dannjedes freie Vorkommen von xi in Gnicht im Wirkungsbereich eines �antors xj oder xj
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 38 / 63
Logisch äquivalente FormelnFormeln G und H logisch äquivalent, wenn
für jede passende Interpretation (D, I ) undjede passende Variablenbelegung β
gilt:valD, I,β (G ) = valD, I,β (H )
Satz. WennG und H logisch äquivalent,Formel F enthält G als Teilformel undFormel F ′ entsteht aus F durch Ersetzen von G durch H
dannist F logisch äquivalent F ′.
Lemma. Wenn G und H logisch äquivalent sind,dann ist G H allgemeingültig.
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 39 / 63
Logisch äquivalente Formeln — Beispiele (1)G,H ∈ LFor , xi , xj ∈ VarPL
xi G und xi Gxi G und xi G
xi xj G und xj xi Gxi xj G und xj xi G
xi(G > H)und xi G > xi Hxi(G < H)und xi G < xi H
wenn xj < fv(G ) und σ {xi /xj } kollisionsfrei für G,dann sind äquivalent
xi G und x j σ {xi /xj } (G )
xi G und x j σ {xi /xj } (G )
gebundene Umbenennung der Variable
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 40 / 63
Logisch äquivalente Formeln — Beispiele (2)G,H ∈ LFor , xi , xj ∈ VarPL
wenn xi < fv(G ), dann sind äquivalentG > xi H und xi(G > H)G > xi H und xi(G > H)
G < xi H und xi(G < H)G < xi H und xi(G < H)
G xi H und xi(G H)G xi H und xi(G H)
wenn xi < fv(H ), dann sind äquivalent( xi G) H und xi(G H)( xi G) H und xi(G H)
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 41 / 63
Weitere allgemeingültige Formeln (1)G,H ∈ LFor , xi , xj ∈ VarPL
wenn Substitution σ {xi /t } kollisionsfrei für G ist, dann
( xi G) σ {xi /t } (G )
allgemeingültig
wenn xi < fv(G ), dann
xi(G H) (G xi H)
allgemeingültig
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 42 / 63
Weitere allgemeingültige Formeln (2)G,H ∈ LFor
Für xi , xj , xk ∈ VarPL sindxi =̇ xixi =̇ xj xj =̇ xixi =̇ xj (xj =̇ xk xi =̇ xk)
allgemeingültig.
Für jedes k ∈ N+ gilt:Wenn x1, . . . ,xk ∈ VarPL und y1, . . . ,yk ∈ VarPL ,fi ein k-stelliges Funktionssymbol undRi ein k-stelliges Relationssymbol, dann sind
x1 =̇y1 (x2 =̇y2 ( · · ·(xk =̇yk fi(x1, . . . ,xk)=̇ fi(y1, . . . ,yk))· · · ))x1 =̇y1 (x2 =̇y2 ( · · ·(xk =̇yk (Ri(x1, . . . ,xk) Ri(y1, . . . ,yk)))· · · ))
allgemeingültig.
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 43 / 63
Wo sind wir?
Syntax prädikatenlogischer Formeln
Semantik prädikatenenlogischer Formeln
Freie und gebundene Variablenvorkommen und Substitutionen
Beweisbarkeit
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 44 / 63
KalküleFormeln
Axiome
Ableitungsregeln
Theoreme
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 45 / 63
Hilbert-Kalkül — für Prädikatenlogik erster StufeAlphabet AFor
Variablen-, Konstanten-, Funktions-, Relationssymbole
Formelmenge LFor
Axiomenmenge AxPL ⊆ LFor (kommt gleich)
SchlussregelnModus ponensGeneralisierung (kommt gleich)
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 46 / 63
Axiome für Hilbert-Kalkül — alle allgemeingültig (1)
AxAL1 ={(G (H G)) ��� G,H ∈ LFor
}
AxAL2 ={(G (H K)) ((G H) (G K))��� G,H ,K ∈ LFor
}
AxAL3 ={( H G) (( H G) H) ��� G,H ∈ LFor
}
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 47 / 63
Axiome für Hilbert-Kalkül — alle allgemeingültig (2)
AxPL1 ={( xi G) σ {xi /t } (G ) ��� G ∈ LFor , xi ∈ VarPL, t ∈ LTer
und σ {xi /t } kollisionsfrei für G}
AxPL2 ={( xi(G H)) (G xi H)��� G,H ∈ LFor , xi ∈ VarPL, und xi < fv(G )
}
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 48 / 63
Axiome für Hilbert-Kalkül — alle allgemeingültig (3)
AxEq 1 ={xi =̇ xi
��� xi ∈ VarPL}
AxEq2 ={xi =̇ xj xj =̇ xi
��� xi , xj ∈ VarPL}
AxEq3 ={xi =̇ xj (xj =̇ xk xi =̇ xk)
��� xi , xj , xk ∈ VarPL}
AxEq4 ={xi1 =̇ xj1 (xi2 =̇ xj2 ( · · ·(xin =̇ xjn
fi(xi1, . . . ,xin)=̇ fi(xj1, . . . ,xjn))· · · ))��� xi1 , · · · , xin , xj1 , · · · , xjn ∈ VarPL, fi ∈ FunPL
}
AxEq5 ={xi1 =̇ xj1 (xi2 =̇ xj2 ( · · ·(xin =̇ xjn
(Ri(xi1, . . . ,xin) Ri(xj1, . . . ,xjn)))· · · ))��� xi1 , · · · , xin , xj1 , · · · , xjn ∈ VarPL, Ri ∈ RelPL
}
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 49 / 63
Schlussregeln für den Hilbert-Kalkül
Modus ponens MP ⊆ L3ForMP = {(G H ,G,H ) | G,H ∈ LFor }
G H G
H
Generalisierung GEN ⊆ L2ForGEN = {(G,( xi G)) | G ∈ LFor und xi ∈ VarPL }
G
( xi G)
beide Schlussregeln erhalten Allgemeingültigkeit
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 50 / 63
Ableitungen — formal gefasstAbleitungen nutzen Prämissen, Axiome und Schlussregeln
Γ ⊆ ForAL Hypothesen oder Prämissen undG eine Formel
Ableitung von G aus Γendliche Folge (G1, . . . ,Gn ) von Formeln mitGn = G (oder weiter vorne) undfür jedes Gi tri�t einer der folgenden Fälle zu:
Axiom Gi ∈ AxAL ,Prämisse Gi ∈ Γes gibt Indizes i1 und i2 echt kleiner i , für die gilt:(Gi1 ,Gi2 ,Gi ) ∈ MP .es gibt Index i1 echt kleiner i , für den gilt: (Gi1 ,Gi ) ∈ GEN .
einziger Unterschied zur Aussagenlogik
geschrieben Γ ` G
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 51 / 63
Ableitungen — formal gefasstAbleitungen nutzen Prämissen, Axiome und Schlussregeln
Γ ⊆ ForAL Hypothesen oder Prämissen undG eine Formel
Ableitung von G aus Γendliche Folge (G1, . . . ,Gn ) von Formeln mitGn = G (oder weiter vorne) undfür jedes Gi tri�t einer der folgenden Fälle zu:
Axiom Gi ∈ AxAL ,Prämisse Gi ∈ Γes gibt Indizes i1 und i2 echt kleiner i , für die gilt:(Gi1 ,Gi2 ,Gi ) ∈ MP .es gibt Index i1 echt kleiner i , für den gilt: (Gi1 ,Gi ) ∈ GEN .
einziger Unterschied zur Aussagenlogik
geschrieben Γ ` G
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 51 / 63
Beweis — formal gefasstBeweis von G: Ableitung aus Γ = {}
geschrieben ` GG heißt Theorem des Kalküls
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 52 / 63
Hilbert-Kalkül — korrekt und vollständigSatz.Für jede Formelmenge Γ ⊆ LFor und jedes G ∈ LFor gilt:
wenn Γ ` G, dann auch Γ |= G .
Der Hilbert-Kalkül ist korrekt.
Satz.Für jede Formelmenge Γ ⊆ LFor und jedes G ∈ LFor gilt:
wenn Γ |= G, dann auch Γ ` G .
Der Hilbert-Kalkül ist vollständig.
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 53 / 63
Deduktionstheorem — aber nur mit EinschränkungenSatz.Für geschlossene Formel G ∈ LFor und jede H ∈ LFor gilt
G ` H genau dann, wenn `(G H)
gilt.
es gibt schwächere hinreichende Voraussetzungen
aber falsch für beliebige G und G ` H
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 54 / 63
Skizze eines Beispielses sei
FunPL = {f}ConstPL = {c}Γ = { x(f(c,x)=̇ x > f(x,c)=̇ x) }.
Modell (D, I ) von Γ
besitzt zweistellige Operation I (f) auf Deine Konstante I (c), die neutrales Element bezüglich I (f) ist.
BeispieleD = N0, I (f) : N0 × N0 → N0 : (x ,y) 7→ x + y und I (c) = 0,
D = {a,b}∗,I (f) : {a,b}∗ × {a,b}∗ → {a,b}∗ : (w1,w2) 7→ w1 ·w2 undI (c) = ε .
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 55 / 63
Skizze eines Beispielses sei
FunPL = {f}ConstPL = {c}Γ = { x(f(c,x)=̇ x > f(x,c)=̇ x) }.
Modell (D, I ) von Γ
besitzt zweistellige Operation I (f) auf Deine Konstante I (c), die neutrales Element bezüglich I (f) ist.
BeispieleD = N0, I (f) : N0 × N0 → N0 : (x ,y) 7→ x + y und I (c) = 0,
D = {a,b}∗,I (f) : {a,b}∗ × {a,b}∗ → {a,b}∗ : (w1,w2) 7→ w1 ·w2 undI (c) = ε .
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 55 / 63
Skizze eines Beispielses sei
FunPL = {f}ConstPL = {c}Γ = { x(f(c,x)=̇ x > f(x,c)=̇ x) }.
Modell (D, I ) von Γ
besitzt zweistellige Operation I (f) auf Deine Konstante I (c), die neutrales Element bezüglich I (f) ist.
BeispieleD = N0, I (f) : N0 × N0 → N0 : (x ,y) 7→ x + y und I (c) = 0,D = {a,b}∗,I (f) : {a,b}∗ × {a,b}∗ → {a,b}∗ : (w1,w2) 7→ w1 ·w2 undI (c) = ε .
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 55 / 63
Skizze eines Beispiels (2)Ziel: neutrales Element immer eindeutig
in jedem Modell von Γ ist Formel G
y( x(f(y,x)=̇ x > f(x,y)=̇ x) y =̇ c)
wahr.
Weg:zeige Γ ` Gdann auch Γ |= G (Hilbert-Kalkül korrekt)
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 56 / 63
Skizze eines Beispiels (3)Kern der Argumentation
y = f (c,y) weil c (links)neutral
= c weil y (rechtbs)neutral
Übertragung in Hilbert-Kalkülprinzipiell möglichsehr mühsambeschränken uns auf Skizze
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 57 / 63
Skizze eines Beispiels (4)grobe Vorgehensweise in fünf Schri�en
Schri� 0: Ziel: für „beliebiges“ y giltx(f(y,x)=̇ x > f(x,y)=̇ x) y =̇ c
Schri� 1: zeige: y =̇ f(c,y)
Schri� 2: zeige: x(f(y,x)=̇ x > f(x,y)=̇ x) y =̇ f(c,y)
Schri� 3: zeige: x(f(y,x)=̇ x > f(x,y)=̇ x) f(c,y)=̇ c
Schri� 4: zeige x(f(y,x)=̇ x > f(x,y)=̇ x) y =̇ c
Schri� 5: von Schri� 4 durch Generalisierung zu:y( x(f(y,x)=̇ x > f(x,y)=̇ x) y =̇ c)
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 58 / 63
Skizze eines Beispiels (5)Schri� 1: zeige: y =̇ f(c,y)
Schri� 1.1: wegen x(f(c,x)=̇ x > f(x,c)=̇ x)giltinsbesonderef(c,y)=̇ y > f(y,c)=̇ y
Schri� 1.2: Also gilt f(c,y)=̇ y.Schri� 1.3: Also gilt y =̇ f(c,y).
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 59 / 63
Skizze eines Beispiels (6)Schri� 2: zeige: x(f(y,x)=̇ x > f(x,y)=̇ x) y =̇ f(c,y)
Schri� 1: y =̇ f(c,y)nutze Tautologieschema G (H G)
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 60 / 63
Skizze eines Beispiels (7)Schri� 3: zeige:x(f(y,x)=̇ x > f(x,y)=̇ x) f(c,y)=̇ c
Schri� 3.1: zeige x(f(y,x)=̇ x > f(x,y)=̇ x)x(f(y,x)=̇ x) > x(f(x,y)=̇ x)
Schri� 3.2: zeige x(f(y,x)=̇ x) > x(f(x,y)=̇ x)x(f(x,y)=̇ x)
Schri� 3.3: also x(f(y,x)=̇ x > f(x,y)=̇ x) x(f(x,y)=̇ x)
Schri� 3.4: zeige x(f(x,y)=̇ x) f(c,y)=̇ c
Schri� 3.5: also x(f(y,x)=̇ x > f(x,y)=̇ x) f(c,y)=̇ c
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 61 / 63
Skizze eines Beispiels (8)Schri� 4: zeige x(f(y,x)=̇ x > f(x,y)=̇ x) y =̇ c
Schri� 4.1 mit Ergebnissen von Schri� 2 und Schri� 3 zeige:x(f(y,x)=̇ x > f(x,y)=̇ x) (y =̇ f(c,y) > f(c,y)=̇ c)
Schri� 4.2: zeige(y =̇ f(c,y) > f(c,y)=̇ c) y =̇ c
Schri� 4.3: also x(f(y,x)=̇ x > f(x,y)=̇ x) y =̇ c
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 62 / 63
ZusammenfassungSyntax prädikatenlogischer Formeln
Terme, atomare Formeln, Formeln
SemantikInterpretationen und VariablenbelegungenModelle von Formel(menge)n oder nichtAllgemeingültigkeit
KalküleBeweisbarkeitHilbert-Kalkül korrekt und vollständig
GBI — Grundbegri�e der Informatik KIT, Institut für Theoretische Informatik 63 / 63