User:Edisonabcd/Sandbox

Table of the consistency strength about NF-style theory

Table of the consistency strength about NF-style theory

Beth number	NF-style set theory	ZF-style set theory	Typed-style theory	Higher-order arithmetic
	${\mathsf {KF}}$		$[\Pi _{2}^{\mathcal {P}}-{\mathsf {TST}}]^{*}$ $[\Pi _{2}^{\mathcal {P}}-{\mathsf {TST}}+\Pi _{1}^{\mathcal {P}}-{\mathsf {Amb}}]^{*}$
	${\mathsf {NFP}}$		${\mathsf {TTP}}$	$\triangleright \ {\mathsf {EFA}}$ $\triangleleft \ {\mathsf {PA}}$
	${\mathsf {NF}}_{3}$
	${\mathsf {NFU}}$[A] ${\mathsf {MLU}}$		${\mathsf {TTU}}$ ${\mathsf {TSTU}}$	$\trianglerighteq \ {\mathsf {I\Delta _{0}+exp}}$ $\trianglerighteq \ {\mathsf {EFA}}$ $\triangleleft \ {\mathsf {PA}}$
$\triangleleft \ \beth _{\omega _{1}}$[B]	${\mathsf {iNF}}$		${\mathsf {T}}\mathbb {Z} {\mathsf {T}}$	$\trianglerighteq \ {\mathsf {I\Delta _{0}+exp}}$ $\trianglerighteq \ {\mathsf {EFA}}$
$\beth _{n<\omega }$ $\triangleleft \ \beth _{\omega }$	${\mathsf {NFU+Inf}}$ ${\mathsf {MLU+Inf}}$		${\mathsf {TTT+FlatOP}}$ ${\mathsf {TSTU+FlatOP}}$
	${\mathsf {NFI}}$		${\mathsf {TTI}}$	${\mathsf {Z}}_{2}$
$\trianglerighteq \beth _{\omega }$ $\triangleleft \ \beth _{\omega _{1}}$	${\mathsf {NF}}$ ${\mathsf {ML}}$	${\mathsf {MACQ}}$ $\triangleleft \$(MAC + a tangled web of cardinals)	${\mathsf {TTT}}$ ${\mathsf {TST}}$
$\beth _{\beth _{n<\omega }}$ $\triangleleft \ \beth _{\beth _{\omega }}$	${\mathsf {NFU}}+\mathbb {N} {\mathsf {\ is\ SC}}$		${\mathsf {TTU}}+\mathbb {N} {\mathsf {\ is\ SC}}$ ${\mathsf {TSTU}}+\mathbb {N} {\mathsf {\ is\ SC}}$
	${\mathsf {NFU*}}$	${\mathsf {Z}}^{-}+\Sigma _{2}\!-\!{\mathsf {Replacement}}$	${\mathsf {TTU+SCS}}+\mathbb {N} {\mathsf {\ is\ SC}}$ ${\mathsf {TSTU+SCS}}+\mathbb {N} {\mathsf {\ is\ SC}}$
	${\mathsf {NFUA}}$	${\mathsf {ZFC}}+n<\omega -{\mathsf {Mahlo}}$	${\mathsf {TTU+Inf+AC}}+{\mathsf {C\ is\ SC}}$ ${\mathsf {TSTU+Inf+AC}}+{\mathsf {C\ is\ SC}}$ ${\mathsf {MLM}}_{n<\omega }+{\mathsf {AC}}$

Key

This is a list of symbols used in this table:

• $A\triangleleft \ B$ represents $B\vdash {\text{Con}}(A)$
• $A\trianglelefteq B$ represents ${\text{Con}}(B)\to {\text{Con}}(A)$
• ${\mathsf {Inf}}$ in this table only denotes "exist a Dedekind infinite set".

All theories that do not have sufficient information to infer their consistency strength ordering, but whose consistency proofs are explicit, are colored yellow.

This is a list of the abbreviations used in this table:

• NF-style set theory
  • ${\mathsf {KF}}$ is a subsystem of both ${\mathsf {NF}}$ and Zermelo set theory ${\mathsf {Z}}^{-}$, axiomatized as extensionality, pair set, power set, sumset, and stratified $\Delta _{0}^{\mathcal {P}}$ separation. In particular, ${\mathsf {KF}}+\exists$ Universal set $={\mathsf {NF}}$.
  • ${\mathsf {NFI}}$ is a subsystem of ${\mathsf {NF}}$, axiomatized as untyped ${\mathsf {TTI}}$. In particular, ${\mathsf {NFI}}$ + Axiom of union $={\mathsf {NF}}$.
  • ${\mathsf {NFP}}$ is a subsystem of ${\mathsf {NF}}$ like ${\mathsf {NFI}}$, axiomatized as untyped ${\mathsf {TTP}}$. In particular, ${\mathsf {NFP}}$ + Axiom of union $={\mathsf {NF}}$.
  • ${\mathsf {NF}}_{3}$ is a subsystem of ${\mathsf {NF}}$, in which only comprehension is restricted to those formulae which can be stratified using no more than three types. It is not clear whether it is appropriate to put ${\mathsf {NF}}_{3}$ on this row.
  • ${\mathsf {NFU}}$ see NF with urelements.^A It is not recommended to read references that are too old and can be read instead
  • ${\mathsf {MLU}}$ is ${\mathsf {ML}}$ with urelements.
  • ${\mathsf {iNF}}$ the system of set theory that has the same nonlogical axioms as ${\mathsf {NF}}$ but is embedded in an intuitionistic logic. ${\mathsf {INF}}$, ${\mathsf {iNF}}$, $i{\mathsf {NF}}$, and ${\mathsf {constructive\ NF}}$ are the same theory.^B It is not clear whether it is appropriate to put ${\mathsf {iNF}}$ on this row, because we just have ${\mathsf {NF}}\trianglerighteq {\mathsf {iNF}}\trianglerighteq {\mathsf {NFU}}$ and don't have a proof for ${\mathsf {iNF}}\trianglerighteq {\mathsf {HA}}$ and ${\mathsf {iNF}}\vdash {\mathsf {Inf}}$. That is, there might be a largest finite cardinal $|U|$, which would contain a finite set U that is "unenlargeable", that not exist ${\mathsf {iNF}}$ set $x\not \in U$.
  • ${\mathsf {NF}}$ see New Foundations#Definition.
  • ${\mathsf {ML}}$ is the theory obtained by adding class notion to ${\mathsf {NF}}$. Its equiconsistency with ${\mathsf {NF}}$ implies that we cannot prove anything about classes that are not ${\mathsf {NF}}$ sets.
  • ${\mathsf {NFU*}}$ axiomatized as ${\mathsf {NFU+SCS}}+\mathbb {N} {\mathsf {\ is\ SC}}$
  • ${\mathsf {NFUA}}$ axiomatized as ${\mathsf {NFU+Inf+AC}}+{\mathsf {C\ is\ SC}}$.

The axioms listed below are higher infinite axioms specific to NF-style set theory, and they also apply to NF-style type theory. When used individually, they are not necessarily very strong in the traditional sense (such as $\trianglerighteq {\text{Con}}({\textsf {ZFC}})$), but when used in combination, they are indeed very strong.

• NF-style higher infinite
  • $\mathbb {N} {\mathsf {\ is\ SC}}$ or ${\mathsf {Count}}$ is Rosser's Axiom of Counting, which asserts that the set of natural numbers is a strongly Cantorian set.
  • ${\mathsf {SCS}}$ is Axiom of strongly Cantorian separation, which asserts that for any strongly Cantorian set A and any formula $\phi$ (not necessarily stratified) the set $\{x\in A|\;\phi \}$ exists.
  • ${\mathsf {C\ is\ SC}}$ or ${\mathsf {A}}$ is Axiom of Cantorian Sets, which asserts that Every Cantorian set is strongly Cantorian.

• ZF-style set theory
  • ${\mathsf {MACQ}}$ as Mac Lane set theory ${\mathsf {MAC}}$ with foundation weakened to allow Quine atoms and an axiom scheme asserting the existence of an n-tree of cardinals for each concrete natural number n.
  • A tangled web of cardinals is, by article, a tangled web of cardinals of order $\tau$. For any infinite ordinal $\alpha$, a tangled web of cardinals of order $\alpha$ is a function $\tau$ from the set of nonempty sets of ordinals with $\alpha$ as maximum to cardinals such that

1. If $|A|>1,\tau (A_{1})=2^{\tau (A)}$.
2. If $|A|\leq n$, the first order theory of a natural model of ${\mathsf {TST}}_{n}$ with base type $\tau (A)$ is completely determined by $A\backslash A_{n}$, the n smallest elements of $A$.

• Type-style theory
  • ${\mathsf {FlatOP}}$ see New Foundations#Ordered pairs, is Axiom of type-level ordered pair, which can also be called flat ordered pair. In models without the Axiom of Choice ${\mathsf {AC}}$, the existence of a type-level ordered pair implies but is not equivalent to the existence of an infinite set, but NFU with the axiom "there is an infinite set" interprets NFU with a type-level pair in a straightforward manner.. It's well-known that proofs concerning like $\alpha$-strong cardinals run into problems if one doesn't use the flat ordered pair, and this is no different from ZF-style set theory.
  • ${\mathsf {Amb}}$ is typical ambiguity axiom, which asserts that validity for closed predicates is invariant under shifts of type levels. Unless it is necessary to refer to a restricted version of ${\mathsf {Amb}}$, this table omits the axiom because all ${\mathsf {TST}}$-style type theories are consistent with ${\mathsf {Amb}}$.
  • ${\mathsf {TTI}}$ is a subsystem of ${\mathsf {TTT}}$, axiomatized as unrestricted extensionality and those instances of comprehension in which no variable is assigned a type higher than that of the set asserted to exist.
  • ${\mathsf {TTP}}$ is a subsystem of ${\mathsf {TTT}}$ like ${\mathsf {TTI}}$, in which only free variables are allowed to have the type of the set asserted to exist by an instance of comprehension.
  • ${\mathsf {TTU}}$ is ${\mathsf {TTT}}$ with urelements, and ${\mathsf {NFU}}$ is untyped ${\mathsf {TTU}}$.
  • ${\mathsf {TSTU}}$ is ${\mathsf {TST}}$ with urelements, and ${\mathsf {NFU}}$ is untyped ${\mathsf {TSTU}}$.
  • ${\mathsf {T}}\mathbb {Z} {\mathsf {T}}$ is Simple theory of types with all integer types, it has a realizability model and computational interpretation and is therefore consistent., and ${\mathsf {iNF}}$ is untyped ${\mathsf {T}}\mathbb {Z} {\mathsf {T}}$.
  • ${\mathsf {TTT}}$ see New Foundations#Tangled Type Theory. ${\mathsf {NF}}$ is untyped ${\mathsf {TTT}}$.
  • ${\mathsf {TST}}$ see New Foundations#Typed Set Theory. ${\mathsf {NF}}$ is untyped ${\mathsf {TTT}}$.

• Higher-order arithmetic
  • [todo]