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

Abstract

In this paper NFU-AC is 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 that NFU-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 that NFU-AC + AxCount>_ proves the consistency of NFU-AC.