Logische ÄquivalenzDefinition 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äquivalenzDefinition 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. |
SignaturenEine 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-StrukturenDefinition 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-TermeDefinition 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ültigkeitDefinition 2.6 [Allgemeingültigkeit] | Eine Formel φ ∈ FO(S) heißt allgemeingültig gdw. für alle S-Interpretationen J gilt: J |= φ. |
| | FolgerungsbeziehungDefinition 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 GleichheitDefinition 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 ∪ {∼}). |
TermstrukturDefintion 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 NormalformDefinition 3.1 [pränexe NF] FO-Formeln in pränexer Normalform sind von der Form Q1xi1 ...Qkxik ψ, wo k ∈ N, Qi ∈ {∀, ∃} und ψ quantorenfrei. ψ heißt auch quantorenfreier Kern der Formel, Q1xi1 . . . Qk xik 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 . | | BelegungenDefinition 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 (t1J,...,tnJ ). |
Schreibweisen für Belegungen und Interpretationen auf Seite 6 FO Skript über Kapitel 2 Freie VariablenDefinition 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}. QuantorenrangDefinition 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. SemantikDefinition 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. |
HerbrandSatz 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