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

TL;DR

This paper demonstrates that a weak variant of the Axiom of Counting within a modified set theory proves the consistency of the Simple Theory of Types with Infinity, linking it to the consistency of related set theories.

Contribution

It shows that a specific weak form of the Axiom of Counting can prove the consistency of TSTI within a modified NFU framework.

Findings

NFU^{-AC} + AxCount_≥ proves TSTI's consistency

NF + AxCount_≥ proves TSTI's consistency

NFU^{-AC} + AxCount_≥ proves NFU^{-AC}'s consistency

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}_\geq$ 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}_\geq$ proves the consistency of the Simple Theory of Types with Infinity ($\mathrm{TSTI}$). This result implies that $\mathrm{NF}+\mathrm{AxCount}_\geq$ proves that consistency of $\mathrm{TSTI}$, and that $\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq$ proves the consistency of $\mathrm{NFU}^{-\mathrm{AC}}$.