Zum Entscheidungsproblem des logischen Funktionenkalküls. (Q2624160)

Klassifiziert man die Formern des engeren Funktionenkalküls (im Sinn der ``Theoretischen Logik'' von \textit{Hilbert} und \textit{Ackermann}) nach der Zahl der in der Normalform auftretenden (benachbarten) Allzeichen, so ist für den Fall eines einzigen Allzeichens seit längerem bekannt, daß die Formern, soweit überhaupt erfüllbar, schon in einem endlichen Individuenbereich erfüllbar sind. Für den Fall zweier Allzeichen haben \textit{Gödel} (Ergebnisse Math. Kolloquium Wien 2 (1931), 27-29; F. d. M. 57\(_{\text{II}}\)) und \textit{Kalmár} (vorstehendes Referat) kürzlich gezeigt, wie über die Erfüllbarkeit der Formel entschieden werden kann. Der Nachweis, daß auch eine solche Formel, falls erfüllbar, schon in einem endlichen Bereich erfüllt werden kann, bildet den Hauptteil der vorliegenden Arbeit. Bei dem interessanten, nicht einfachen Beweis spielt eine wesentliche Rolle der Gebrauch von ``Modellen über einem Individuenbereich \(\mathfrak F\)'', d. h. von Systemen endlich vieler in \(\mathfrak F\) definierter Funktionen mit Je endlich vielen Leerstellen; dabei ist für \(\mathfrak F\) vor allem der Bereich der natürlichen Zahlen \(\leqq k\) heranzuziehen. - Das Resultat gilt auch noch für Formern, die das \(=\)-Zeichen enthalten. Zum Schluß wird der Fall dreier Allzeichen in einer Formel der eingangs beschriebenen Art diskutiert und gezeigt, daß jedem Zählausdruck ein Zählausdruck mit drei Allzeichen gleichwertig (gleichzeitig erfüllbar oder unerfüllbar) ist. Die Lösung dieses Falls wäre also gleichwertig mit der Lösung des Entscheidungsproblems überhaupt. Editorial remark (2021): In the last sentence, Gödel mentions that Theorem I can also be proved, by the same method, for formulas that contain the identity sign. As Wiliam Goldfarb remarks on p. 229--231 of [\textit{K. Gödel}, Collected works. Volume I: Publications 1929--1936. Ed. by Solomon Feferman et al. (1986; Zbl 0592.01035)], this is not true - the satisfiability of formulas in the larger class is not decidable.