A theorem on deducibility for second-order functions. (Q2590257)

Verf. hat schon früher gezeigt, daß jeder Satz erster Stufe, in welchem eine einzige freie Funktionsvariable \(R\) mit zwei Leerstellen auftritt, entscheidbar wird, sobald man den Axiomen des Funktionenkalküls die Aussage hinzufügt, welche inhaltlich besagt, daß die mit \(R\) bezeichnete Relation ihr Feld nach einem dichten Typus ordnet (Ann. Math., Princeton, (2) 28 (1926), 16-40; F. d. M. 52, 48). Wird nun außerdem die Stetigkeit gefordert, so läßt sich die Entscheidbarkeit auf gewisse Sätze zweiter Ordnung übertragen. Diese Sätze dürfen nämlich Funktionsvariablen \(\varPhi\) mit einer Leerstelle als gebundene Funktionsvariablen enthalten, hinter jedem Quantifikator \((\varPhi)\) bzw. \((\exists \varPhi)\) muß jedoch die Bedingung hinzugefügt werden, daß das betreffende \(\varPhi\) ein Anfangsstück des Feldes von \(R\) bezeichnet. Dieses Ergebnis ist eine unmittelbare Folgerung des oben erwähnten Theorems und der Tatsache, daß jedem Satz der beschriebenen Art ein äquivalenter Satz erster Stufe zugeordnet werden kann, was sich auf natürliche Weise dadurch erklärt, daß jedes Anfangsstück des Feldes von \(R\) durch seine obere Grenze eineindeutig bestimmt ist.