Zum Eliminationsproblem der mathematischen Logik. (Q2611337)

Verf. sagt, daß er in dem Falle, wo hinter dem Seinszeichen für das zu eliminierende Prädikat ein Wechsel von All- und Seinszeichen für Individuen auftritt, in seiner früheren Arbeit (Untersuchungen über das Eliminationsproblem der mathematischen Logik, Math. Ann. 110 (1934), 390-413; JFM 60.0022.*) keine allgemeine Lösungsmethode angeben konnte. Dagegen wurde dort darauf hingewiesen, daß mittels Einführung von Belegungsfunktionen das Problem sich auf ein solches reduziert, bei dem das ursprüngliche Prädikat verschwunden ist, und dafür zu eliminierende Belegungsfunktionen auftreten. Während man nun, wie er l. c. gezeigt hat, in einigen Fällen die Belegungsfunktionen fortschaffen kann, so erweist sich das doch nicht allgemein möglich. Man kann deshalb fragen, ob es nicht besser ist, die Belegungsfunktionen zu vermeiden, und in der Tat zeigt Verf., daß die früher mit ihrer Hilfe erreichten Resultate auch mit Hilfe einer anderen Methode ableitbar sind. Man hat es nämlich in allen jenen Fällen mit Ausdrücken zu tun, die in der Form \[ (EF)\,(x)\,\mathfrak A_c(Fxc,x) \] geschrieben werden können. Es gilt aber die Äquivalenz \[ (EF)\,(x)\,\mathfrak A_c(Fxc, x) \longleftrightarrow (x)\,(EG)\,\mathfrak A_c(Gc,x); \] denn einerseits ist \(Fxy\) bei festem \(x\) ein Prädikat von \(y\), so daß die Implikation \[ (EF)\,(x)\,\mathfrak A_c(Fxc,x) \to (x)\,(EG)\,\mathfrak A_c(Gc,x) \] gilt, und andererseits bekommt man durch Anwendung des Auswahlaxioms auch die umgekehrte Implikation. Mittels dieser Äquivalenz gelingt dann leicht die Elimination von \(F\). Es werden fünf Beispiele betrachtet; die schon von \textit{Schröder} vermuteten Resultanten erweisen sich als richtig. Zum Schlusse erwähnt Verf. die verallgemeinerte Äquivalenz: \[ (EF)\,(x)\,\mathfrak A_{c_1\ldots c_n}\,(Fxc_1\;\ldots c_n,x ) \longleftrightarrow (x)\,(EG)\,\mathfrak A_{c_1\ldots c_n}(Gc_1 \ldots c_n, x) \]