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
	$𝖪𝖥$		$[{\mathrm{\Pi }}_2^{𝒫}-𝖳𝖲𝖳{]}^{\ast }$ $[{\mathrm{\Pi }}_2^{𝒫}-𝖳𝖲𝖳+{\mathrm{\Pi }}_1^{𝒫}-𝖠𝗆𝖻{]}^{\ast }$
	$𝖭𝖥𝖯$		$𝖳𝖳𝖯$	$▹𝖤𝖥𝖠$ $◃𝖯𝖠$
	${𝖭𝖥}_3$
	$𝖭𝖥𝖴$[A] $𝖬𝖫𝖴$		$𝖳𝖳𝖴$ $𝖳𝖲𝖳𝖴$	$⊵𝖨{\Delta }_{\mathrm{𝟢}}\mathsf{+}𝖾𝗑𝗉$ $⊵𝖤𝖥𝖠$ $◃𝖯𝖠$
$◃{\beth }_{{\omega }_1}$[B]	$𝗂𝖭𝖥$		$𝖳\mathbb{Z}𝖳$	$⊵𝖨{\Delta }_{\mathrm{𝟢}}\mathsf{+}𝖾𝗑𝗉$ $⊵𝖤𝖥𝖠$
${\beth }_{n<\omega }$ $◃{\beth }_{\omega }$	$𝖭𝖥𝖴\mathsf{+}𝖨𝗇𝖿$ $𝖬𝖫𝖴\mathsf{+}𝖨𝗇𝖿$		$𝖳𝖳𝖳\mathsf{+}𝖥𝗅𝖺𝗍𝖮𝖯$ $𝖳𝖲𝖳𝖴\mathsf{+}𝖥𝗅𝖺𝗍𝖮𝖯$
	$𝖭𝖥𝖨$		$𝖳𝖳𝖨$	${𝖹}_2$
$⊵{\beth }_{\omega }$ $◃{\beth }_{{\omega }_1}$	$𝖭𝖥$ $𝖬𝖫$	$𝖬𝖠𝖢𝖰$ $◃$(MAC + a tangled web of cardinals)	$𝖳𝖳𝖳$ $𝖳𝖲𝖳$
${\beth }_{{\beth }_{n<\omega }}$ $◃{\beth }_{{\beth }_{\omega }}$	$𝖭𝖥𝖴+\mathbb{N}𝗂𝗌𝖲𝖢$		$𝖳𝖳𝖴+\mathbb{N}𝗂𝗌𝖲𝖢$ $𝖳𝖲𝖳𝖴+\mathbb{N}𝗂𝗌𝖲𝖢$
	$𝖭𝖥𝖴\mathsf{\ast }$	${𝖹}^{-}+{\mathrm{\Sigma }}_2-𝖱𝖾𝗉𝗅𝖺𝖼𝖾𝗆𝖾𝗇𝗍$	$𝖳𝖳𝖴\mathsf{+}𝖲𝖢𝖲+\mathbb{N}𝗂𝗌𝖲𝖢$ $𝖳𝖲𝖳𝖴\mathsf{+}𝖲𝖢𝖲+\mathbb{N}𝗂𝗌𝖲𝖢$
	$𝖭𝖥𝖴𝖠$	$𝖹𝖥𝖢+n<\omega -𝖬𝖺𝗁𝗅𝗈$	$𝖳𝖳𝖴\mathsf{+}𝖨𝗇𝖿\mathsf{+}𝖠𝖢+𝖢𝗂𝗌𝖲𝖢$ $𝖳𝖲𝖳𝖴\mathsf{+}𝖨𝗇𝖿\mathsf{+}𝖠𝖢+𝖢𝗂𝗌𝖲𝖢$ ${𝖬𝖫𝖬}_{n<\omega }+𝖠𝖢$

Key

This is a list of symbols used in this table:

• $A◃B$ represents $B⊢\text{Con}(A)$
• $A⊴B$ represents $\text{Con}(B)\to \text{Con}(A)$
• $𝖨𝗇𝖿$ 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
  • $𝖪𝖥$ is a subsystem of both $𝖭𝖥$ and Zermelo set theory ${𝖹}^{-}$, axiomatized as extensionality, pair set, power set, sumset, and stratified ${\mathrm{\Delta }}_0^{𝒫}$ separation. In particular, $𝖪𝖥+\mathrm{\exists }$ Universal set $=𝖭𝖥$.
  • $𝖭𝖥𝖨$ is a subsystem of $𝖭𝖥$, axiomatized as untyped $𝖳𝖳𝖨$. In particular, $𝖭𝖥𝖨$ + Axiom of union $=𝖭𝖥$.
  • $𝖭𝖥𝖯$ is a subsystem of $𝖭𝖥$ like $𝖭𝖥𝖨$, axiomatized as untyped $𝖳𝖳𝖯$. In particular, $𝖭𝖥𝖯$ + Axiom of union $=𝖭𝖥$.
  • ${𝖭𝖥}_3$ is a subsystem of $𝖭𝖥$, 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 ${𝖭𝖥}_3$ on this row.
  • $𝖭𝖥𝖴$ see NF with urelements.^A It is not recommended to read references that are too old and can be read instead
  • $𝖬𝖫𝖴$ is $𝖬𝖫$ with urelements.
  • $𝗂𝖭𝖥$ the system of set theory that has the same nonlogical axioms as $𝖭𝖥$ but is embedded in an intuitionistic logic. $𝖨𝖭𝖥$, $𝗂𝖭𝖥$, $i𝖭𝖥$, and $𝖼𝗈𝗇𝗌𝗍𝗋𝗎𝖼𝗍𝗂𝗏𝖾𝖭𝖥$ are the same theory.^B It is not clear whether it is appropriate to put $𝗂𝖭𝖥$ on this row, because we just have $𝖭𝖥⊵𝗂𝖭𝖥⊵𝖭𝖥𝖴$ and don't have a proof for $𝗂𝖭𝖥⊵𝖧𝖠$ and $𝗂𝖭𝖥⊢𝖨𝗇𝖿$. That is, there might be a largest finite cardinal $|U|$, which would contain a finite set U that is "unenlargeable", that not exist $𝗂𝖭𝖥$ set $x\in ̸U$.
  • $𝖭𝖥$ see New Foundations#Definition.
  • $𝖬𝖫$ is the theory obtained by adding class notion to $𝖭𝖥$. Its equiconsistency with $𝖭𝖥$ implies that we cannot prove anything about classes that are not $𝖭𝖥$ sets.
  • $𝖭𝖥𝖴\mathsf{\ast }$ axiomatized as $𝖭𝖥𝖴\mathsf{+}𝖲𝖢𝖲+\mathbb{N}𝗂𝗌𝖲𝖢$
  • $𝖭𝖥𝖴𝖠$ axiomatized as $𝖭𝖥𝖴\mathsf{+}𝖨𝗇𝖿\mathsf{+}𝖠𝖢+𝖢𝗂𝗌𝖲𝖢$.

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 $⊵\text{Con}(\mathsf{\text{𝖹𝖥𝖢}})$), but when used in combination, they are indeed very strong.

• NF-style higher infinite
  • $\mathbb{N}𝗂𝗌𝖲𝖢$ or $𝖢𝗈𝗎𝗇𝗍$ is Rosser's Axiom of Counting, which asserts that the set of natural numbers is a strongly Cantorian set.
  • $𝖲𝖢𝖲$ is Axiom of strongly Cantorian separation, which asserts that for any strongly Cantorian set A and any formula $\varphi$ (not necessarily stratified) the set $\{x\in A|\varphi \}$ exists.
  • $𝖢𝗂𝗌𝖲𝖢$ or $𝖠$ is Axiom of Cantorian Sets, which asserts that Every Cantorian set is strongly Cantorian.

• ZF-style set theory
  • $𝖬𝖠𝖢𝖰$ as Mac Lane set theory $𝖬𝖠𝖢$ 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|\le n$, the first order theory of a natural model of ${𝖳𝖲𝖳}_n$ with base type $\tau (A)$ is completely determined by $A\mathrm{\setminus }{A}_n$, the n smallest elements of $A$.

• Type-style theory
  • $𝖥𝗅𝖺𝗍𝖮𝖯$ 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 $𝖠𝖢$, 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.
  • $𝖠𝗆𝖻$ 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 $𝖠𝗆𝖻$, this table omits the axiom because all $𝖳𝖲𝖳$-style type theories are consistent with $𝖠𝗆𝖻$.
  • $𝖳𝖳𝖨$ is a subsystem of $𝖳𝖳𝖳$, 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.
  • $𝖳𝖳𝖯$ is a subsystem of $𝖳𝖳𝖳$ like $𝖳𝖳𝖨$, in which only free variables are allowed to have the type of the set asserted to exist by an instance of comprehension.
  • $𝖳𝖳𝖴$ is $𝖳𝖳𝖳$ with urelements, and $𝖭𝖥𝖴$ is untyped $𝖳𝖳𝖴$.
  • $𝖳𝖲𝖳𝖴$ is $𝖳𝖲𝖳$ with urelements, and $𝖭𝖥𝖴$ is untyped $𝖳𝖲𝖳𝖴$.
  • $𝖳\mathbb{Z}𝖳$ is Simple theory of types with all integer types, it has a realizability model and computational interpretation and is therefore consistent., and $𝗂𝖭𝖥$ is untyped $𝖳\mathbb{Z}𝖳$.
  • $𝖳𝖳𝖳$ see New Foundations#Tangled Type Theory. $𝖭𝖥$ is untyped $𝖳𝖳𝖳$.
  • $𝖳𝖲𝖳$ see New Foundations#Typed Set Theory. $𝖭𝖥$ is untyped $𝖳𝖳𝖳$.

• Higher-order arithmetic
  • [todo]