Database Reference
In-Depth Information
Theorem 3.17 (Deduktionstheorem)
F
|
= G
gdw.
|
= F
⇒
G
Beachten Sie aber bitte, dass auf der rechten Seite des Deduktionstheorems
|
= F
⇒
G und
nicht
F
⇒
G steht! Wahrend
|
= F
⇒
G die Allgemeingultigkeit der
Implikation ausdruckt, ist F
G eine syntaktische Formel, uber die nichts weiter
gesagt ist, die also insbesondere in verschiedenen Interpretationen wahr oder falsch
sein kann.
⇒
Selbsttestaufgabe 3.18 (Inferenzoperation)
Benutzen Sie das Deduktions-
theorem, um fur aussagenlogische Formeln F und G zu zeigen:
Cn(F
∨
G)=Cn(F )
∩
Cn(G)
3.3.3
Inferenzregeln und Kalkule
Wenn wir voraussetzen, dass wir Syntax und Semantik eines logischen Systems be-
reits definiert haben, so konnen wir eine solche Logik um einen
Kalkul
erweitern. Ein
Kalkul besteht aus einer Menge von logischen
Axiomen
und
Inferenzregeln
(siehe
z.B. [17, 19]). Die Axiome sind entweder eine Menge von elementaren Tautologi-
en (
positiver
Kalkul) oder eine Menge von elementaren Widerspruchen (
negativer
Kalkul). Die Inferenzregeln eines Kalkuls bilden eine Menge von Vorschriften, nach
denen aus Formeln weitere Formeln abgeleitet werden konnen. Inferenzregeln wer-
den ublicherweise wie folgt notiert:
F
1
,
...,
F
n
F
Eine solche Regel besagt, dass aus den Formeln F
1
,...,F
n
die Formel F abgeleitet
werden kann. Um diese Regel anwenden zu konnen, muss lediglich das Vorhanden-
sein von Formeln uberpruft werden, die syntaktisch mit den Formeln F
1
,...,F
n
ubereinstimmen. F
1
,...,F
n
sind die
Bedingungen
und F ist die
Schlussfolgerung
der Regel. Ein Beispiel fur eine Inferenzregel ist der
modus ponens
:
F,
F
⇒
G
(
MP
)
G
Diese Regel besagt, dass man bei Vorliegen von Formeln F und F
G die Formel
G ableiten kann. Die Inferenzregel des
modus tollens
ist eine Umkehrung des
modus
ponens
⇒
F
⇒
G,
¬
G
(
MT
)
¬
F
-Einfuhrung besagt, dass aus der Gultigkeit von zwei Formeln deren Kon-
junktion geschlossen werden kann:
Die
∧
F, G
F
(
∧
-Einf
)
∧
G
