Obelisk Entity Database — 5. Incompleteness-Related Statements (5.01–5.02)

Formalized Löb's theorem and Gödel's second incompleteness theorem. (Generated directly from newchecker.ML via html_generator.ML).

Formula Display:

Proof Trees:

5. Incompleteness-Related Statements (5.01–5.02)

Formalized Löb's theorem and Gödel's second incompleteness theorem.

Num Entity Database Record (Vertical Field Table)

Title	Löb's theorem(WIP) `#ThmLoeb` `#label-l-b-s-theorem-wip`
Classification	Theorem
Formula	0(∀(𝛗:Fm)(𝘌,[]⊢‹(𝘛,[]⊢‹(𝘛,[]⊢𝛗)→⟦𝛗⟧›)→(𝘛,[]⊢𝛗)›)) 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/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/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/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/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \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/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/quotation.html}{\rangle } \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpHolds`
Scheme of Types	0`(∀([𝛗@Variable]:[Fm@Type])(𝘌,[]⊢‹(𝘛,[]⊢‹(𝘛,[]⊢[𝛗@Fm.Expression])→⟦[𝛗@Fm.Expression]⟧›)→(𝘛,[]⊢[𝛗@Fm.Expression])›))`
Kernel Note	Here 𝘌 ∈ {IΣ₁, PA, 𝘛, NBG, MK} is an unspecified elementary metatheory capable of proving the Hilbert-Bernays-Löb derivability conditions D1-D3 for the r.e. base theory 𝘛 (specifically D3, Σ₁-completeness, which requires Σ₁-induction and fails in Robinson's arithmetic Q; see Hájek & Pudlák 1993, Metamathematics of First-Order Arithmetic, Ch. I §3 & Ch. III; Bezboruah & Shepherdson 1976, JSL 41(2):503-512; Boolos 1993, The Logic of Provability, Ch. 2).
Verification	Verified (Kernel) · Standalone Entry (`ThmLoeb`) → · (5.01) · `#ThmLoeb`

Title	Gödel's second incompleteness theorem(WIP) `#ThmSecondIncompleteness` `#label-g-del-s-second-incompleteness-theorem-wip`
Classification	Theorem
Formula	0(𝘌,[]⊢‹(¬(𝘛,[]⊢‹⊥›))→¬(𝘛,[]⊢‹¬(𝘛,[]⊢‹⊥›)›)›) 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`