Database Reference
In-Depth Information
In Abschnitt 3.2.4 hatten wir bereits uber die Erfullungsrelation und den Zu-
sammenhang zur logischen Folgerung gesprochen. Die folgende Definition fuhrt den
Begriff der logischen Folgerung fur Formeln und auch fur Formelmengen ein.
Definition 3.14 (klassisch-logische Folgerung)
Die Relation
|
=
Σ
⊆
Formel
(Σ)
×
Formel
(Σ)
ist definiert durch
F
|
=
Σ
G gdw. Mod
Σ
(F )
⊆
Mod
Σ
(G)
wobei F und G Formeln sind. Fur F
=
Σ
G sagen wir “aus F folgt (logisch) G”
oder auch “aus F folgt semantisch G”. Wir erweitern
|
|
=
Σ
, indem wir fur F und G
auch Formelmengen zulassen.
)=
Int
(Σ) gilt, ist eine Formel F offen-
sichtlich genau dann allgemeingultig, wenn sie aus der leeren Menge von Formeln
folgt; statt
Da fur die leere Formelmenge Mod
Σ
(
∅
∅|
=
Σ
F schreiben wir dann auch
|
=
Σ
F . Zur Vereinfachung unserer No-
tation werden wir im Folgenden statt
= schreiben, wenn die betreffende
Signatur aus dem Kontext heraus klar ist; also z. B.
|
=
Σ
einfach
|
|
= F
gdw.
F
ist allgemeingultig.
Ebenso werden wir den Index Σ in
Mod(F)
etc. weglassen. Falls F
|
= G
nicht
gilt,
so schreiben wir dafur F
|
= G.
Mit der Relation
|
=konnen wir nun eine Funktion definieren, die jeder Formel-
menge
F
die Menge aller Formeln zuordnet, die logisch aus
F
folgen.
Definition 3.15 (klassisch-logische Inferenzoperation)
Die Funktion
Forme l (Σ)
2
Forme l (Σ)
:
→
Cn
Cn
(
F
):=
{
G
∈
Formel
(Σ)
|F|
= G
}
heißt
klassisch-logische Inferenzoperation
.
Definition 3.16 (deduktiv abgeschlossen, Theorie)
Eine Formelmenge
F⊆
Formel
(Σ) mit
Cn
(
F
)=
F
heißt
(deduktiv) abgeschlossen
. Formelmengen
F
bzw. ihr deduktiv abgeschlossenes
Pendant
Cn
(
F
) werden auch als
Theorien
bezeichnet.
Eine (deduktiv abgeschlossene) Theorie ist daher ein
Fixpunkt
des Operators
Cn
.
Fur aussagenlogische Formeln und fur geschlossene PL1-Formeln gilt die fol-
gende fundamentale Beziehung zwischen logischer Folgerung und Implikation, die
es gestattet, die logische Folgerung auf den Begriff der Allgemeingultigkeit zuruck-
zufuhren: