Database Reference
In-Depth Information
Selbsttestaufgabe 3.63 (Steuern)
Gegeben sei die Formelmenge
Wahl steht bevor
⇒
(
∀
x
Steuer
(x)
⇒
wird nicht erhoht
(x))
Steuer
(
Mehrwertsteuer
)
Wahl steht bevor
(vgl. Selbsttestaufgabe 3.1(3)). Leiten Sie daraus die Formel
wird nicht erhoht
(
Mehrwertsteuer
)
mit Hilfe der oben angegebenen Ableitungsregeln ab.
3.5.6
Normalformen
Im Folgenden zeigen wir auf, wie sich mit den in Theorem 3.58 angegebenen Trans-
formationen jede PL1-Formel F in eine aquivalente Formel F
transformieren lasst,
so dass in F
alle Quantoren außen stehen. Eine Formel, in der alle Quantoren au-
ßen stehen, wird
Pranexform
genannt. Eine Pranexform, die als Junktor nur noch
Konjunktion, Disjunktion und Negation enthalt, wobei die Negation dabei nur un-
mittelbar vor Atomen auftritt, nennen wir
verneinungstechnische Normalform
.
Durch das folgende Verfahren konnen wir jede PL1-Formel in eine aquivalente
Formel in verneinungstechnischer Normalform uberfuhren:
1. Der erste Schritt, eine Formel in Pranexform zu uberfuhren, besteht darin,
eine bereinigte Form zu erstellen. Dabei heißt eine Formel
bereinigt
,sofernin
ihr keine Variable sowohl frei als auch gebunden auftritt und sofern hinter al-
len vorkommenden Quantoren verschiedene Variablen stehen. Eine bereinigte
Form einer PL1-Formel erhalten wir durch Anwendung der unter (5.) in Theo-
rem 3.58 angegebenen Transformationen, d.h. durch geeignete Umbenennung
von Variablen.
2. Mit Hilfe der Aquivalenzen (11) und (12) in Theorem 3.35 lassen sich die
Junktoren ⇒ und ⇔ vollstandig beseitigen. Danach muss Schritt 1 gegebe-
nenfalls wiederholt werden, da die Auflosung von ⇔ zu einer nicht bereinigten
Form fuhren kann.
3. Mit den de Morganschen Gesetzen und dem Satz von der doppelten Negation
( Aquivalenzen (6) und (7) in Theorem 3.35) wird das Negationszeichen ganz
nach “innen” geschoben, so dass es nur noch unmittelbar vor Atomen auftritt.
4. Die Regeln unter (2.) und (3.) in Theorem 3.58 erlauben es, alle Quantoren
ganz nach außen zu schieben.
Selbsttestaufgabe 3.64 (Pranexform)
Bilden Sie eine Pranexform zu der For-
mel (
¬∃
xP(x))
⇒
(
¬∃
xQ(x)).
Selbsttestaufgabe 3.65 (Normalform)
Uberfuhren Sie die Formel
C =
def
∃
z ((
¬∃
x(P (x, z)
∨∀
yQ(x, f (y))))
∨∀
yP(g(z, y),z))
in eine verneinungstechnische Normalform.
