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

2016/01/16 by McKenzie, Zachiri
#FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.1601.04168

Abstract

In this paper NFU^-AC is used to denote Ronald 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.

Related

• Automorphisms of models of set theory and extensions of NFU
• The Church numbers in NF set theory
• Finite Sets and Counting
• NF is Consistent
• The consistency strength of NFUB