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 {NFI}}$		${\mathsf {TTTI}}$	$\triangleright \ {\mathsf {Z}}_{2}$ $\triangleleft \ {\mathsf {Z}}_{3}$
	${\mathsf {NFP}}$		${\mathsf {TTTP}}$	$\triangleright \ {\mathsf {EFA}}$ $\triangleleft \ {\mathsf {PA}}$
	${\mathsf {NF}}_{3}$
$\beth _{n<\omega }$	${\mathsf {NFU}}$ ${\mathsf {MLU}}$	$\mathrm {KPu} ^{r}$p. 878	${\mathsf {TTTU}}$ ${\mathsf {TSTU}}$	$\trianglerighteq \ {\mathsf {(I\Delta _{0}+exp)=EFA}}$ $\triangleleft \ {\mathsf {PA}}$
$\triangleleft \ \beth _{\omega _{1}}$	${\mathsf {iNF}}$		${\mathsf {T}}\mathbb {Z} {\mathsf {T}}$	$\trianglerighteq \ {\mathsf {(I\Delta _{0}+exp)=EFA}}$
$\beth _{\omega }$	${\mathsf {NFU+Inf}}$ ${\mathsf {MLU+Inf}}$		${\mathsf {TTTU+Inf}}$ ${\mathsf {TSTU+Inf}}$
$\trianglerighteq \beth _{\omega }$ $\triangleleft \ \beth _{\omega _{1}}$	${\mathsf {NF}}$ ${\mathsf {ML}}$	${\mathsf {MACQ}}$ $\triangleleft \$(MAC + Tangled web of cardinal)	${\mathsf {TTT}}$ ${\mathsf {TST}}$

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".

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. Adding the assertion of the existence of the universal set to KF yields NF exactly.
  • ${\mathsf {NFI}}$ is a subsystem of ${\mathsf {NF}}$, 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 {NFP}}$ is a subsystem of ${\mathsf {NF}}$ like ${\mathsf {NFI}}$, in which only free variables are allowed to have the type of the set asserted to exist by an instance of comprehension.
  • ${\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.
  • ${\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

• ZF-style set theory
  • 123

• Type-style theory
  • 123

• First-order arithmetic
  • 123