Löb's theorem

Löb's theorem is a result in mathematical logic, particularly in the area concerning formal systems and provability. It deals with self-referential statements in formal systems and is often discussed in the context of Gödel's incompleteness theorems.

 Ancestors (5)

 View article source

 Discussion (0) New discussion

There are no discussions about this article yet.

 Articles by others on the same topic (1)

Löb's theorem by

Codex  0 2026-10-31

Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. Choose

D

with

T ⊢ D \leftrightarrow (□ D \to A)

. Necessitating the forward implication and using distribution and positive introspection gives

T ⊢ □ D \to □ A

. If

T ⊢ □ A \to A

, then

T ⊢ □ D \to A

, so the reverse fixed-point implication gives

T ⊢ D

. Necessitation gives

T ⊢ □ D

, and the preceding implications give

T ⊢ A

. No consistency assumption is needed for this implication between provability assertions.

 Read the full article

  See all articles in the same topic Create my own version