Database Reference
In-Depth Information
xF
F [x/t]
∀
(
∀
-Inst
)
Dabei entsteht F [x/t]ausF , indem man jedes freie Auftreten von x in F durch t
ersetzt.
6
Stellt man sich vor, dass die Konstanten c
1
,c
2
,c
3
,... alle Objekte des
Universums bezeichnen, so kann man durch wiederholte Anwendung der ∀-
Instantiierungsregel aus ∀xF jede Formel F [x/c
i
] ableiten; somit kann man auch
die (im Allgemeinen unendliche) Konjunktion
F [x/c
1
]
∧
F [x/c
2
]
∧
F [x/c
3
]
∧
...
ableiten (vgl. die Aquivalenzen unter (3.) in Theorem 3.58 und die Diskussion dazu!).
Dual zu diesen Uberlegungen steht eine Formel
∃
xF fur die (im Allgemeinen
unendliche) Disjunktion
F [x/c
1
]
∨
F [x/c
2
]
∨
F [x/c
3
]
∨
...
Allerdings konnen wir nicht wissen, welches c
i
wir fur x einsetzen durfen. Daraus
ergibt sich die
∃
-Instantiierungsregel
(“Es gibt”-Instantiierungsregel):
xF
F [x/c]
∃
(
∃
-Inst
)
wobei c eine
neue
Konstante ist, die bisher noch nicht benutzt wurde (dies ent-
spricht also einer impliziten Signaturerweiterung um die Konstante c). Die Idee
dieser Inferenzregel ist die folgende: Eine Formel
xP(x)istgenaudannineiner
Interpretation
I
erfullbar, wenn wir ein Element e des Universums von
I
finden, so
dass e
∃
P
I
gilt. Wenn wir c gerade durch dieses e interpretieren, erfullt
I
wegen
[[ c]]
I
= e auch die Formel P (c). Essentiell ist dabei, dass c eine
neue
Konstante
ist, uber die wir bisher folglich noch keinerlei Annahmen gemacht oder abgeleitet
haben. Alles, was die
∈
∃
-Instantiierungsregel macht, ist also, dass fur das Objekt,
dessen Existenz durch
xF sichergestellt ist, ein Name vergeben wird; wie dieser
Name interpretiert wird, bleibt dabei vollig offen.
7
Wir wollen nun ein bekanntes Beispiel mit Hilfe der eingefuhrten Inferenzregeln
beweisen.
∃
Beispiel 3.62 (Politiker)
Wir nehmen einmal an, dass Politiker niemanden
mogen, der knauserig ist, dass jeder Politiker eine Firma mag und dass es uber-
haupt Politiker gibt. Zu zeigen ist, dass aus diesen Annahmen folgt, dass es eine
Firma gibt, die nicht knauserig ist. Die Annahmen konnen wir durch die drei fol-
genden PL1-Formeln ausdrucken:
6
Tatsachlich darf
t
sogar Variablen enthalten. Dann gilt jedoch noch eine kleine technische Ein-
schrankung, um Konflikte zwischen den Variablen in
t
und den Variablen in
F
zu vermeiden
(
t
darf keine Variable enthalten, die in
F
gebunden ist); hierauf wollen wir aber nicht weiter
eingehen.
7
Tatsachlich konnten wir auch hier etwas großzugiger sein und anstelle einer neuen Konstanten
c
einen Term
f
(
x
1
,...,x
n
) zulassen, wobei
f
ein neues Funktionssymbol und
x
1
,...,x
n
die in
F
frei auftretenden Variablen sind; auch hierauf wollen wir hier aber nicht weiter eingehen.
