DefMetaGeneralisation (4.02, Axiom): Generalisation(meta,WIP)

DefMetaGeneralisation (4.02) — Generalisation(meta,WIP)

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

Num Entity Database Record (Vertical Field Table)

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`