| Title |
Soundness of the theory π #AxmSoundnessOfFullTheory #label-soundness-of-the-theory |
| Classification |
Axiom |
| 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/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/impl-conn.html}{\rightarrow} \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/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
PCredo_prf |
| Scheme of Types |
0(β([π@Variable]:[Fm@Type])((π,[]β’[π@Fm.Expression])βeval([π@Fm.Expression]))) |
| Kernel Note |
π is a non-recursively-enumerable (non-r.e.), Henkin-complete extension of the r.e. base theory π (π β π). Because π is non-r.e., GΓΆdel's incompleteness theorems do not apply to π itself, and π is postulated with full soundness (π, [] β’ Ο) β β¦Οβ§. |
| Verification |
Postulated (Kernel Axiom) · Standalone Entry (AxmSoundnessOfFullTheory) → · (3.73) · #AxmSoundnessOfFullTheory |