On the strength of a weak variant of the axiom of counting

In this paper NFU − ACis used to denote Jensen's modification of Quine's ‘new foundations’ set theory ( NF ) fortified with a type‐level pairing function but without the axiom of choice. The axiom AxCount ≥ 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 thatNFU − AC + AxCount ≥proves the consistency of the simple theory of types with infinity ( TSTI ). This result implies that NF + AxCount ≥proves that consistency of TSTI , and thatNFU − AC + AxCount ≥proves the consistency of NFU − AC .