RulGeneralisation (2.06, Inference Rule): Generalisation (admissible rule)

RulGeneralisation (2.06) — Generalisation (admissible rule)

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

Num Entity Database Record (Vertical Field Table)

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`