AxmMetaClassComprehension (4.06, Axiom): Class comprehension axiom schema(meta,WIP)

AxmMetaClassComprehension (4.06) — Class comprehension axiom schema(meta,WIP)

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

Num Entity Database Record (Vertical Field Table)

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`