AxmCompletenessOfFullTheory (3.74, Definition): Completeness of the theory 𝘍

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

Formula Display:
Proof Trees:

AxmCompletenessOfFullTheory (3.74) — Completeness of the theory 𝘍

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

Num Entity Database Record (Vertical Field Table)
3.74
Title Completeness of the theory 𝘍 #AxmCompletenessOfFullTheory #label-completeness-of-the-theory
Classification Definition
Formula
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/delimiters-brackets.html}{(} \href{../symbols/eval.html}{\mathsf{eval}} \href{../symbols/delimiters-brackets.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-fau.html}{\mathcal{F}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \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 POmnis_prf
Scheme of Types 0(βˆ€([𝛗@Variable]:[Fm@Type])(eval([𝛗@Fm.Expression])β†’(𝘍,[]⊒[𝛗@Fm.Expression])))
Kernel Note Negation-completeness of the non-r.e. Henkin extension 𝘍: for every sentence Ο†, if ¬φ is not derivable in 𝘍, then Ο† is derivable in 𝘍.
Verification Definitional (Kernel AST) · Standalone Entry (AxmCompletenessOfFullTheory) → · (3.74) · #AxmCompletenessOfFullTheory