On the strength of a weak variant of the Axiom of Counting

In this paper ${\mathrm{N}\mathrm{F}\mathrm{U}}^{-\mathrm{A}\mathrm{C}}$ is used to denote Ronald Jensen’s modification of Quine’s `New Foundations’ Set Theory ($\mathrm{N}\mathrm{F}$) fortified with a type-level pairing function but without the Axiom of Choice. The axiom ${\mathrm{A}\mathrm{x}\mathrm{C}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{t}}_{\ge }$ is the variant of the Axiom of Counting which asserts that no finite set is smaller than its own set of singletons. This paper shows that ${\mathrm{N}\mathrm{F}\mathrm{U}}^{-\mathrm{A}\mathrm{C}}+{\mathrm{A}\mathrm{x}\mathrm{C}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{t}}_{\ge }$ proves the consistency of the Simple Theory of Types with Infinity ($\mathrm{T}\mathrm{S}\mathrm{T}\mathrm{I}$). This result implies that $\mathrm{N}\mathrm{F}+{\mathrm{A}\mathrm{x}\mathrm{C}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{t}}_{\ge }$ proves that consistency of $\mathrm{T}\mathrm{S}\mathrm{T}\mathrm{I}$, and that ${\mathrm{N}\mathrm{F}\mathrm{U}}^{-\mathrm{A}\mathrm{C}}+{\mathrm{A}\mathrm{x}\mathrm{C}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{t}}_{\ge }$ proves the consistency of ${\mathrm{N}\mathrm{F}\mathrm{U}}^{-\mathrm{A}\mathrm{C}}$.