Zurückführung des Entscheidungsproblems auf den Fall von Formeln mit einer einzigen, binären Funktionsvariablen. (Q2610759)

Verf. hat (Verhdl. internat. Math.-Kongr. Zürich 2 (1932), 337-338; F.~d.~M. 58\(_{\text{I}}\), 70) bewiesen: (1) Das Entscheidungsproblem des engeren Funktionenkalküls ist zurückführbar auf die Frage der Erfüllbarkeit eines Zählausdrucks mit einer einzigen ternären Funktionsvariablen und einem Präfix der Form \[ (E x_1) \, (E x_2) \ldots (E x_m) \, (y_1) \, (y_2) \, (E z) \, (u_1) \, (u_2) \ldots (u_n). \] (2) Es ist auch zurückführbar auf einen Zählausdruck mit einer einzigen binären Funktionsvariablen und einem Präfix, das nur ein Seinszeichen mehr enthält als das obige, nämlich unmittelbar nach \((Ez)\). -- Er vermutete aber, daß man auch im Falle einer binären Funktion dasselbe Präfix wie oben erreichen könnte. Das trifft zu, und vorliegender Aufsatz enthält den Beweis dafür. Beim Beweis geht Verf. von einer früher von ihm aufgestellten Normalform \(\mathfrak{A}\) der Zählausdrücke aus. Diese hat das obige Präfix; der Kern enthält die binären Funktionsvariablen \(F_1, \ldots \!, F_l\). Er führt eine neue binäre Funktionsvariable \(G\) ein und bildet einen Zählausdruck \(\mathfrak{B}\), in dessen Kern bloß \(G\) auftritt, während das Präfix die obige Form hat. Verf. beweist dann erstens, daß aus dem Erfülltsein von \(\mathfrak{A}\) in einem Bereiche \(I\) für eine gewisse Wahl \(\varPhi_1, \ldots \!, \varPhi_l\) der Variablen \(F_1, \ldots \!, F_l\) das Erfülltsein von \(\mathfrak{B}\) im Bereiche \(I^2+\{\varPhi_1, \ldots \!, \varPhi_l\}\) folgt, wo \(I^2\) die Menge aller geordneten Paare von \(I\) ist, und zwar für eine geeignet definierte Funktion \(\psi\) als Wert von \(G\). Zweitens beweist er, daß, wenn \(\mathfrak{B}\) in einem Bereiche \(I\) erfüllt ist für \(G=\psi\), \(\psi\) eine gewisse binäre logische Funktion \(\mathfrak{A}\) erfüllt in \(I'\) bei geeigneter Wahl der \(F_{\lambda}\), wobei \(I'\) die Menge aller Elemente \(a\) von \(I\) ist, für die \(\psi \,(a, \,a)\) wahr ist; dabei ist \(\psi \,(a, \,b)\) eine mathematische Funktion in \(I\), welche dem letzten Seinszeichen im Präfix entspricht.