Was bisher geschah

Was bisher geschah
Syntax:
Signatur Σ = (ΣF , ΣR )
Menge X von
Terme Term(Σ, X )
Grundterme Term(Σ, ∅)
Semantik:
Σ-Struktur A = (A, ·
A ):
nichtleere Trägermenge A
für jedes (f , n) ∈ ΣF eine Funktion f A : An → A
für jedes (R, n) ∈ ΣF eine Relation R A ⊆ An
Σ-Interpretation (A, α) mit Σ-Struktur A = (A, ·
Belegung der Individuenvariablen α : X → A
A)
und
Wert t A des Termes t ∈ Term(Σ, X ) in einer
Σ-Interpretation (A, α)
Äquivalenz von Grundtermen s, t ∈ Term(Σ, ∅) in einer
Struktur A: s ≡A t gdw. s A = t A
Wiederholung: Terme (mit Variablen) – Semantik
Signatur Σ = (ΣF , ΣR ), Variablenmenge X
Menge Term(ΣF , X ) aller Terme mit Variablen aus X
Σ-Interpretation (A, α) mit
Σ-Struktur A = (A, ·
A)
Belegung der Individuenvariablen α : X → A
Wert des ΣF -Termes t = f (t1 , . . . , tn ) ∈ Term(ΣF , X ) in der
Interpretation (A, α):
IA: für t = x mit x ∈ X : t
(A,α)
= α(x)
IS: für t = f (t1 , . . . , tn ): t (A,α) = f A t1 (A,α) , . . . , tn
(Spezialfall t = c mit (c, 0) ∈ ΣF : t (A,α) = c A )
Wert eines Termes in einer Interpretation ((A, ·
Element aus A.
A ), α)
(A,α)
ist ein
Wert von Grundtermen in einer Interpretation (A, α) hängt nicht
von der Belegung α ab.
Beispiel
Signatur Σ = (ΣF , ΣR ) mit
ΣF = {(a, 0), (b, 0), (f , 1), (g, 2), (h, 2)} und ΣR = ∅
Variablenmenge X = {x, y }
Σ-Struktur S = (S, · S ) mit
S =
f
g
◆
a
S
= 5
b
S
= 3
S (a)
= 1+a
S (a, b)
= a+b
h S (a, b) = a · b
Variablenbelegungen
β : {x, y } →
γ : {x, y } →
◆ mit β(x) = 0, β(y ) = 1
◆ mit γ(x) = 2, γ(y ) = 0
Terme s = g(h(f (a), x), h(x, y )) und t = h(f (x), g(y , a))
s (S,β) , t (S,β) , s (S,γ) , t (S,γ) (Tafel)
Atome – Syntax
Atom elementare Formel,
repräsentiert Eigenschaften von oder
Beziehungen zwischen Objekten
Signatur Σ = (ΣF , ΣR ) mit
Menge ΣF von Funktionssymbolen mit Stelligkeit (f , n)
Menge ΣR von Relationssymbolen mit Stelligkeit (R, n)
Menge aller Σ-Atome mit Variablen aus Menge X :
Atom(Σ, X ) = {R(t1 , . . . , tn ) | (R, n) ∈ ΣR und t1 , . . . , tn ∈ Term(ΣF , X )}
Atome ohne Individuenvariablen heißen Grundatome.
Menge aller Grundatome: Atom(Σ, ∅)
Atome – Beispiele
Signatur Σ = (ΣF , ΣR√) mit
ΣF = {(1, 0), (2, 0), ( , 1), (+, 2)}
ΣR = {(=, 2), (≤, 2)}
Variablenmenge X = {x, y , z}
√
√x = 2 ∈ Atom(Σ, X )
√
x + 2 ∈ Atom(Σ, X ) (aber x + 2 ∈ Term(ΣF , X ))
√
√
1+ 2≤
2 ∈ Atom(Σ, X )
Signatur Σ = (ΣF , ΣR ) mit
ΣF = {(a, 0), (b, 0), (k , 2), (d, 2)}
ΣR = {(P, 1), (Q, 2)}
Variablenmenge X = {x, y }
y ∈ Atom(Σ, X )
P(a) ∈ Atom(Σ, X )
P(Q(P(a), k (x, y ))) ∈ Atom(Σ, X )
Q(k (a, a), x) ∈ Atom(Σ, X )
Atome – Semantik
Signatur Σ = (ΣF , ΣR ), Variablenmenge X
Menge Atom(Σ, X ) aller Atome mit Variablen aus X
Σ-Interpretation (A, α) mit
Σ-Struktur A = (A, ·
A)
Belegung der Individuenvariablen α : X → A
Wert des Atomes a = P(t1 , . . . , tn ) ∈ Atom(Σ, X ) in der
Interpretation (A, α):
a
(A,α)
= P(t1 , . . . , tn )
(A,α)
= P
A
(Spezialfall Atom a mit (a, 0) ∈ ΣF : a
t1
(A,α)
(A,α) , . . . ,
= a
Wert eines Atomes in einer Interpretation ((A, ·
Wahrheitswert.
tn
(A,α)
A)
A ), α)
ist ein
Wert von Grundatomen in einer Interpretation (A, α) hängt
nicht von der Belegung α ab.
Semantik von Atomen – Beispiele
Signatur Σ = (ΣF , ΣR ) mit
ΣF = {(a, 0), (f , 1)}
ΣR = {(P, 1), (R, 2)}
X = {x, y }
Σ-Struktur S = (S, · S ) mit
S = {0, 1, 2}
a
f
S
S (d)
= 1
= 2−d
P
S
= {0, 2}
R
S
= {(1, 0), (1, 2), (2, 2)}
Belegung β : {x, y } → {0, 1, 2}: β(x) = 0, β(y ) = 1
Wert von Atomen aus Atom(Σ, X ) in Interpretation (S, β):
P(a) (S,β) , P(x) (S,β) , P(f (x)) (S,β) , P(f (f (x))) (S,β) ,
R(x, a) (S,β) , R(f (y ), x) (S,β) (Tafel)
Prädikatenlogik (der ersten Stufe) – Syntax
aussagenlogische Junktoren t, f, ¬, ∨, ∧, →, ↔
neu: Σ-Atome, Quantoren ∀, ∃
Definition (induktiv)
Die Menge FO(Σ, X ) aller Formeln der Prädikatenlogik (der
ersten Stufe) über der Signatur Σ mit (Individuen-)Variablen
aus der Menge X ist definiert durch:
IA: Atom(Σ, X ) ⊆ FO(Σ, X )
(alle Atome sind Formeln)
IS:
Aus {ϕ1 , . . . , ϕn } ⊆ FO(Σ, X ) folgt für jeden
n-stelligen Junktor ∗:
∗(ϕ1 , . . . , ϕn ) ∈ FO(Σ, X )
Aus ϕ ∈ FO(Σ, X ) und x ∈ X folgt
{∀xϕ, ∃xϕ} ⊆ FO(Σ, X )
(Baumstruktur, analog zur Definition von Termen)
Beispiele
Σ = (ΣF , ΣR ) mit
ΣF = {(a, 0), (f , 1)}
ΣR = {(P, 1), (R, 2)}
X = {x, y }
Formeln aus FO(Σ, X ):
ϕ1 = P(f (x))
ϕ3 = (P(x) ↔ (¬P(f (x)) ∧ (∀x∃y ((P(x) ↔ P(y )) ∧ R(x, y )))))
ϕ4 = ∀x∀y ϕ3
Σ = (∅, ΣR ) mit ΣR = {(p, 0), (q, 0)}
Formeln aus FO(Σ, ∅):
ψ1 = p ∨ q
ψ2 = ¬p ∨ ¬(q ∨ p)
(Spezialfall: Syntax der Aussagenlogik)
Variablen in Formeln
Vorkommen einer Individuenvariablen x ∈ X in
Term t, falls t = x oder t = f (t1 , . . . , tn ) und x in einem ti
vorkommt
Atom a = p(t1 , . . . , tn ), falls x in einem ti vorkommt
Formel ϕ, falls x in einem Atom in ϕ
(Teilformel von ϕ, die Atom ist) vorkommt.
var(ϕ) Menge aller in ϕ vorkommenden Indiviuenvariablen
Vorkommen der Indiviuenvariablen x in ϕ heißt
gebunden , falls x in einer Teilformel von ϕ der Form ∃xψ
oder ∀xψ vorkommt,
bvar(ϕ) Menge aller gebundenen Variablen in ϕ
freie , sonst
fvar(ϕ) Menge aller freien Variablen in ϕ
var(ϕ) = fvar(ϕ) ∪ bvar(ϕ) gilt immer.
fvar(ϕ) ∩ bvar(ϕ) = ∅ ist möglich.
Beispiele
ϕ1 = R(x, a)
ϕ2 = ∃xR(x, f (y , x))
bvar(ϕ1 ) = ∅, fvar(ϕ1 ) = {x}
bvar(ϕ2 ) = {x}, fvar(ϕ2 ) = {y }
ϕ3 = (P(x) ↔ (¬P(f (x)) ∧ (∀x∃y ((P(x) ↔ P(y )) ∧ R(x, y )))))
bvar(ϕ3 ) = {x, y }, fvar(ϕ3 ) = {x}
ϕ4 = ∀x∀y ϕ3
bvar(ϕ4 ) = {x, y }, fvar(ϕ4 ) = ∅
Sätze
Formel ϕ ∈ FO(Σ, X ) mit fvar(ϕ) = ∅ heißt Satz.
Beispiele:
∀x∀y (R(x, y ) → R(y , x)) ist ein Satz.
R(x, y ) → R(y , x), ∀x(R(x, y ) → R(y , x)),
∃y (R(x, y ) → R(y , x)), ∀x(R(x, y ) → ∀yR(y , x))
sind keine Sätze.
für ϕ ∈ FO(Σ, X ) mit fvar(ϕ) = {x1 , . . . , xn }:
universeller Abschluß ∀ϕ := ∀x1 · · · ∀xn ϕ
existentieller Abschluß ∃ϕ := ∃x1 · · · ∃xn ϕ
Fakt
Für jede Formel ϕ ∈ FO(Σ, X ) sind ∀ϕ und ∃ϕ Sätze.
Modifizierte Interpretationen
Signature Σ, Variablenmenge X
Σ-Struktur S = (S, · S )
Belegung β : X −→ S der Variablen aus X in S
modifizierte Belegung β[x → a] : X −→ S mit
β[x → a](y ) =
a
für y = x
β(y ) sonst
Σ-Interpretation (S, β) mit
Σ-Struktur S = (S, · S )
Variablenbelegung β : X −→ S
modifizierte Interpretation (S, β[x → a])
Wert in Interpretationen
Wert in Σ-Interpretation (S, β) mit S = (S, · S )
einer Individuenvariable x ∈ X : x
(S,β)
= β(x) ∈ S
eines Termes t = f (t1 , . . . , tn ) ∈ Term(ΣF , X ):
t (S,β) = f S t1 (S,β) , . . . , tn (S,β) ∈ S
eines Atomes a = p(t1 , . . . , tn ) ∈ Atom(Σ, X ):
a (S,β) = p S ( t1 (S,β) , . . . , tn (S,β) ) ∈ {0, 1}
einer Formel ϕ ∈ FO(Σ, X ): ϕ
¬ϕ
(S,β)
(S,β)
= 1− ϕ
ϕ∨ψ
(S,β)
= max( ϕ
ϕ∧ψ
(S,β)
= min( ϕ
∃xϕ
(S,β)
= max{ ϕ
∀xϕ
(S,β)
= min{ ϕ
∈ {0, 1}
(S,β)
(S,β) ,
(S,β) ,
ψ
ψ
(S,β) )
(S,β) )
(S,β[x→a])
(S,β[x→a])
| a ∈ S}
| a ∈ S}
Beispiele
Σ = (ΣR , ΣF ) mit ΣF = {(f , 1)},ΣR = {(R, 2)}, X = {x, y , z}
ϕ = ¬R(x, y ) ∧ ∃zR(z, z)
ψ = ∀x∃yR(x, f (y ))
Σ-Struktur A = (A, · A ) mit A = {a, b, c}
f A (a) = f A (b) = c, f A (c) = a
R A = {(a, a), (b, a), (a, c)}
Belegung α(x) = b, α(y ) = a , α(z) = b
ϕ (A,α) =
ψ (A,α) =
❩
Σ-Struktur B = (B, · B ) mit B =
f B (d) = −d, R B =≤
Belegung β(x) = 5, β(y ) = 3, β(z) = −1,
ϕ (B,β) =
ψ (B,β) =
Modelle für Formeln
(analog zu Aussagenlogik)
Σ-Interpretation (S, β) erfüllt (ist Modell für) die Formel
ϕ ∈ FO(Σ, X ) genau dann, wenn ϕ (S,β) = 1.
Menge aller Modelle der Formel ϕ ∈ FO(Σ, X )
Mod(ϕ) =
(S, β)
(S, β) ist Σ-Interpretation und
ϕ (S,β) = 1
(Menge von Σ-Interpretationen)
Erfüllbarkeit und Allgemeingültigkeit
(analog zu Aussagenlogik)
Formel ϕ ∈ FO(Σ, X ) heißt
erfüllbar gdw. Mod(ϕ) = ∅
(z.B. ∀x (P(x) ∨ Q(x)))
unerfüllbar gdw. Mod(ϕ) = ∅
(z.B. ∀xP(x) ∧ ∃x¬P(x) )
allgemeingültig gdw.
Mod(ϕ) = {(S, β) | S = (S, · S ) ist Σ-Struktur, β : X → S}
(Menge aller Σ-Interpretationen)
(z.B. ∀x¬P(x) ∨ ∃xP(x))
Beispiele
ϕ = R(x) ∧ ∃y ((¬R(y )) ∧ E(y , x))
Struktur G = ({1, 2, 3, 4}, · G ) mit
R G = {1, 2, 4},
E G = {(1, 2), (3, 2)} und
Belegung β : {x, y } −→ {1, . . . , 4} mit β(x) = 2, β(y ) = 2
(G, β) ist Modell für ϕ
Struktur H = ({a, b}, · H ) mit
R H = {a},
E H = {(a, a), (b, b)},
Belegung β : {x, y } −→ {a, b} mit β(x) = a, β(y ) = a
(H, β) ist kein Modell für ϕ
Struktur J = ( , · J ) mit
R J = 2 (Menge aller geraden Zahlen),
E J = {(i, i + 1) | i ∈ } und
Belegung β : {x, y } −→ mit β(x) = β(y ) = 0
(J , β) ist Modell für ϕ
❩
❩
❩
❩
Semantische Folgerung und Äquivalenz
(analog Aussagenlogik)
Für Φ ⊆ FO(Σ, X ) und ψ ∈ FO(Σ, X ) gilt
Φ |= ψ
gdw.
Mod(Φ) ⊆ Mod(ψ)
Beispiel:{∀x(P(x) ∨ Q(x)), ¬(P(x))} |= Q(x)
Für ϕ, ψ ∈ FO(Σ, X ) gilt
ϕ≡ψ
gdw.
Beispiel: ¬∀xP(x) ≡ ∃x¬P(x)
Mod(ϕ) = Mod(ψ)
Wichtige Äquivalenzen mit Quantoren
¬∀xϕ ≡ ∃x¬ϕ
¬∃xϕ ≡ ∀x¬ϕ
∀xϕ ∧ ∀xψ ≡ ∀x(ϕ ∧ ψ)
∃xϕ ∨ ∃xψ ≡ ∃x(ϕ ∨ ψ)
∀x∀y ϕ = ∀y ∀xϕ
∃x∃y ϕ = ∃y ∃xϕ
für x ∈ fvar(ψ) und ∗ ∈ {∨, ∧} gilt außerdem
∀xϕ ∨ ψ ≡ ∀x(ϕ ∨ ψ)
∃xϕ ∨ ψ ≡ ∃x(ϕ ∨ ψ)
∀xϕ ∧ ψ ≡ ∀x(ϕ ∧ ψ)
∃xϕ ∧ ψ ≡ ∃x(ϕ ∧ ψ)

Download Report