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}}$	$\triangleleft \ {\mathsf {PA}}$
	${\mathsf {iNF}}$		${\mathsf {T}}\mathbb {Z} {\mathsf {T}}$
$\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)$

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}}$ like ${\mathsf {NFI}}$, in which only comprehension is restricted to those formulae which can be stratified using no more than three types.

• ZF-style set theory
  • 123

• Type-style theory
  • 123

• First-order arithmetic
  • 123

Notes

^ It is not recommended to read references that are too old and can be read instead