|
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: φ≡ψ.
|
|
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.
|
|
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.
|
1, . . . , tn ∈ T (S), so ist auch ft1...tn ∈T(S).n(S) ⊆ T(S): die Mengen der Terme, in denen nur Variablensymbole aus Vn = {x1, . . . , xn} vorkommen.0(S) für die Menge der Variablen-freien Terme (= ∅ wenn S keine Konstanten hat).|
Definition 2.6 [Allgemeingültigkeit]
|
|
Eine Formel φ ∈ FO(S) heißt allgemeingültig gdw. für alle S-Interpretationen J gilt: J |= φ.
|
|
Definition 2.5 [Folgerungsbeziehung]
|
|
φ |= ψ bzw. Φ |= ψ.
|
|
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 ∪ {∼}). |
|
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: |
1,...,tn) → ft1 ...tn.0(S) Träger einer entsprechenden Termstruktur T0(S) (eine Substruktur von T (S)).
|
Definition 3.1 [pränexe NF] FO-Formeln in pränexer Normalform sind von der Form Q
1xi1 ...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.
|
1 ...tn, mit n-stelligem Funktionssymbol f ∈ S:1J,...,tnJ ).|
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(φ) ⊆ Vn}. Für φ ∈ FOn(S) schreiben wir auch φ = φ(x1, . . . , x n) um die möglicherweise freien Variablen explizit anzudeuten. |
1 = t2) := var(t1) ∪ var(t2). 1 . . . t n) := var(t1) ∪ . . . ∪ var(t n).|
Definition 2.3 [Quantorenrang]
|
|
Induktive Definition des Quantorenrangs, qr(φ) ∈ N, für φ ∈ FO(S):
|
|
Formeln von Quantorenrang 0 heißen quantorenfrei.
|
|
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.
|
|
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 = ( T
0(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 Φ ⊆ FO
0≠ (S) eine Menge von universell-pränexen Sätzen. Dann sind äquivalent: |
|
(i) Φ erfüllbar. (ii) [[Φ]]AL erfüllbar.
|
|
• Φ ⊆ 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 Φ ⊆ FO0≠ (S) zurückziehen können. |
0(S),(RH)R∈S .
|
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.
|
No comments yet.
Cheatography n. The art of mapping complex subjects into clear, instantly navigable reference guides.