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

Abstract

In this paper ${\mathrm{NFU}}^{-\mathrm{AC}}$ is used to denote Ronald Jensen's modification of Quine's `New Foundations' Set Theory ($\mathrm{NF}$) fortified with a type-level pairing function but without the Axiom of Choice. The axiom ${\mathrm{AxCount}}_{\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{NFU}}^{-\mathrm{AC}}+{\mathrm{AxCount}}_{\ge }$ proves the consistency of the Simple Theory of Types with Infinity ($\mathrm{TSTI}$). This result implies that $\mathrm{NF}+{\mathrm{AxCount}}_{\ge }$ proves that consistency of $\mathrm{TSTI}$, and that ${\mathrm{NFU}}^{-\mathrm{AC}}+{\mathrm{AxCount}}_{\ge }$ proves the consistency of ${\mathrm{NFU}}^{-\mathrm{AC}}$.

arXiv comment14 pages