Obelisk Proof Assistant — Metatheory, Explicit Substitution & Incompleteness

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

Title	Soundness of the theory 𝘛 `#AxmSoundnessOfBaseTheory` `#label-soundness-of-the-theory`
Classification	Axiom
Formula	0(∀(𝛗:Fm)((𝘛,[]⊢𝛗)→eval (𝛗))) 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/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/eval.html}{\mathsf{eval}} \href{symbols/delimiters-brackets.html}{(} \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	`TpHolds`
Scheme of Types	0`(∀([𝛗@Variable]:[Fm@Type])((𝘛,[]⊢[𝛗@Fm.Expression])→eval([𝛗@Fm.Expression])))`
Kernel Note	Local reflection / soundness schema for the recursively enumerable (r.e.) base theory of classes 𝘛: if (𝘛, [] ⊢ φ), then the explicit formula valuation ⟦φ⟧ holds in the fixed background model.
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmSoundnessOfBaseTheory`) → · (3.72) · `#AxmSoundnessOfBaseTheory`

3.73

Title	Soundness of the theory 𝘍 `#AxmSoundnessOfFullTheory` `#label-soundness-of-the-theory`
Classification	Axiom
Formula	0(∀(𝛗:Fm)((𝘍,[]⊢𝛗)→eval (𝛗))) 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/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/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/eval.html}{\mathsf{eval}} \href{symbols/delimiters-brackets.html}{(} \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]:[Fm@Type])((𝘍,[]⊢[𝛗@Fm.Expression])→eval([𝛗@Fm.Expression])))`
Kernel Note	𝘍 is a non-recursively-enumerable (non-r.e.), Henkin-complete extension of the r.e. base theory 𝘛 (𝘛 ⊆ 𝘍). Because 𝘍 is non-r.e., Gödel's incompleteness theorems do not apply to 𝘍 itself, and 𝘍 is postulated with full soundness (𝘍, [] ⊢ φ) → ⟦φ⟧.
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmSoundnessOfFullTheory`) → · (3.73) · `#AxmSoundnessOfFullTheory`

3.74

Title	Completeness of the theory 𝘍 `#AxmCompletenessOfFullTheory` `#label-completeness-of-the-theory`
Classification	Definition
Formula	0(∀(𝛗:Fm)(eval (𝛗)→(𝘍,[]⊢𝛗))) 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/eval.html}{\mathsf{eval}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \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/empty-list-const.html}{[\,]} \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	`POmnis_prf`
Scheme of Types	0`(∀([𝛗@Variable]:[Fm@Type])(eval([𝛗@Fm.Expression])→(𝘍,[]⊢[𝛗@Fm.Expression])))`
Kernel Note	Negation-completeness of the non-r.e. Henkin extension 𝘍: for every sentence φ, if ¬φ is not derivable in 𝘍, then φ is derivable in 𝘍.
Verification	Definitional (Kernel AST) · Standalone Entry (`AxmCompletenessOfFullTheory`) → · (3.74) · `#AxmCompletenessOfFullTheory`

3.75

Title	If a formula is derivable in 𝘛, then it is derivable in 𝘍 `#AxmBaseSubtheoryOfFull` `#label-if-a-formula-is-derivable-in-then-it-is-derivable-in`
Classification	Axiom
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-tau.html}{\mathcal{T}} \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/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	`TpHolds`
Scheme of Types	0`(∀([Γ@Variable]:[Ctx@Type])∀([𝛗@Variable]:[Fm@Type])((𝘛,[Γ@Ctx.Expression]⊢[𝛗@Fm.Expression])→(𝘍,[Γ@Ctx.Expression]⊢[𝛗@Fm.Expression])))`
Kernel Note	Theory extension monotonicity (𝘛 ⊆ 𝘍): every theorem of the r.e. base theory 𝘛 is also a theorem of its non-r.e. Henkin completion 𝘍.
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmBaseSubtheoryOfFull`) → · (3.75) · `#AxmBaseSubtheoryOfFull`

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

Title	Instantiation(meta,WIP) `#DefMetaInstantiation` `#label-instantiation-meta-wip`
Classification	Axiom
Formula	0(∀(A:Type)∀(G:Ctx.Expression)∀(𝛗:Fm)∀(t:eval (A).Expression)∀(v:Variable)(𝘞,⟦G⟧⊢‹(∀(⦃v⦄:⟦A⟧)⟦𝛗⟧)→(let ⟦v⟧ = ⟦t⟧ in ⟦𝛗⟧)›)) 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/type-sort.html}{\mathsf{Type}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{G} \href{symbols/typing-colon.html}{:} \href{symbols/ctx-sort.html}{\mathsf{Ctx}} \href{symbols/dot-delim.html}{.} \href{symbols/expression-sort.html}{\mathsf{Expression}} \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/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{t} \href{symbols/typing-colon.html}{:} \href{symbols/eval.html}{\mathsf{eval}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/expression-sort.html}{\mathsf{Expression}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{v} \href{symbols/typing-colon.html}{:} \href{symbols/variable-sort.html}{\mathsf{Variable}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-wau.html}{\mathcal{W}} \href{symbols/comma-delim.html}{,} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{G} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \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}{v} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/typing-colon.html}{:} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{A} \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/delimiters-brackets.html}{(} \href{symbols/substitution-let.html}{\mathbf{let}} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{v} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/eq-pred.html}{=} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{t} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/substitution-let.html}{\mathbf{in}} \href{symbols/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`ELet`
Scheme of Types	0`(∀([A@Variable]:[Type@Type])∀([G@Variable]:[Ctx.Expression@Type])∀([𝛗@Variable]:[Fm@Type])∀([t@Variable]:[eval([A@Type.Expression.Expression]).Expression@Type])∀([v@Variable]:[Variable@Type])(𝘞,⟦[G@Ctx.Expression.Expression]⟧⊢‹(∀([⦃[v@Variable.Expression]⦄@Variable]:[⟦[A@Type.Expression.Expression]⟧@Type])⟦[𝛗@Fm.Expression]⟧)→(let ⟦[v@Name.Expression]⟧ = ⟦[t@Class.Expression.Expression]⟧ in ⟦[𝛗@Fm.Expression]⟧)›))`
Verification	Postulated (Kernel Axiom) · Standalone Entry (`DefMetaInstantiation`) → · (4.01) · `#DefMetaInstantiation`

4.02

Title	Generalisation(meta,WIP) `#DefMetaGeneralisation` `#label-generalisation-meta-wip`
Classification	Axiom
Formula	0(∀(A:Type)∀(Γ:Ctx)∀(𝛗:Fm)∀(v:Variable)((¬Ctx .IFV(v,Γ))→((𝘞,Γ⊢𝛗)→(𝘞,Γ⊢‹∀(⦃v⦄: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/type-sort.html}{\mathsf{Type}} \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/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{v} \href{symbols/typing-colon.html}{:} \href{symbols/variable-sort.html}{\mathsf{Variable}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/neg-conn.html}{\neg} \href{symbols/ctx-sort.html}{\mathsf{Ctx}} \href{symbols/dot-delim.html}{.} \href{symbols/ifv-pred.html}{\mathrm{IFV}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{v} \href{symbols/comma-delim.html}{,} \href{symbols/formula-metavariables.html}{\Gamma} \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/theory-wau.html}{\mathcal{W}} \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/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/theory-wau.html}{\mathcal{W}} \href{symbols/comma-delim.html}{,} \href{symbols/formula-metavariables.html}{\Gamma} \href{symbols/turnstile-derivability.html}{\vdash} \href{symbols/quotation.html}{\langle } \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/binder-brackets.html}{\{\!\lvert } \href{symbols/variables.html}{v} \href{symbols/binder-brackets.html}{\rvert\!\}} \href{symbols/typing-colon.html}{:} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \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/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PForaR_prf`
Scheme of Types	0`(∀([A@Variable]:[Type@Type])∀([Γ@Variable]:[Ctx@Type])∀([𝛗@Variable]:[Fm@Type])∀([v@Variable]:[Variable@Type])((¬Ctx.IFV([v@Variable.Expression],[Γ@Ctx.Expression]))→((𝘞,[Γ@Ctx.Expression]⊢[𝛗@Fm.Expression])→(𝘞,[Γ@Ctx.Expression]⊢‹∀([⦃[v@Variable.Expression]⦄@Variable]:[[A@Type]@Type])⟦[𝛗@Fm.Expression]⟧›))))`
Kernel Note	(A theory 𝘞 is assumed here to contain only formulas without free variables, so the variable x has no free occurences in any formula of a set of formulas [\|Dec(Theory.Expression)(W)\|]. Here Enc(v) (μ_Variable(v) : Variable.Expression → Class.Expression) denotes the explicit typed term interpretation / valuation homomorphism mapping a typed term of sort A into a term of sort Class while respecting the fixed model and variable valuation.)
Verification	Postulated (Kernel Axiom) · Standalone Entry (`DefMetaGeneralisation`) → · (4.02) · `#DefMetaGeneralisation`

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`

4.04

Title	Quantifier “unique”(meta,WIP) `#DefAtMostOneBinder` `#label-quantifier-unique-meta-wip`
Classification	Definition
Formula	0(∀(𝛗:Fm)((!(z:Class)⟦𝛗⟧)⟷(∀(x:Class)∀(y:Class)((⟦𝛗[(x:Class.Expression)/‹z›]⟧∧(let z = y in ⟦𝛗⟧))→(x=y))))) 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/delimiters-brackets.html}{(} \href{symbols/uniq-binder.html}{!} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \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/iff-conn.html}{\longleftrightarrow} \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/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/image-op.html}{[} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/dot-delim.html}{.} \href{symbols/expression-sort.html}{\mathsf{Expression}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/subst-slash.html}{/} \href{symbols/quotation.html}{\langle } \href{symbols/variables.html}{z} \href{symbols/quotation.html}{\rangle } \href{symbols/image-op.html}{]} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/substitution-let.html}{\mathbf{let}} \href{symbols/variables.html}{z} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{y} \href{symbols/substitution-let.html}{\mathbf{in}} \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}{)} \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}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpUniq`
Scheme of Types	0`(∀([𝛗@Variable]:[Fm@Type])((!([z@Variable]:[Class@Type])⟦[𝛗@Fm.Expression]⟧)⟷(∀([x@Variable]:[Class@Type])∀([y@Variable]:[Class@Type])((⟦[𝛗@Fm.Expression][([x@Class.Expression.Expression]:Class.Expression)/‹z›]⟧∧(let z = [y@Class.Expression] in ⟦[𝛗@Fm.Expression]⟧))→([x@Class.Expression]=[y@Class.Expression])))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefAtMostOneBinder`) → · (4.04) · `#DefAtMostOneBinder`

4.05

Title	Quantifier “exists and unique”(meta,WIP) `#DefExistsUniqueBinder` `#label-quantifier-exists-and-unique-meta-wip`
Classification	Definition
Formula	0(∀(𝛗:Fm)(𝘛,[]⊢‹(∃!(x:Class)⟦𝛗⟧)⟷((∃(x:Class)⟦𝛗⟧)∧!(x:Class)⟦𝛗⟧)›)) 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-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/exists-uniq-binder.html}{\exists!} \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/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/iff-conn.html}{\longleftrightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/exists-binder.html}{\exists} \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/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/uniq-binder.html}{!} \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/antiquotation.html}{[\![ } \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/delimiters-brackets.html}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpExisUniq`
Scheme of Types	0`(∀([𝛗@Variable]:[Fm@Type])(𝘛,[]⊢‹(∃!([x@Variable]:[Class@Type])⟦[𝛗@Fm.Expression]⟧)⟷((∃([x@Variable]:[Class@Type])⟦[𝛗@Fm.Expression]⟧)∧!([x@Variable]:[Class@Type])⟦[𝛗@Fm.Expression]⟧)›))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefExistsUniqueBinder`) → · (4.05) · `#DefExistsUniqueBinder`

4.06

Title	Class comprehension axiom schema(meta,WIP) `#AxmMetaClassComprehension` `#label-class-comprehension-axiom-schema-meta-wip`
Classification	Axiom
Formula	0(∀(𝛗:Fm)∀(x:Name)∀(k:Class.Expression)(Fm .FFI((k:Class.Expression),‹x›,𝛗)→(𝘛,[]⊢‹(⟦k⟧∈{⦃x⦄\|⟦𝛗⟧})⟷((⟦k⟧ set )∧(let x = ⟦k⟧ in ⟦𝛗⟧))›))) 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/forall-binder.html}{\forall} \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/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/dot-delim.html}{.} \href{symbols/expression-sort.html}{\mathsf{Expression}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \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}{k} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/dot-delim.html}{.} \href{symbols/expression-sort.html}{\mathsf{Expression}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/quotation.html}{\langle } \href{symbols/variables.html}{x} \href{symbols/quotation.html}{\rangle } \href{symbols/comma-delim.html}{,} \href{symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \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/quotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{k} \href{symbols/antiquotation.html}{ ]\!]} \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/antiquotation.html}{[\![ } \href{symbols/variables.html}{k} \href{symbols/antiquotation.html}{ ]\!]} \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/substitution-let.html}{\mathbf{let}} \href{symbols/variables.html}{x} \href{symbols/eq-pred.html}{=} \href{symbols/antiquotation.html}{[\![ } \href{symbols/variables.html}{k} \href{symbols/antiquotation.html}{ ]\!]} \href{symbols/substitution-let.html}{\mathbf{in}} \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}{)} \href{symbols/quotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PComprAx_prf`
Scheme of Types	0`(∀([𝛗@Variable]:[Fm@Type])∀([x@Variable]:[Name@Type])∀([k@Variable]:[Class.Expression@Type])(Fm.FFI(([k@Class.Expression.Expression]:Class.Expression),‹[x@Name.Expression]›,[𝛗@Fm.Expression])→(𝘛,[]⊢‹(⟦[k@Class.Expression.Expression]⟧∈{[⦃[x@Variable.Expression]⦄@Class.Expression]\|⟦[𝛗@Fm.Expression]⟧})⟷((⟦[k@Class.Expression.Expression]⟧ set)∧(let [x@Name.Expression] = ⟦[k@Class.Expression.Expression]⟧ in ⟦[𝛗@Fm.Expression]⟧))›)))`
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmMetaClassComprehension`) → · (4.06) · `#AxmMetaClassComprehension`

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`