AxmBaseSubtheoryOfFull (3.75, Axiom): If a formula is derivable in 𝘛, then it is derivable in 𝘍

Standalone kernel entity record from 3. Set/Class-Theoretic Foundations (3.01–3.78) — View in Complete Entity Database (#AxmBaseSubtheoryOfFull) →

Formula Display:

Proof Trees:

AxmBaseSubtheoryOfFull (3.75) — If a formula is derivable in 𝘛, then it is derivable in 𝘍

Morse-Kelley / Von Neumann-Bernays-Gödel class comprehension, sethood, ordinals, Dunaev pairs, cardinals, universes, and reflection.

Num Entity Database Record (Vertical Field Table)

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`