| 5.02 |
| Title |
Gödel's second incompleteness theorem(WIP) #ThmSecondIncompleteness #label-g-del-s-second-incompleteness-theorem-wip |
| Classification |
Theorem |
| Formula |
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-eau.html}{\mathcal{E}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/neg-conn.html}{\neg} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-tau.html}{\mathcal{T}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/bot-const.html}{\bot} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/neg-conn.html}{\neg} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-tau.html}{\mathcal{T}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/neg-conn.html}{\neg} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/theory-tau.html}{\mathcal{T}} \href{../symbols/comma-delim.html}{,} \href{../symbols/empty-list-const.html}{[\,]} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/quotation.html}{\langle } \href{../symbols/bot-const.html}{\bot} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
TpHolds |
| Scheme of Types |
0(𝘌,[]⊢‹(¬(𝘛,[]⊢‹⊥›))→¬(𝘛,[]⊢‹¬(𝘛,[]⊢‹⊥›)›)›) |
| Kernel Note |
Formalized in the unspecified elementary metatheory 𝘌 ∈ {IΣ₁, PA, 𝘛, NBG, MK} (not Robinson's Q, which lacks Σ₁-induction needed for HBL condition D3; cf. Hájek & Pudlák 1993; Bezboruah & Shepherdson 1976) for the recursively enumerable object theory 𝘛. Note that Gödel's second incompleteness theorem applies to the r.e. theory 𝘛, whereas 𝘍 is non-r.e. |
| Verification |
Verified (Kernel) · Standalone Entry (ThmSecondIncompleteness) → · (5.02) · #ThmSecondIncompleteness |
|