8 11. _ Das Entscheidungsproblem im Funktionenkalkül. 73

druck bei beliebigen Einsetzungen für die vorkommenden Variablen eine
vichtige Behawptung darstellt oder micht?

Bei dem Problem der Erfüllbarkeit handelt es sich um die Frage,
ob es überhaupt eine Einsetzung für die Variablen gibt, so daß durch den
betreffenden Ausdruck eine rvichtige Behauptung dargestellt wird.

Beide Probleme sind zueinander dual. Ist ein Ausdruck nicht
allgemeingültig, so ist das Gegenteil erfüllbar und umgekehrt.

Das Entscheidungsproblem läßt sich nun auch für den Funktionen-
kalkül aufwerfen. Zu den Aussagenvariablen treten hier die Funktions-
variablen hinzu. Die Individuenvariablen wollen wir uns hier immer
- durch vorgesetzte Klammerzeichen gebunden denken. Man kann sich
übrigens auf den Fall beschränken, daß die Aussagenvariablen fehlen.
Diese lassen sich nämlich nach den in $ 8 des I. Kapitels gemachten
Bemerkungen immer eliminieren.

Ein Beispiel für eine allgemeingültige Formel des Funktionen-
kalküls ist die folgende Formel:

(x)(F(x) v F(x)).
Diese ist richtig, welches Prädikat auch für / eingesetzt wird. Die
} 1
Forme (EOFO

ist zwar nicht allgemeingültig, aber erfüllbar. Wir brauchen hier ja
nur das Prädikat ‚,mit sich selber identisch sein‘ zu nehmen. Dieses
trifft nicht nur auf einen, sondern sogar auf alle Gegenstände zu. Daraus
ergibt sich, daß auch

(%) F (%)
einen erfüllbaren Ausdruck darstellt. Weitere Beispiele für allgemein-
gültige Formeln sind

(x) (Ey)(R(x, %) v R(x, y)),
(Ex) (y)(Rı(x, x) v Rı(y, y) v Ra(%, y))

sowie alle Formeln, die sich aus den logischen Axiomen ableiten lassen,
z. B. unsere früheren Formeln (21)—(36). Nicht allgemeingültig ist
dagegen
(x) F (x, x),
nicht erfüllbar
(Ex) (y)(F(x, x) & F(%, y)) -

Das Entscheidungsproblem ist gelöst, wenn man ein Verfahren kennt»
das bei einem vorgelegten logischen Ausdruck durch endlich viele Ope-
yationen die Entscheidung über die Allgemeingültigkeit bzw. Erfüllbarkeit
erlaubt.

Die Lösung des Entscheidungsproblems ist für die Theorie aller Ge-
biete, deren Sätze überhaupt einer logischen Entwickelbarkeit aus endlich