DefMetaInstantiation (4.01, Axiom): Instantiation(meta,WIP)

DefMetaInstantiation (4.01) — Instantiation(meta,WIP)

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

Num Entity Database Record (Vertical Field Table)

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`