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 t1 , . . . , tn ∈ T (S), so ist auch ft1 ...tn ∈T(S).
Tn (S) ⊆ T(S): die Mengen der Terme, in denen nur Variablensymbole aus Vn = {x1 , . . . , xn } 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 SF -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:
cT := c ∈ T(S).
• für n-stelliges Funktionssymbol f ∈ S: f T: T(S)n → T(S)
(t1 ,...,tn ) → ft1 ...tn .
Wenn S Konstantensymbole hat, ist auch T0 (S) Träger einer entsprechenden Termstruktur T0 (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 Q1 xi 1 ...Qk xik ψ, wo k ∈ N, Qi ∈ {∀, ∃} und ψ quantorenfrei. ψ heißt auch quantorenfreier Kern der Formel, Q1 xi1 . . . Qk xi 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):
tJ:=β(x).
• Für t = c (c ∈ S Konstantensymbol):
tJ:= cA.
• Für t = ft1 ...tn , mit n-stelligem Funktionssymbol f ∈ S:
tJ := fA (t1 J,...,tn 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: FOn (S) := {φ ∈ FO(S): frei(φ) ⊆ Vn }. Für φ ∈ FOn (S) schreiben wir auch φ = φ(x1 , . . . , x n ) um die möglicherweise freien Variablen explizit anzudeuten. |
frei(t1 = t2 ) := var(t1 ) ∪ var(t2 ).
frei(Rt1 . . . t n ) := var(t1 ) ∪ . . . ∪ 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 Φ ⊆ FO0 ≠ (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 T0 (S) übereinstimmen (H erweitert die SF -Struktur T0 (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 Φ ⊆ FO0 ≠ (S) eine Menge von universell-pränexen Sätzen. Dann sind äquivalent: |
(i) Φ erfüllbar. (ii) [[Φ]]AL erfüllbar. |
|
|
Erfülbarkeit
• Φ ⊆ FO0 (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 |
• Φ ⊆ FO0 ≠ (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. |
• Φ ⊆ FO0 ≠ (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 T0 (S) ≠ ∅ ist, und wir uns ggf. auf Herbrand-Modelle von Φ ⊆ FO0 ≠ (S) zurückziehen können. |
Φ erfüllbar ⇔ H |= Φ für eine
Herbrand-Struktur H = T0 (S),(RH)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