Logische Äquivalenz
Definition 2.7 [Logische Äquivalenz] |
Zwei Formeln φ, ψ ∈ FO(S) heißen (logisch) äquivalent, gdw. für alle S-Interpretationen J gilt: J |= φ gdw. J |=ψ. In Symbolen: φ≡ψ. |
Bem.: Logische Äquivalenzen der AL übertragen sich auf FO. Hinzu treten charakteristische logische Äquivalenzen im Zusammenhang mit Quantoren.
Z.B. die Dualität zwischen ∀ und ∃, die besagt dass für alle φ ∈ FO(S):
∃xφ ≡ ¬∀x¬φ,
∀xφ ≡ ¬∃x¬φ.
Erfüllbarkeitsäquivalenz
Definition 2.10 Erfüllbarkeitsäquivalenz |
Formeln φ,φ′ heißen erfülbarkeitsäquivalent wenn gilt: φ erfüllbar gdw. φ′ erfülbar. Analog wird Erfüllbarkeitsäquivalenz für Formelmengen definiert. |
Signaturen
Eine Signatur S ist eine Menge von Konstanten-, Funktions- und Relationssymbolen, mit angegebenen Stelligkeiten. Spezialfa ̈lle: S ohne Funktionssymbole : relationale Signatur; S ohne Relationssymbole : funktionale Signatur. |
S-Strukturen
Definition 1.1 [S-Strukturen] |
Für Signatur S: Eine S-Struktur A = (A,cA,...,fA,...,RA,...) besteht aus ihrer Trägermenge A ≠ ∅ zusammen mit einer Interpretation der Symbole in S, d.h., für jedes Konstantensymbol c ∈ S: ein ausgezeichnetes Element cA ∈ A. für jedes n-stellige Funktionssymbol f ∈ S: eine n-stellige Funktion fA : An→ A. für jedes n-stellige Relationssymbol R ∈ S: eine n-stellige Relation RA ⊆ An. |
S-Terme
Definition 1.3 [S-Terme] Die Menge der S-Terme, T(S) (mit Variablenmenge V) ist induktiv erzeugt wie folgt:
• x∈T(S) für jede Variable x ∈ V.
• c ∈ T(S) für jedes Konstantensymbol c ∈ S.
• ist f ∈ S ein n-stelliges Funktionssymbol, und sind t 1
, . . . , t n
∈ T (S), so ist auch ft 1
...t n
∈T(S).
T n
(S) ⊆ T(S): die Mengen der Terme, in denen nur Variablensymbole aus V n
= {x 1
, . . . , x n
} vorkommen.
Speziell steht T0 (S) für die Menge der Variablen-freien Terme (= ∅ wenn S keine Konstanten hat). |
Allgemeingültigkeit
Definition 2.6 [Allgemeingültigkeit] |
Eine Formel φ ∈ FO(S) heißt allgemeingültig gdw. für alle S-Interpretationen J gilt: J |= φ. |
|
|
Folgerungsbeziehung
Definition 2.5 [Folgerungsbeziehung] |
φ |= ψ bzw. Φ |= ψ. |
Für φ,ψ ∈ FO(S):
ψ ist eine logische Folgerung von φ, oder ψ folgt aus φ, in Symbolen φ |= ψ, gdw. für alle S-Interpretationen J gilt: J |= φ ⇒ J |= ψ.
Entsprechend ist Φ |= ψ für Formelmengen Φ definiert (ψ folgt aus Φ).
FO mit und ohne Gleichheit
Definition 2.11 [FO ohne Gleichheit] |
FO≠(S) ⊆ FO(S) ist aufgebaut wie FO aber ohne Termgleichheiten als atomare Formeln. Die Semantik von FO überträgt sich auf die Teillogik FO≠. |
Bemerkung 2.13 Zu jeder Formelmenge Φ ⊆ FO(S) erhält man durch eine systematische Übersetzung in eine explizite Modellierung der Gleichheitsrelation durch eine neues Relationssysmbol ∼ eine erfülbarkeitsäquivalente Formelmenge Φ ∼
⊆ F0 ≠(S ∪ {∼}). |
Termstruktur
Defintion 1.4 Termstrukturen |
Die Menge der S-Terme ist Träger einer S F
-Struktur T = T (S), der Termstruktur ( Herbrand-Struktur) zu S, mit der folgenden natürlichen Interpretation der Konstanten- und Funktionssymbole in S: |
• für Konstantensymbol c ∈ S:
c T := c ∈ T(S).
• für n-stelliges Funktionssymbol f ∈ S: f T: T(S) n → T(S)
(t 1
,...,t n
) → ft 1
...t n
.
Wenn S Konstantensymbole hat, ist auch T 0
(S) Träger einer entsprechenden Termstruktur T 0
(S) (eine Substruktur von T (S)).
Pränexe Normalform
Definition 3.1 [pränexe NF] FO-Formeln in pränexer Normalform sind von der Form Q 1
x i
1
...Q k
x ik
ψ, wo k ∈ N, Q i
∈ {∀, ∃} und ψ quantorenfrei. ψ heißt auch quantorenfreier Kern der Formel, Q 1
x i1
. . . Q k
x i
k
ihr Quantorenpräfix. |
Man braucht i.d.R. zusätzliche Variablensymbole! |
Satz 3.4 Jede FO-Formel ist äquivalent zu einer Formel in pränexer NF. |
Beispiel 3.2 S = {E}, E 2-st. Relations-Symbol. Die folgenden Äquivalenzen liefern auf der rechten Seite pränexe Formalisierungen:
∃y(Exy ∧ ∀x(Eyx → x = y)) ≡ ∃y∀z Exy ∧ (Eyz → z = y) ,
∃y∀xExy ∨ ¬∃yExy ≡ ∃y1∀y2∀y3 Ey2y1 ∨ ¬Exy3 .
|
|
Belegungen
Definition 1.5
[Belegungen und Interpretationen]
Eine Funktion β: V → A heißt Belegung (für die x ∈ V) in der S-Struktur A = (A,...). Eine S-Struktur A und Belegung β zusammen bilden eine S-Interpretation J = (A, β).
•Für t = x ( x ∈ V Variable):
t J:=β(x).
• Für t = c ( c ∈ S Konstantensymbol):
t J:= c A.
• Für t = ft 1
...t n
, mit n-stelligem Funktionssymbol f ∈ S:
t J := f A (t 1 J,...,t n J ). |
Schreibweisen für Belegungen und Interpretationen auf Seite 6 FO Skript über Kapitel 2
Freie Variablen
Definition 2.2 [freie Variablen] |
Induktive Definition der Menge der freien Variablen, frei(φ) ⊆ V, für φ ∈ FO(S): |
Formeln ohne freie Variablen heißen Sätze. |
Schreibweisen: FO n
(S) := {φ ∈ FO(S): frei(φ) ⊆ V n
}. Für φ ∈ FO n
(S) schreiben wir auch φ = φ(x 1
, . . . , x n
) um die möglicherweise freien Variablen explizit anzudeuten. |
frei(t 1
= t 2
) := var(t 1
) ∪ var(t 2
).
frei(Rt 1
. . . t n
) := var(t 1
) ∪ . . . ∪ var(t n
).
frei(¬φ) := frei(φ).
frei(φ ∧ ψ) = frei(φ ∨ ψ) := frei(φ) ∪ frei(ψ).
frei(∃xφ) = frei(∀xφ) := frei(φ) \ {x}.
Quantorenrang
Definition 2.3 [Quantorenrang] |
Induktive Definition des Quantorenrangs, qr(φ) ∈ N, für φ ∈ FO(S): |
Formeln von Quantorenrang 0 heißen quantorenfrei. |
qr(φ) = 0 für atomares φ.
qr(¬φ) := qr(φ).
qr(φ ∧ ψ) = qr(φ ∨ ψ) := max(qr(φ), qr(ψ)).
qr(∃xφ) = qr(∀xφ) := qr(φ) + 1.
Semantik
Definition 2.4 [Semantik] |
Für S-Interpretation J = (A, β) und φ ∈ FO(S): J erfüllt φ gdw. φ J = 1. Schreibweise: J|= φ. |
Für Formelmengen Φ ⊆ AL(V) entsprechend: J|= Φ gdw. J |= φ für alle φ ∈ Φ. |
Die Relation |= heißt Modellbeziehung. |
Herbrand
Satz 3.10 (Herbrand) |
Sei Φ ⊆ FO 0
≠ (S) eine Menge von universellen, gleichheitsfreien Sätzen. Dann sind äquivalent: |
(i) Φ erfüllbar. |
(ii) Φ hat ein Herbrand-Modell H = ( T0 (S), (RH)R ∈S ) |= Φ, dessen Trägermenge und Funktions- und Konstanteninterpretationen mit der Termstruktur T 0
(S) übereinstimmen (H erweitert die S F
-Struktur T 0
(S) lediglich um eine geeignete Interpretation der Relationssymbole in S). |
Definition 3.8 Eine Formel ist universell wenn sie aus atomaren und negiert atomaren Formeln allein mittels ∧, ∨ und ∀-Quantoren aufgebaut ist. |
Lemma 3.12 Sei Φ ⊆ FO 0
≠ (S) eine Menge von universell-pränexen Sätzen. Dann sind äquivalent: |
(i) Φ erfüllbar. (ii) [[Φ]]AL erfüllbar. |
|
|
Erfülbarkeit
• Φ ⊆ FO 0
(S) eine Satzmenge (ohne freie Variablen) ist. Man erhält eine zu einer Formelmenge erfüllbarkeitsäquivalente Satzmenge, indem man neue Konstantensymbole für alle freien Variablen substituiert |
• Φ ⊆ FO 0
≠ (S) gleichheitsfrei ist. Eine explizite Modellierung der Gleichheitsrelation durch eine zusätzliche Äquivalenzrelation (siehe Bemerkung 2.13) führt zu erfüllbarkeitsäquivalenten Satzmengen ohne Gleichheit. |
• Φ ⊆ FO 0
≠ (S) aus universell-pränexen, gleichheitsfreien Sätzen besteht. Skolemisierung liefert eine erfüllbarkeitsäquivalente Satzmenge in universell-pränexer Form. |
• S mindestens ein Konstantensymbol enthält, sodass T 0
(S) ≠ ∅ ist, und wir uns ggf. auf Herbrand-Modelle von Φ ⊆ FO 0
≠ (S) zurückziehen können. |
Φ erfüllbar ⇔ H |= Φ für eine
Herbrand-Struktur H = T 0
(S),(R H) R
∈ S
.
Kompaktheitssatz (FO)
Satz 4.1 (Kompaktheitssatz) Für jede Formelmenge Φ ⊆ FO sind äquivalent: |
(i) Φ erfüllbar. (ii) Jede endliche Teilemenge Φ 0
⊆ Φ ist erfüllbar. |
Korollar 4.2 Für jede Formelmenge Φ ⊆ FO und Formel ψ ∈ FO sind äquivalent: |
(i) Φ |= ψ. (ii) Es existiert eine endliche Teilemenge Φ 0
⊆ Φ, sodass Φ 0
|= ψ. |
Das Korollar folgt aus dem Satz über den Zusammenhang: Φ|=φ gdw. Φ ∪ {¬φ} unerfüllbar. |
|
Created By
Metadata
Comments
No comments yet. Add yours below!
Add a Comment
More Cheat Sheets by tiziano123