$ 1. Notwendigkeit einer Erweiterung des Kalküls, 85

in den Formein ausgedrückten Eliminationsregel fort. Z.B. erhält
man aus

(X1) X (41X, Xi& AyXı Xr& Ap Xı Xr& Ar X, X3
zunächst durch Fortschaffung des Klammerzeichens (X,)

(X)((4, & 4,) X; & (43 & 44)X;)
und weiter
A, &1A2 &4Az&As.

Diese jetzt symbolisch formulierbare E/iminationsregel erlaubt uns,
* die Richtigkeit bzw. Falschheit der Formeln zu erkennen, in denen
nur Aussagenvariable und die zugehörigen Klammerzeichen vorkommen,
Bei der obenerwähnten Formel

(X)(EY)(XY & X & Y)
z. B. entwickeln wir zunächst XY & X& Y nach Y. Man erhält
(L,
Die Elimination der innersten Klammerzeichen liefert
(X)(XX).

XX ist aber ein allgemeingültiger Ausdruck, (X)(EY)(XY & X & Y)
demnach eine richtige Formel,

Wir haben hier einen Spezialfall des Entscheidungsproblems für
den erweiterten Funktionenkalkül. Das Entscheidungsproblem war vor-
her formuliert als das Problem der Allgemeingültigkeit bzw. Erfüll-
barkeit für Ausdrücke, die von Aussagen und Funktionsvariablen ab-
hängen. In dem erweiterten Kalkül sind auch Formeln möglich, die
von keiner Variablen abhängen, die also bestimmte Aussagen dar-
stellen. Für diese handelt es sich darum, über ihre Richtigkeit bzw.
Falschheit zu entscheiden. Da wir jetzt für die Allgemeingültigkeit
bzw. Erfüllbarkeit einen symbolischen Ausdruck haben, so kann man
das Entscheidungsproblem immer in der zweiten Fassung betrachten.
Der Allgemeingültigkeit bzw. Erfüllbarkeit z. B. einer Formel

(Ex) (y) (F(x, x) v F(y, y) v G(%, y))
entspricht in dem erweiterten Kalkül die Richtigkeit der Formel
(F) (G) (Ex) (y)(F(x, x) v F(y, y) v G(%, y))
bzw. (EF) (EG) (Ex) (y)(F(x, x) v F(y, y) v G(x, y)).
Nun brauchen wir uns nicht auf die Formeln zu beschränken, in denen
die zu den Funktionsvariablen gehörigen Klammerzeichen entweder
alle Allzeichen oder alle Existenzialzeichen sind, sondern wir können

ganz beliebige Kombinationen von All- und Existenzialzeichen zulassen,
und können nach einem Kriterium für die Richtigkeit von derartigen