Beiträge zum Entscheidungsproblem der mathematischen Logik. (Q2605693)

Bei den Untersuchungen über das Erfüllbarkeitsproblem für Zählausdrücke kann man sich bekanntlich auf die Betrachtung gewisser Normalformen von besonders einfacher Gestalt beschränken. Zu den früher bekannten Normalformen wird in der vorliegenden Arbeit noch eine hinzugefügt. Verf. beweist nämlich, daß man zu jedem gegebenen Zählausdruck einen anderen mit dem Präfix \[ (Ex) (y) (Ez) (u_1) \dots (u_n) \tag{1} \] angeben kann derart, daß beide Ausdrücke hinsichtlich ihrer Erfüllbarkeit gleichwertig sind. In seinem Beweis geht er von einem Ausdruck der \textit{Kalmár}schen Normalform aus; das ist aber nicht nötig, und er gibt eine Andeutung davon, wie der Beweis aussieht, wenn er von der Normalform des Ref. ausgeht. Der Beweis beruht im Wesentlichen darauf, daß die Seinszeichen durch Belegungsfunktionen ersetzt werden, der Bereich, worin der Zählausdruck erfüllt ist, auf die Zahlenreihe \(Z\) abgebildet wird, die Belegungsfunktionen dann durch Einschachtelung aufgebaut werden und dieser Aufbau durch Allzeichen charakterisiert wird. Hierdurch gelingt ein Ersatz der Seinszeichen bis auf zwei durch Allzeichen, so daß man ein Präfix der Form (1) bekommt. Im Teil II seiner Arbeit betrachtet Verf. die Zählausdrücke vom Typ \[ (x) (Ey) F(x, y) \;\& \;(z_1) \dots (z_n) A(z_1, \dots, z_n; F). \tag{2} \] Indem \(B(z_1, \dots, z_n; F)\) die Konjunktion aller Ausdrücke ist, die aus \(A\) entstehen, wenn man darin statt \(z_1, \dots, z_n\), alle Reihen von \(n\) gleichen oder verschiedenen der \(z_i\) einsetzt, wobei natürlich (2) mit \[ (x) (Ey) F(x, y) \;\& \;(z_1) \dots (z_n) B(z_1, \dots, z_n; F) \tag{3} \] gleichwertig ist, zeigt Verf., daß (3) schon in einem Bereiche mit \(n +1\) Elementen erfüllt ist, falls (3) überhaupt im Endlichen erfüllbar ist. Weiter bildet er den Zählausdruck \[ (x) (Ey) F(x, y) \& (z_1) \dots (z_n) [B(z_1, \dots, z_n; F) \& \overline F(z_1, z_1) \& \overline F(z_1, z_2) \overline F(z_2, z_1) \& \dots \tag{4} \] \[ \& \overline F(z_1, z_2) \overline F(z_2, z_3) \dots \overline F(z_n, z_1) \& \overline F(z_1, z_2) \overline F(z_2, z_3) \dots \overline F(z_{n-1}, z_n) \varPi^\prime F(z_i, z_k)], \] wo \(\varPi^\prime F(z_i, z_k)\) die Disjunktion aller \(F(z_i, z_k)\) bedeutet, wo \(1 \leqq i\), \(k \leqq n\) und \(k \geqq i + 2\) ist, und zeigt, daß, wenn (3) in keinem endlichen Bereiche erfüllt ist, die Erfüllbarkeit von (3) mit der von (4) gleichwertig ist. Durch Abbildung auf \(Z\) gelingt nun die Lösung des Erfüllbarkeitsproblems in den Fällen \(n = 3\) und \(n = 4\), während \(n < 3\) kein Interesse hat, da dieser Fall durch frühere Arbeiten mit erledigt ist. Ist \(n = 3\), so ist (4) dann und nur dann erfüllbar, wenn \[ (z_1)(z_2)(z_3) B(z_1, z_2, z_3; <) \tag{5} \] in \(Z\) erfüllbar ist, was man bekanntlich entscheiden kann. Ist \(n = 4\), so bekommt man statt (5) den Ausdruck \[ (z_1)(z_2)(z_3)(z_4) B(z_1, z_2, z_3, z_4; \varPhi_1) \vee (z_1)(z_2)(z_3)(z_4) B(z_1, z_2, z_3, z_4; \varPhi_2), \tag{6} \] wo \(\varPhi_1(x, y)\) die Relation \(x < y\) und \(\varPhi_2(x, y)\) die Relation \(x< y \;\& \;y \equiv x + 1 \pmod 2\) bedeuten. Da man auch entscheiden kann, ob (6) in \(Z\) erfüllbar ist oder nicht, so ist also auch der Fall \(n = 4\) erledigt. Es ist bemerkenswert, daß es hierdurch zum ersten Male gelungen ist, das Entscheidungsproblem zu lösen für eine Klasse von Ausdrücken, die erfüllbar sein können, ohne bereits im Endlichen erfüllbar zu sein.