Obelisk Proof Assistant — Verified Theorems & Inference Rules Gallery

1. Propositional Logic (1.01–1.14)

Classical propositional calculus axiom schemas (A01–A13) and Modus Ponens.

Num Entity Database Record (Vertical Field Table)

Title	Modus Ponens `#RulModusPonens` `#label-modus-ponens`
Classification	Inference Rule
Formula	0(⟦𝛂⟧, (⟦𝛂⟧→⟦𝛃⟧) ⊢ ⟦𝛃⟧) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PMP_prf`
Scheme of Types	0`(⟦[𝛂@Fm.Expression]⟧, (⟦[𝛂@Fm.Expression]⟧→⟦[𝛃@Fm.Expression]⟧) ⊢ ⟦[𝛃@Fm.Expression]⟧)`
Judgements	1[(𝛂:Fm ), (𝛃:Fm )] 1\(\href{symbols/image-op.html}{[} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/image-op.html}{]} \)
Side Condition	1⊤ 1\(\href{symbols/top-const.html}{\top} \)
Verification	Primitive / Derived Rule (Kernel) · Standalone Entry (`RulModusPonens`) → · (1.14) · `#RulModusPonens`

2. Predicate Logic (2.01–2.06)

First-order quantifier instantiation, abstraction rules, and non-empty discourse domain over Classes.

Num Entity Database Record (Vertical Field Table)

2.02

Title	Forall Instantiation `#RulForallInstantiation` `#label-forall-instantiation`
Classification	Inference Rule
Formula	0((∀(⦃x⦄:⟦X⟧)⟦𝛗⟧)→⟦𝛗[t/x]⟧) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{x} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/typing-colon.html}{:} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{X} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/image-op.html}{[} \href{symbols/variables.html}{t} \href{symbols/subst-slash.html}{/} \href{symbols/variables.html}{x} \href{symbols/image-op.html}{]} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PForaL_prf`
Scheme of Types	0`((∀([⦃[x@Variable.Expression]⦄@Variable]:[⟦[X@Type.Expression.Expression]⟧@Type])⟦[𝛗@Fm.Expression]⟧)→⟦[𝛗@Fm.Expression][[t@LCEWIP]/[x@Variable.Expression]]⟧)`
Judgements	1[(t:X.Expression ), (X:Type ), (x:Name ), (𝛗:Fm )] 1\(\href{symbols/image-op.html}{[} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{t} \href{symbols/typing-colon.html}{:} \href{symbols/variables.html}{X} \href{symbols/dot-delim.html}{.} \href{symbols/expression-sort.html}{\mathsf{Expression}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/type-sort.html}{\mathsf{Type}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/name-sort.html}{\mathsf{Name}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/image-op.html}{]} \)
Side Condition	1Fm .FFI ((t:X.Expression ),x,𝛗) 1\(\href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/dot-delim.html}{.} \href{symbols/ffi-pred.html}{\mathrm{FFI}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{t} \href{symbols/typing-colon.html}{:} \href{symbols/variables.html}{X} \href{symbols/dot-delim.html}{.} \href{symbols/expression-sort.html}{\mathsf{Expression}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/delimiters-brackets.html}{)} \)
Verification	Primitive / Derived Rule (Kernel) · Standalone Entry (`RulForallInstantiation`) → · (2.02) · `#RulForallInstantiation`

2.03

Title	Exists Instantiation `#RulExistsInstantiation` `#label-exists-instantiation`
Classification	Inference Rule
Formula	0(⟦𝛗[t/x]⟧→∃(⦃x⦄:⟦X⟧)⟦𝛗⟧) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/image-op.html}{[} \href{symbols/variables.html}{t} \href{symbols/subst-slash.html}{/} \href{symbols/variables.html}{x} \href{symbols/image-op.html}{]} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{x} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/typing-colon.html}{:} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{X} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PExisR_prf`
Scheme of Types	0`(⟦[𝛗@Fm.Expression][[t@LCEWIP]/[x@Variable.Expression]]⟧→∃([⦃[x@Variable.Expression]⦄@Variable]:[⟦[X@Type.Expression.Expression]⟧@Type])⟦[𝛗@Fm.Expression]⟧)`
Judgements	1[(t:X.Expression ), (X:Type ), (x:Name ), (𝛗:Fm )] 1\(\href{symbols/image-op.html}{[} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{t} \href{symbols/typing-colon.html}{:} \href{symbols/variables.html}{X} \href{symbols/dot-delim.html}{.} \href{symbols/expression-sort.html}{\mathsf{Expression}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/type-sort.html}{\mathsf{Type}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/name-sort.html}{\mathsf{Name}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/image-op.html}{]} \)
Side Condition	1Fm .FFI ((t:X.Expression ),x,𝛗) 1\(\href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/dot-delim.html}{.} \href{symbols/ffi-pred.html}{\mathrm{FFI}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{t} \href{symbols/typing-colon.html}{:} \href{symbols/variables.html}{X} \href{symbols/dot-delim.html}{.} \href{symbols/expression-sort.html}{\mathsf{Expression}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/delimiters-brackets.html}{)} \)
Verification	Primitive / Derived Rule (Kernel) · Standalone Entry (`RulExistsInstantiation`) → · (2.03) · `#RulExistsInstantiation`

2.04

Title	Forall Abstraction `#RulForallAbstraction` `#label-forall-abstraction`
Classification	Inference Rule
Formula	0((⟦𝛃⟧→⟦𝛂⟧) ⊢ (⟦𝛃⟧→∀(⦃x⦄:⟦X⟧)⟦𝛂⟧)) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{x} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/typing-colon.html}{:} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{X} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PForaR_prf`
Scheme of Types	0`((⟦[𝛃@Fm.Expression]⟧→⟦[𝛂@Fm.Expression]⟧) ⊢ (⟦[𝛃@Fm.Expression]⟧→∀([⦃[x@Variable.Expression]⦄@Variable]:[⟦[X@Type.Expression.Expression]⟧@Type])⟦[𝛂@Fm.Expression]⟧))`
Judgements	1[(X:Type ), (x:Name ), (𝛂:Fm ), (𝛃:Fm )] 1\(\href{symbols/image-op.html}{[} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/type-sort.html}{\mathsf{Type}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/name-sort.html}{\mathsf{Name}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/image-op.html}{]} \)
Side Condition	1NFV (X,x,(𝛃:Fm )) 1\(\href{symbols/nfv-pred.html}{\mathrm{NFV}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
Verification	Primitive / Derived Rule (Kernel) · Standalone Entry (`RulForallAbstraction`) → · (2.04) · `#RulForallAbstraction`

2.05

Title	Exists Abstraction `#RulExistsAbstraction` `#label-exists-abstraction`
Classification	Inference Rule
Formula	0((⟦𝛂⟧→⟦𝛃⟧) ⊢ ((∃(⦃x⦄:⟦X⟧)⟦𝛂⟧)→⟦𝛃⟧)) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{x} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/typing-colon.html}{:} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{X} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PExisL_prf`
Scheme of Types	0`((⟦[𝛂@Fm.Expression]⟧→⟦[𝛃@Fm.Expression]⟧) ⊢ ((∃([⦃[x@Variable.Expression]⦄@Variable]:[⟦[X@Type.Expression.Expression]⟧@Type])⟦[𝛂@Fm.Expression]⟧)→⟦[𝛃@Fm.Expression]⟧))`
Judgements	1[(X:Type ), (x:Name ), (𝛂:Fm ), (𝛃:Fm )] 1\(\href{symbols/image-op.html}{[} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/type-sort.html}{\mathsf{Type}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/name-sort.html}{\mathsf{Name}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/image-op.html}{]} \)
Side Condition	1NFV (X,x,(𝛃:Fm )) 1\(\href{symbols/nfv-pred.html}{\mathrm{NFV}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
Verification	Primitive / Derived Rule (Kernel) · Standalone Entry (`RulExistsAbstraction`) → · (2.05) · `#RulExistsAbstraction`

2.06

Title	Generalisation (admissible rule) `#RulGeneralisation` `#label-generalisation-admissible-rule`
Classification	Inference Rule
Formula	0(⟦𝛂⟧ ⊢ (∀(⦃x⦄:⟦X⟧)⟦𝛂⟧)) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{x} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/typing-colon.html}{:} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{X} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PForaR_prf`
Scheme of Types	0`(⟦[𝛂@Fm.Expression]⟧ ⊢ (∀([⦃[x@Variable.Expression]⦄@Variable]:[⟦[X@Type.Expression.Expression]⟧@Type])⟦[𝛂@Fm.Expression]⟧))`
Judgements	1[(x:Name ), (X:Type ), (𝛂:Fm )] 1\(\href{symbols/image-op.html}{[} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/name-sort.html}{\mathsf{Name}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/type-sort.html}{\mathsf{Type}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/image-op.html}{]} \)
Side Condition	1⊤ 1\(\href{symbols/top-const.html}{\top} \)
Verification	Primitive / Derived Rule (Kernel) · Standalone Entry (`RulGeneralisation`) → · (2.06) · `#RulGeneralisation`

3. Set/Class-Theoretic Foundations (3.01–3.78)

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

Num Entity Database Record (Vertical Field Table)

3.01

Title	Class comprehension `#RulClassComprehension` `#label-class-comprehension`
Classification	Inference Rule
Formula	0((⦃x⦄∈{⦃x⦄\|⟦𝛗⟧})⟷((⦃x⦄ set )∧⟦𝛗⟧)) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{x} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/in-pred.html}{\in} \href{symbols/class-comprehension.html}{\{} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{x} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/class-comprehension.html}{ \mid } \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/class-comprehension.html}{\}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{x} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PComprAx_prf`
Scheme of Types	0`(([⦃[x@Variable.Expression]⦄@Class.Expression]∈{[⦃[x@Variable.Expression]⦄@Class.Expression]\|⟦[𝛗@Fm.Expression]⟧})⟷(([⦃[x@Variable.Expression]⦄@Class.Expression] set)∧⟦[𝛗@Fm.Expression]⟧))`
Judgements	1[(x:Name), (𝛗:Fm)] 1\(\href{symbols/image-op.html}{[} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/name-sort.html}{\mathsf{Name}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/image-op.html}{]} \)
Side Condition	1⊤ 1\(\href{symbols/top-const.html}{\top} \)
Verification	Primitive / Derived Rule (Kernel) · Standalone Entry (`RulClassComprehension`) → · (3.01) · `#RulClassComprehension`

3.07

Title	Example: “The empty class is a subclass of any class” statement `#ThmEmptySetIsSubclass` `#label-example-the-empty-class-is-a-subclass-of-any-class-statement`
Classification	Theorem
Formula	0(∀(X:Class)(∅⊆X)) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/emptyset-const.html}{\emptyset} \href{symbols/sub-pred.html}{\subseteq} \href{symbols/variables.html}{X} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PSubDef_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])(∅⊆[X@Class.Expression]))`
Verification	Verified (Kernel) · Standalone Entry (`ThmEmptySetIsSubclass`) → · (3.07) · `#ThmEmptySetIsSubclass`

3.11

Title	“Intensionality”(admissible) `#AxmIntensionality` `#label-intensionality-admissible`
Classification	Theorem
Formula	0(∀(X:Class)∀(Y:Class)(((X set )∧(Y set ))→((∀(W:Class)((X∈W)⟷(Y∈W)))→(X=Y)))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Y} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{W} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{W} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Y} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{W} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{Y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PEqDef_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])∀([Y@Variable]:[Class@Type])((([X@Class.Expression] set)∧([Y@Class.Expression] set))→((∀([W@Variable]:[Class@Type])(([X@Class.Expression]∈[W@Class.Expression])⟷([Y@Class.Expression]∈[W@Class.Expression])))→([X@Class.Expression]=[Y@Class.Expression]))))`
Verification	Verified (Kernel) · Standalone Entry (`AxmIntensionality`) → · (3.11) · `#AxmIntensionality`

3.18

Title	The class of all ordinals is an ordinal class `#ThmOrdinalsIsOrdinal` `#label-the-class-of-all-ordinals-is-an-ordinal-class`
Classification	Theorem
Formula	0Ord(On) 0\(\href{symbols/ord-pred.html}{\mathrm{Ord}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpOrd`
Scheme of Types	0`Ord(On)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOrdinalsIsOrdinal`) → · (3.18) · `#ThmOrdinalsIsOrdinal`

3.37

Title	Evaluation of “Family Value” via semi-singleton subsets `#ThmFamilyEvaluation` `#label-evaluation-of-family-value-via-semi-singleton-subsets`
Classification	Theorem
Formula	0(∀(F:Class)∀(x:Class)((F family )→(F(x)=⋃{s\|(x,s)∈F}))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/family-pred.html}{\mathsf{family}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/bigunion-op.html}{\bigcup} \href{symbols/class-comprehension.html}{\{} \href{symbols/variables.html}{s} \href{symbols/class-comprehension.html}{ \mid } \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{s} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{F} \href{symbols/class-comprehension.html}{\}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpValOf`
Scheme of Types	0`(∀([F@Variable]:[Class@Type])∀([x@Variable]:[Class@Type])(([F@Class.Expression] family)→([F@Class.Expression]([x@Class.Expression])=⋃{[s@Class.Expression]\|([x@Class.Expression],[s@Class.Expression])∈[F@Class.Expression]})))`
Verification	Verified (Kernel) · Standalone Entry (`ThmFamilyEvaluation`) → · (3.37) · `#ThmFamilyEvaluation`

3.39

Title	“Dependent Product (Pi-Type)” predicate and section model `#DefPiPredicateModel` `#label-dependent-product-pi-type-predicate-and-section-model`
Classification	Theorem
Formula	0(∀(B:Class)∀(f:Class)(((B family )∧((f family )∧(Dom(f)=Dom(B))))→∀(x:Class)((x∈Dom(B))→(f(x)∈B(x))))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/family-pred.html}{\mathsf{family}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/family-pred.html}{\mathsf{family}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/dom-op.html}{\mathrm{Dom}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{f} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpPi`
Scheme of Types	0`(∀([B@Variable]:[Class@Type])∀([f@Variable]:[Class@Type])((([B@Class.Expression] family)∧(([f@Class.Expression] family)∧(Dom([f@Class.Expression])=Dom([B@Class.Expression]))))→∀([x@Variable]:[Class@Type])(([x@Class.Expression]∈Dom([B@Class.Expression]))→([f@Class.Expression]([x@Class.Expression])∈[B@Class.Expression]([x@Class.Expression])))))`
Kernel Note	Explicit typed term interpretation / valuation (μ_A : A.Expression → Class.Expression) of dependent product sections Π(x:Dom(F)) over a family F in the fixed background model.
Verification	Verified (Kernel) · Standalone Entry (`DefPiPredicateModel`) → · (3.39) · `#DefPiPredicateModel`

3.58

Title	Class of all sets is successor-inductive (Peano-inductive) `#ThmUniversalClassInductive` `#label-class-of-all-sets-is-successor-inductive-peano-inductive`
Classification	Theorem
Formula	0Ind(V) 0\(\href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpInd`
Scheme of Types	0`Ind(V)`
Verification	Verified (Kernel) · Standalone Entry (`ThmUniversalClassInductive`) → · (3.58) · `#ThmUniversalClassInductive`

3.59

Title	Intersection of all successor-inductive (Peano-inductive) classes is a successor-inductive class itself (ω is the ⊆-least successor-inductive class) `#ThmOmegaInductive` `#label-intersection-of-all-successor-inductive-peano-inductive-classes-is-a-successor-inductive-class-itself-is-the-least-successor-inductive-class`
Classification	Theorem
Formula	0Ind(ω) 0\(\href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpInd`
Scheme of Types	0`Ind(ω)`
Kernel Note	Establishes that ω itself satisfies Ind(ω), making ω the ⊆-least (minimal) element among all successor-inductive classes in the ⊆ order.
Verification	Verified (Kernel) · Standalone Entry (`ThmOmegaInductive`) → · (3.59) · `#ThmOmegaInductive`

3.60

Title	Class of all ordinal numbers is successor-inductive (Peano-inductive) `#ThmOrdinalsInductive` `#label-class-of-all-ordinal-numbers-is-successor-inductive-peano-inductive`
Classification	Theorem
Formula	0Ind(On) 0\(\href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpInd`
Scheme of Types	0`Ind(On)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOrdinalsInductive`) → · (3.60) · `#ThmOrdinalsInductive`

3.61

Title	ω is transitive `#ThmOmegaTransitive` `#label-is-transitive`
Classification	Theorem
Formula	0Tr(ω) 0\(\href{symbols/trans-pred.html}{\mathrm{Tr}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpTrans`
Scheme of Types	0`Tr(ω)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOmegaTransitive`) → · (3.61) · `#ThmOmegaTransitive`

3.62

Title	ω is ordinal `#ThmOmegaOrdinal` `#label-is-ordinal`
Classification	Theorem
Formula	0Ord(ω) 0\(\href{symbols/ord-pred.html}{\mathrm{Ord}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpOrd`
Scheme of Types	0`Ord(ω)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOmegaOrdinal`) → · (3.62) · `#ThmOmegaOrdinal`

3.63

Title	ω is in the class of all ordinal numbers(=sets) `#ThmOmegaInOrdinals` `#label-is-in-the-class-of-all-ordinal-numbers-sets`
Classification	Theorem
Formula	0(ω∈On) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/in-pred.html}{\in} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpOn`
Scheme of Types	0`(ω∈On)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOmegaInOrdinals`) → · (3.63) · `#ThmOmegaInOrdinals`

3.64

Title	“Is cardinal” predicate `#DefIsCardinal` `#label-is-cardinal-predicate`
Classification	Theorem
Formula	0(∀(C:Class)(Card(C)⟷(∃(K:Class)(\|K\|=C)))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/card-pred.html}{\mathrm{Card}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/card-op.html}{ \mid } \href{symbols/variables.html}{K} \href{symbols/card-op.html}{ \mid } \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpCard`
Scheme of Types	0`(∀([C@Variable]:[Class@Type])(Card([C@Class.Expression])⟷(∃([K@Variable]:[Class@Type])(\|[K@Class.Expression]\|=[C@Class.Expression]))))`
Verification	Verified (Kernel) · Standalone Entry (`DefIsCardinal`) → · (3.64) · `#DefIsCardinal`

3.65

Title	ω is cardinal `#ThmOmegaCardinal` `#label-is-cardinal`
Classification	Theorem
Formula	0Card(ω) 0\(\href{symbols/card-pred.html}{\mathrm{Card}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpCard`
Scheme of Types	0`Card(ω)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOmegaCardinal`) → · (3.65) · `#ThmOmegaCardinal`

3.66

Title	On is a cardinal class `#ThmOrdinalsCardinal` `#label-on-is-a-cardinal-class`
Classification	Theorem
Formula	0Card(On) 0\(\href{symbols/card-pred.html}{\mathrm{Card}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpCard`
Scheme of Types	0`Card(On)`
Verification	Verified (Kernel) · Standalone Entry (`ThmOrdinalsCardinal`) → · (3.66) · `#ThmOrdinalsCardinal`

3.67

Title	Class of all sets is not a cardinal class `#ThmUniversalClassNotCardinal` `#label-class-of-all-sets-is-not-a-cardinal-class`
Classification	Theorem
Formula	0(¬Card(V)) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/neg-conn.html}{\neg} \href{symbols/card-pred.html}{\mathrm{Card}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpCard`
Scheme of Types	0`(¬Card(V))`
Verification	Verified (Kernel) · Standalone Entry (`ThmUniversalClassNotCardinal`) → · (3.67) · `#ThmUniversalClassNotCardinal`

3.69

Title	The class of all sets is a universe `#ThmUniversalClassIsUniverse` `#label-the-class-of-all-sets-is-a-universe`
Classification	Theorem
Formula	0(V universe ) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/universe-pred.html}{\mathsf{universe}} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PVUniverseAx_prf`
Scheme of Types	0`(V universe)`
Formal Kernel Proof	Step 0a (V → set, from #DefUniversalClass + #AxmLeftInSound + #RulClassComprehension): 1(𝘍,[]⊢‹∀(x:Class)((x∈V)→(x set ))›) 1\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \) Step 0b (set → V, from #DefUniversalClass + #AxmLeftInSound + #RulClassComprehension + #AxmPropVerum): 1(𝘍,[]⊢‹∀(x:Class)((x set )→(x∈V))›) 1\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \) Step 1 (ω ∈ V, from #AxmOmegaIsSet + Step 0b): 1(𝘍,[]⊢‹ω∈V›) 1\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/omega-const.html}{\omega} \href{symbols/in-pred.html}{\in} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \) Step 2 (V transitive, from #DefTransitiveClass + #DefSubclass + #DefIsSet + Step 0b): 1(𝘍,[]⊢‹Tr(V)›) 1\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/trans-pred.html}{\mathrm{Tr}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \) Step 3 (V Hereditary, from #DefHereditaryClass + #AxmHeredity + Steps 0a, 0b): 1(𝘍,[]⊢‹Hereditary(V)›) 1\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/hereditary-pred.html}{\mathsf{Hereditary}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \) Step 4 (V Powerful, from #DefPowerfulClass + #AxmExponent + Steps 0a, 0b): 1(𝘍,[]⊢‹Powerful(V)›) 1\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/powerful-pred.html}{\mathsf{Powerful}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \) Step 5 (V Tight, from #DefTightClass + #AxmSizeLimitation + #DefCardinality/#DefCardLess): 1(𝘍,[]⊢‹Tight(V)›) 1\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/tight-pred.html}{\mathsf{Tight}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \) Step 6 (V Pairful, from #DefPairfulClass + #DefUnorderedPair sethood + Steps 0a, 0b): 1(𝘍,[]⊢‹Pairful(V)›) 1\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/pairful-pred.html}{\mathsf{Pairful}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \) Step 7 (Instantiated #DefGrothendieckUniverse at U := V): 1(𝘍,[]⊢‹(V universe )⟷(((ω∈V)∧((Tr(V)∧Hereditary(V))∧(Powerful(V)∧Tight(V))))∧Pairful(V))›) 1\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/universe-pred.html}{\mathsf{universe}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/in-pred.html}{\in} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/trans-pred.html}{\mathrm{Tr}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/hereditary-pred.html}{\mathsf{Hereditary}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/powerful-pred.html}{\mathsf{Powerful}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/tight-pred.html}{\mathsf{Tight}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/pairful-pred.html}{\mathsf{Pairful}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \) Step 8 (Conclusion via PAndR_prf + def_to_intro, verified by Thm.checkPipeline & Thm.slow_check): 1(𝘍,[]⊢‹V universe ›) 1\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/universe-pred.html}{\mathsf{universe}} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \)
Kernel Note	Formal kernel proof (v_universe_thm_proof : unit -> Thm, verified by Thm.checkPipeline and Thm.slow_check) deriving (𝘍, [] ⊢ (V universe)) from 3.68 #DefGrothendieckUniverse (PKernelDef_prf) and the 6 component lemmas: (1) (ω ∈ V) via 3.57 #AxmOmegaIsSet (POmegaSetAx_prf), 3.05 #DefUniversalClass (PKernelDef_prf), 3.08 #AxmLeftInSound (PLeftInSoundAx_prf), and 3.01 #RulClassComprehension (PComprAx_prf); (2) (V transitive) via 3.15 #DefTransitiveClass (PKernelDef_prf), 3.06 #DefSubclass (PKernelDef_prf), and 3.02 #DefIsSet (PSetDef_prf); (3) (V Hereditary) via 3.44 #DefHereditaryClass (PKernelDef_prf) and 3.12 #AxmHeredity (PHeredityAx_prf); (4) (V Powerful) via 3.45 #DefPowerfulClass (PKernelDef_prf) and 3.13 #AxmExponent (PPowSetAx_prf); (5) (V Tight) via 3.47 #DefTightClass (PKernelDef_prf), 3.43 #AxmSizeLimitation (PSizeLimAx_prf), and 3.41/3.42 #DefCardinality/#DefCardLess (PCardLessOrderAx_prf); (6) (V Pairful) via 3.46 #DefPairfulClass (PKernelDef_prf) and 3.49 #DefUnorderedPair sethood (PPairSetAx_prf). Backup axiom constructor PVUniverseAx_prf (v_universe_axm_backup_entry) is also retained in the kernel just in case.
Verification	Verified (Kernel) · Standalone Entry (`ThmUniversalClassIsUniverse`) → · (3.69) · `#ThmUniversalClassIsUniverse`

3.71

Title	General form of the transfinite ∈-induction principle on a transitive class `#ThmTransitiveClassInduction` `#label-general-form-of-the-transfinite-induction-principle-on-a-transitive-class`
Classification	Theorem
Formula	0(∀(K:Class)∀(A:Class)((Tr(K)∧((K∩𝒫(A))⊆A))→(K⊆A))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/trans-pred.html}{\mathrm{Tr}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/bininter-op.html}{\cap} \href{symbols/power-op.html}{\mathcal{P}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/sub-pred.html}{\subseteq} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/sub-pred.html}{\subseteq} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PEpsIndAx_prf`
Scheme of Types	0`(∀([K@Variable]:[Class@Type])∀([A@Variable]:[Class@Type])((Tr([K@Class.Expression])∧(([K@Class.Expression]∩𝒫([A@Class.Expression]))⊆[A@Class.Expression]))→([K@Class.Expression]⊆[A@Class.Expression])))`
Kernel Note	Transfinite membership (∈) induction on a well-founded transitive class, contrasted with successor-induction (Peano 0-successor-induction Ind(X) in 3.55).
Verification	Verified (Kernel) · Standalone Entry (`ThmTransitiveClassInduction`) → · (3.71) · `#ThmTransitiveClassInduction`

3.77

Title	First projection of Dunaev's tagged ordered pair `#ThmDunaevFirstProjection` `#label-first-projection-of-dunaev-s-tagged-ordered-pair`
Classification	Theorem
Formula	0(∀(A:Class)∀(B:Class)({a\|{{{{a}}},{∅}}∈(A,B)}=A)) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/class-comprehension.html}{\{} \href{symbols/variables.html}{a} \href{symbols/class-comprehension.html}{ \mid } \href{symbols/upair-op.html}{\{} \href{symbols/singleton-op.html}{\{} \href{symbols/singleton-op.html}{\{} \href{symbols/singleton-op.html}{\{} \href{symbols/variables.html}{a} \href{symbols/singleton-op.html}{\}} \href{symbols/singleton-op.html}{\}} \href{symbols/singleton-op.html}{\}} \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/in-pred.html}{\in} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/class-comprehension.html}{\}} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpPr1`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])({[a@Class.Expression]\|{{{{[a@Class.Expression]}}},{∅}}∈([A@Class.Expression],[B@Class.Expression])}=[A@Class.Expression]))`
Kernel Note	Recovers A from (A,B) via tag 1 without requiring A or B to be sets.
Verification	Verified (Kernel) · Standalone Entry (`ThmDunaevFirstProjection`) → · (3.77) · `#ThmDunaevFirstProjection`

3.78

Title	Second projection of Dunaev's tagged ordered pair `#ThmDunaevSecondProjection` `#label-second-projection-of-dunaev-s-tagged-ordered-pair`
Classification	Theorem
Formula	0(∀(A:Class)∀(B:Class)({b\|{{{{b}}},{∅,{∅}}}∈(A,B)}=B)) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/class-comprehension.html}{\{} \href{symbols/variables.html}{b} \href{symbols/class-comprehension.html}{ \mid } \href{symbols/upair-op.html}{\{} \href{symbols/singleton-op.html}{\{} \href{symbols/singleton-op.html}{\{} \href{symbols/singleton-op.html}{\{} \href{symbols/variables.html}{b} \href{symbols/singleton-op.html}{\}} \href{symbols/singleton-op.html}{\}} \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/in-pred.html}{\in} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/class-comprehension.html}{\}} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpPr2`
Scheme of Types	0`(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])({[b@Class.Expression]\|{{{{[b@Class.Expression]}}},{∅,{∅}}}∈([A@Class.Expression],[B@Class.Expression])}=[B@Class.Expression]))`
Kernel Note	Recovers B from (A,B) via tag 2 without requiring A or B to be sets.
Verification	Verified (Kernel) · Standalone Entry (`ThmDunaevSecondProjection`) → · (3.78) · `#ThmDunaevSecondProjection`

4. Metalogical Laws (4.01–4.06)

Explicit substitution, context encoding, co-necessitation, uniqueness quantifiers, and reflected comprehension.

Num Entity Database Record (Vertical Field Table)

4.03

Title	CoNecessitation(meta,WIP) `#DefMetaConecessitation` `#label-conecessitation-meta-wip`
Classification	Inference Rule
Formula	0(∀(Γ:Ctx)∀(𝛗:Fm)((𝘍,[]⊢‹𝘍,Γ⊢𝛗›)→(𝘍,Γ⊢𝛗))) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\Gamma} \href{symbols/typing-colon.html}{:} \href{symbols/ctx-sort.html}{\mathsf{Ctx}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/formula-metavariables.html}{\Gamma} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-fau.html}{\mathcal{F}} \href{symbols/comma-delim.html}{,} \href{symbols/formula-metavariables.html}{\Gamma} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PCredo_prf`
Scheme of Types	0`(∀([Γ@Variable]:[Ctx@Type])∀([𝛗@Variable]:[Fm@Type])((𝘍,[]⊢‹𝘍,[Γ@Ctx.Expression]⊢[𝛗@Fm.Expression]›)→(𝘍,[Γ@Ctx.Expression]⊢[𝛗@Fm.Expression])))`
Kernel Note	If a formula < 𝘍,Γ⊢𝛗> is derived in 𝘍 from the empty context, then the formula 𝛗 is derived in 𝘍 from the context Γ. Why this holds for 𝘍: for an arbitrary theory 𝘞, concluding (𝘞, Γ⊢𝛗) from (𝘞, [] ⊢ <𝘞, Γ⊢𝛗>) requires 1-consistency / Σ₁-soundness of 𝘞 (and for the r.e. base theory 𝘛, asserting internal co-necessitation would by Löb's theorem 5.01 trivialize 𝘛). Because 𝘍 is a non-r.e. sound Henkin extension equipped with Soundness 3.73 ((𝘍, [] ⊢ ψ) → ⟦ψ⟧), instantiating 3.73 at ψ := <𝘍, Γ⊢𝛗> directly yields (𝘍, Γ⊢𝛗).
Verification	Primitive / Derived Rule (Kernel) · Standalone Entry (`DefMetaConecessitation`) → · (4.03) · `#DefMetaConecessitation`

5. Incompleteness-Related Statements (5.01–5.02)

Formalized Löb's theorem and Gödel's second incompleteness theorem.

Num Entity Database Record (Vertical Field Table)

5.01

Title	Löb's theorem(WIP) `#ThmLoeb` `#label-l-b-s-theorem-wip`
Classification	Theorem
Formula	0(∀(𝛗:Fm)(𝘌,[]⊢‹(𝘛,[]⊢‹(𝘛,[]⊢𝛗)→⟦𝛗⟧›)→(𝘛,[]⊢𝛗)›)) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/typing-colon.html}{:} \href{symbols/fm-sort.html}{\mathsf{Fm}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-eau.html}{\mathcal{E}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-tau.html}{\mathcal{T}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-tau.html}{\mathcal{T}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-tau.html}{\mathcal{T}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpHolds`
Scheme of Types	0`(∀([𝛗@Variable]:[Fm@Type])(𝘌,[]⊢‹(𝘛,[]⊢‹(𝘛,[]⊢[𝛗@Fm.Expression])→⟦[𝛗@Fm.Expression]⟧›)→(𝘛,[]⊢[𝛗@Fm.Expression])›))`
Kernel Note	Here 𝘌 ∈ {IΣ₁, PA, 𝘛, NBG, MK} is an unspecified elementary metatheory capable of proving the Hilbert-Bernays-Löb derivability conditions D1-D3 for the r.e. base theory 𝘛 (specifically D3, Σ₁-completeness, which requires Σ₁-induction and fails in Robinson's arithmetic Q; see Hájek & Pudlák 1993, Metamathematics of First-Order Arithmetic, Ch. I §3 & Ch. III; Bezboruah & Shepherdson 1976, JSL 41(2):503-512; Boolos 1993, The Logic of Provability, Ch. 2).
Verification	Verified (Kernel) · Standalone Entry (`ThmLoeb`) → · (5.01) · `#ThmLoeb`

5.02

Title	Gödel's second incompleteness theorem(WIP) `#ThmSecondIncompleteness` `#label-g-del-s-second-incompleteness-theorem-wip`
Classification	Theorem
Formula	0(𝘌,[]⊢‹(¬(𝘛,[]⊢‹⊥›))→¬(𝘛,[]⊢‹¬(𝘛,[]⊢‹⊥›)›)›) 0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-eau.html}{\mathcal{E}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/neg-conn.html}{\neg} \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-tau.html}{\mathcal{T}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/bot-const.html}{\bot} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/neg-conn.html}{\neg} \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-tau.html}{\mathcal{T}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/neg-conn.html}{\neg} \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-tau.html}{\mathcal{T}} \href{symbols/comma-delim.html}{,} \href{symbols/empty-list-const.html}{[\,]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/bot-const.html}{\bot} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpHolds`
Scheme of Types	0`(𝘌,[]⊢‹(¬(𝘛,[]⊢‹⊥›))→¬(𝘛,[]⊢‹¬(𝘛,[]⊢‹⊥›)›)›)`
Kernel Note	Formalized in the unspecified elementary metatheory 𝘌 ∈ {IΣ₁, PA, 𝘛, NBG, MK} (not Robinson's Q, which lacks Σ₁-induction needed for HBL condition D3; cf. Hájek & Pudlák 1993; Bezboruah & Shepherdson 1976) for the recursively enumerable object theory 𝘛. Note that Gödel's second incompleteness theorem applies to the r.e. theory 𝘛, whereas 𝘍 is non-r.e.
Verification	Verified (Kernel) · Standalone Entry (`ThmSecondIncompleteness`) → · (5.02) · `#ThmSecondIncompleteness`