Status of the type-$\alpha$ axiom of infinity $Y^\alpha$ at $o$-only types in Church's simple theory of types

In Church's 1940 formulation of the simple theory of types, an axiom of infinity is available at every type $\alpha$ as a formula $Y^\alpha$ asserting that successor is injective on the numerals of type $\alpha$. Church's Theorem $26^\alpha$ derived $Y^\alpha$ from the ground instance $Y^\iota$ only for the iterated individual types $\iota'$, $\iota''$, ..., and Newman and Turing (1942) extended the derivation to every type symbol containing $\iota$, at the cost of also using the description axioms (Axiom 9) and the functional-extensionality axioms (Axiom 10). The remaining type symbols, those built from the proposition type $o$ alone, were excluded: Church had observed that $Y^\alpha$ is not provable there under a consistency proviso. The exact status — provable, refutable, or independent — of $Y^\alpha$ at the $o$-only types remains open.

Background

Church's simple theory of types (Church 1940) is a foundation for mathematics built as a typed $\lambda$-calculus, a formalism in which functions are introduced by abstraction ($\lambda x.\,M$ denotes the function mapping $x$ to $M$) and applied by juxtaposition. Its type symbols are generated from two atoms — $\iota$, the type of individuals (objects without structure), and $o$, the type of propositions — by the rule that $(\alpha\beta)$ is the type of total functions from type $\beta$ to type $\alpha$. Church's axiom system, called $(C)$ in Newman and Turing (1942), comprises the propositional axioms 1–4, the quantifier axioms $5^{\alpha}$–$6^{\alpha}$, an Axiom 7 asserting the existence of at least two individuals, an Axiom 8 asserting infinity at the individual type (the instance $Y^{\iota}$), the description axioms $9^{\alpha}$ for a definite-description operator $\iota_{\alpha(o\alpha)}$ that picks the unique object satisfying a property, the functional-extensionality axioms $10^{\alpha\beta}$ (functions equal at every argument are equal), and the choice axioms $11^{\alpha}$, under which the description operator can also serve as a selection operator. (This is Church's own numbering, also used by Newman and Turing; some later surveys number these axioms differently, and Church's printed list does not include the boolean-extensionality axiom for propositions that later presentations add.)

Numbers are represented at every type $\alpha$ by Church numerals: writing $\alpha_0=\alpha$ and $\alpha_{n+1}=(\alpha_n\alpha_n)$, the numeral zero at type $\alpha$ is the closed term $\lambda f_{\alpha\alpha}\lambda x_{\alpha}.x$ of the doubly-iterated type $\alpha_2$, with a successor operator $S$ and a numeral predicate $N$ (defined by an induction formula) at the same iterated type. The type-$\alpha$ axiom of infinity is then

$Y^{\alpha}=\lambda m_{\alpha_2}\lambda n_{\alpha_2}.\;N m\wedge N n\supset S m=S n\supset m=n,$

the assertion that successor is injective on the numerals of type $\alpha$ (Church's Theorem-$26^{\alpha}$ form; Newman and Turing prove it equivalent to a 'posterity' form $X^{\alpha}$ asserting that no number belongs to its own posterity, the objects obtainable from it by iterating successor). Church's Theorem $26^{\alpha}$ derived $Y^{\alpha}$ from the ground instance $Y^\iota$ (his Axiom 8) together with Axioms 1–7, but only for the iterated individual types $\iota'$, $\iota''$, ...; and he observed — under a consistency proviso — that $26^{\alpha}$ is not a theorem when the type symbol $\alpha$ consists solely of $o$'s.

Newman and Turing (1942) closed the individual-side gap: they gave a formal proof of $Y^{\alpha}$ for every type symbol containing $\iota$, using, in addition to Axioms 1–7 and $Y^\iota$, also the description axioms (Axiom 9, in connection with their Def. 4) and the functional-extensionality axioms (Axiom 10, used in their Theorem 9). Their method transports the infinity property along one-one maps: they define an injectivity predicate $\Omega^{\tau'\tau}h$ for a map $h_{\tau'\tau}$ from type $\tau$ into type $\tau'$, show that $Y$-infinity at the domain type $\tau$ is carried along such a map to the codomain type $\tau'$, and then run an induction over the structure of type symbols, embedding each factor type into the composite types built over it by constant functions. The work was motivated by Newman's intrinsic characterisation of the Church type stratification, published separately as Newman (1943). What the 1942 note leaves aside are the $o$-only type symbols — those built from the proposition type $o$ alone, such as $o$, $(oo)$, $((oo)o)$ — exactly the types to which Church's conditional non-provability observation applies.

The modern semantic framework for such questions is Henkin's (1950) completeness theorem for the theory of types: provability in $(C)$ is equivalent to truth in all general models, models in which each function domain may be a proper subset of the full function space, so non-provability questions become model-existence questions. Andrews (1963, 1972) refined the axiomatics of the propositional-types fragment and the roles of descriptions and choice under these semantics, and Turing (1948) developed alternative type disciplines. The per-type status of the axiom of infinity at the $o$-only types remains open.

Problem Statement

For Church's 1940 system $(C)$ of the simple theory of types — Axioms 1–11 as printed there: the propositional axioms 1–4, the quantifier axioms $5^{\alpha}$–$6^{\alpha}$, Axiom 7 (at least two individuals), Axiom 8 (the axiom of infinity $Y^{\iota}$), the description axioms $9^{\alpha}$, the functional-extensionality axioms $10^{\alpha\beta}$, and the choice axioms $11^{\alpha}$ — determine the exact deductive status of the type-$\alpha$ axiom of infinity $Y^{\alpha}$, the universal closure of injectivity of successor on the type-$\alpha$ numerals (Church's formula $26^{\alpha}$), for each type symbol $\alpha$ built from $o$ alone, for example $\alpha=o$, $(oo)$, $((oo)o)$: is $Y^{\alpha}$ provable in $(C)$, refutable in $(C)$, or independent of $(C)$? Church 1940 asserted non-provability for these types under a consistency proviso; Newman and Turing (1942) proved the $\iota$-containing cases and left the $o$-only types outside their theorem.

References

1. M. H. A. Newman and A. M. Turing, "A formal theorem in Church's theory of types", Journal of Symbolic Logic 7(1):28–33 (1942). DOI 10.2307/2267552, https://doi.org/10.2307/2267552
2. Alonzo Church, "A formulation of the simple theory of types", Journal of Symbolic Logic 5(2):56–68 (1940). DOI 10.2307/2266170, https://doi.org/10.2307/2266170
3. M. H. A. Newman, "Stratified systems of logic", Proceedings of the Cambridge Philosophical Society 39(2):69–83 (1943). DOI 10.1017/s0305004100017722, https://doi.org/10.1017/s0305004100017722
4. Alonzo Church, review of M. H. A. Newman, "Stratified systems of logic", Journal of Symbolic Logic 9(2):50–52 (1944). DOI 10.2307/2268031, https://doi.org/10.2307/2268031
5. Leon Henkin, "Completeness in the theory of types", Journal of Symbolic Logic 15(2):81–91 (1950). DOI 10.2307/2266967, https://doi.org/10.2307/2266967
6. A. M. Turing, "Practical forms of type theory", Journal of Symbolic Logic 13(2):80–94 (1948). DOI 10.2307/2267329, https://doi.org/10.2307/2267329
7. P. Andrews, "A reduction of the axioms for the theory of propositional types", Fundamenta Mathematicae 52(3):345–350 (1963). DOI 10.4064/fm-52-3-345-350, https://doi.org/10.4064/fm-52-3-345-350
8. Peter B. Andrews, "General models, descriptions, and choice in type theory", Journal of Symbolic Logic 37(2):385–394 (1972). DOI 10.2307/2272981, https://doi.org/10.2307/2272981
9. R. O. Gandy, "Axioms of Infinity in Church's Type Theory", in C. Anthony Anderson and Michael Zelëny (eds.), Logic, Meaning and Computation (Synthese Library 305), Springer, Dordrecht, pp. 139–147 (2001). DOI 10.1007/978-94-010-0526-5_5, https://doi.org/10.1007/978-94-010-0526-5_5
10. Helmut Schwichtenberg, "Definierbare Funktionen im λ-Kalkül mit Typen", Archiv für Mathematische Logik und Grundlagenforschung 17(3–4):113–114 (1975). DOI 10.1007/bf02276799, https://doi.org/10.1007/bf02276799
11. Christoph Benzmüller and Peter Andrews, "Church's Type Theory", The Stanford Encyclopedia of Philosophy (substantive revision of 16 January 2024), https://plato.stanford.edu/entries/type-theory-church/
12. Leon Henkin, review of M. H. A. Newman and A. M. Turing, "A formal theorem in Church's theory of types", Journal of Symbolic Logic 7(3):122 (1942). DOI 10.2307/2269297, https://doi.org/10.2307/2269297