DefNaturalNumberModels (3.50, Definition): Set-theoretic models of natural numbers(TBI)

Standalone kernel entity record from 3. Set/Class-Theoretic Foundations (3.01–3.78) — View in Complete Entity Database (#DefNaturalNumberModels) →

Formula Display:

Proof Trees:

DefNaturalNumberModels (3.50) — Set-theoretic models of natural numbers(TBI)

Morse-Kelley / Von Neumann-Bernays-Gödel class comprehension, sethood, ordinals, Dunaev pairs, cardinals, universes, and reflection.

Num Entity Database Record (Vertical Field Table)

Title	Set-theoretic models of natural numbers(TBI) `#DefNaturalNumberModels` `#label-set-theoretic-models-of-natural-numbers-tbi`
Classification	Definition
Formula	0((0 :Class ) = ∅) ∧ (((1 :Class ) = {∅}) ∧ (((2 :Class ) = {∅,{∅}}) ∧ ((3 :Class ) = {∅,{∅},{∅,{∅}}}))) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/numeral-0.html}{0} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/numeral-1.html}{1} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/numeral-2.html}{2} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/numeral-3.html}{3} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpNatModel`
Scheme of Types	0`((0:Class) = ∅) ∧ (((1:Class) = {∅}) ∧ (((2:Class) = {∅,{∅}}) ∧ ((3:Class) = {∅,{∅},{∅,{∅}}})))`
Kernel Note	Explicit typed term interpretation / valuation (μ_Nat : Nat.Expression → Class.Expression) mapping numeral terms 0, 1, 2, 3 into their von Neumann ordinal classes in the fixed background model.
Verification	Definitional (Kernel AST) · Standalone Entry (`DefNaturalNumberModels`) → · (3.50) · `#DefNaturalNumberModels`