Anwendung des ε-Symbols auf die Untersuchung des logischen Formalismus

Zusammenfassung

Die Ergebnisse der beiden vorigen Paragraphen knüpfen sich an die eine der beiden Problemstellungen, die wir im Zusammenhang mit der Einführung des ε-Symbols aufgeworfen haben, nämlich diejenige betreffend die generelle Möglichkeit, aus einer Ableitung mittels des Prädikatenkalkuls (und eventuell auch der ε-Formel), wenn die darin benutzten Axiome sowie die abgeleitete Formel keine gebundene Variable enthalten, überhaupt die gebundenen Variablen auszuschalten. Diese Möglichkeit wird durch das erste ε-Theorem³ festgestellt. Nun bleibt noch die andere Aufgabe, die sich auf die symbolische Auflösung von Existenzialformeln bezieht ⁴. Wir wollten zeigen, daß die Anwendung dieses Prozesses im Rahmen des Formalismus eines Axiomensystems S der ersten Stufe den Bereich der ableitbaren Formeln, die sich mit den Symbolen von S bilden lassen, nicht erweitert.