132.231.141.109: /* Beispiel */

2024-06-03T12:41:52Z

Beispiel

Neue Seite

Die '''Pränexform''' ist eine mögliche [[Normalform]], in der [[Logische Aussage|Aussagen]] der [[Prädikatenlogik]] dargestellt werden können. Sie wird unter anderem als Vorstufe zur [[Skolemform]] benötigt.

Eine Aussage in der [[Prädikatenlogik erster Stufe]] befindet sich in Pränexform, wenn alle [[Quantor]]en (Beschreibungen des Geltungsbereichs) außerhalb bzw. vor der eigentlichen Formel stehen. Enthält die Pränexform zusätzlich nur [[Konjunktion (Logik)|Konjunktion]], [[Disjunktion]] und [[Negation#Logik|Negation]] (unmittelbar vor Atomen) als [[Junktor]]en, so wird sie auch als ''verneinungstechnische Normalform'' bezeichnet.

In der [[Klassische Logik|klassischen Prädikatenlogik]] gibt es zu jeder Formel eine [[Logische Äquivalenz|logisch äquivalente]] Formel in Pränexform. In der [[Intuitionismus (Logik und Mathematik)|intuitionistischen Logik]] ist das nicht notwendig gegeben.

Eine Formel in [[Bereinigte Normalform|bereinigter]] Pränexform ist [[Erfüllbarkeit|erfüllbar]], wenn ihre [[Skolemform]] erfüllbar ist.

== Mathematische Definition ==
Eine Formel <math>F</math> der Prädikatenlogik befindet sich in Pränexform, wenn sie von der Form

:<math>F = Q_1 y_1 Q_2 y_2 \dots Q_k y_k \hat{F}</math>
:
ist, mit
:<math>k\ge0</math> und
:<math>Q_1,\dots,Q_k\in \left\{ \forall, \exists \right\}</math>.
In <math>\hat{F}</math> darf kein [[Quantor]] vorkommen.

<math>Q_1 y_1 Q_2 y_2 \dots Q_k y_k</math> heißt Präfix, <math>\hat{F}</math> ist die [[Matrix (Logik)|Matrix]].

== Nicht-Eindeutigkeit ==
Die Pränexform ist nicht eindeutig.<ref>https://formal.kastel.kit.edu/teaching/FormSysWS1415/09PK1Normalform-print.pdf#page=12</ref> So hat die Formel
:<math>\forall x p(x) \rightarrow \forall y q(y)</math>
die beiden Pränexformen
:<math>\exists x \forall y (p(x) \rightarrow q(y))</math>
und
:<math>\forall y \exists x (p(x) \rightarrow q(y))</math>.

== Beispiel ==
Die Ausgangsformel laute wie folgt:
: <math>\forall x.P(x)\land \forall y.Q(y) \land \forall z.R(z,y)</math>

Die Variable <math>y</math> kommt sowohl gebunden als auch frei vor. Dies darf in der Pränexform aber nicht sein. Deshalb wird eine neue Variable eingeführt: <math>w</math>. Nach der Anpassung sieht das nun so aus:

: <math>\forall x.P(x)\land \forall w.Q(w) \land \forall z.R(z,y)</math>

Nun kommt jede Variable entweder gebunden oder frei vor und somit können wir die Quantoren alle nach vorn „ziehen“, was dann folgendermaßen aussieht:

: <math>\forall x.\forall w.\forall z.(P(x)\land Q(w)\land R(z,y))</math>

== Einzelnachweise ==
<references/>

[[Kategorie:Logik|Pranexform]]
[[Kategorie:Normalform]]

Pränexform - Versionsgeschichte

132.231.141.109: /* Beispiel */