Löb's theorem ( $T ⊢ (□ A \to A) ⟹ T ⊢ A$ )

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.

Table of contents
- Iterated provability collapse implies the original theorem Löb's theorem
- Internal form of Löb's theorem Löb's theorem

Iterated provability collapse implies the original theorem ( $T ⊢ □^{i + j} A \to □^{i} A ⟹ T ⊢ □^{i} A$ )

For standard provability satisfying positive introspection, suppose

T ⊢ □^{j} A \to A

for some positive integer

j

. Positive introspection gives

T ⊢ □ A \to □^{j} A

, hence

T ⊢ □ A \to A

. Löb's theorem yields

T ⊢ A

. The same argument applies with an already iterated first-order sentence in place of

A

.

Internal form of Löb's theorem ( $T ⊢ □ (□ A \to A) \to □ A$ )

In the Löb's theorem proof,

T ⊢ □ D \to □ A

is obtained before any reflection assumption. Put

H = (□ A \to A)

. Propositional reasoning and the diagonal equation give

T ⊢ H \to D

. Necessitation and distribution yield

T ⊢ □ H \to □ D

, hence the displayed implication. This is the arithmetic interpretation of the Löb axiom in Gödel-Löb logic, and avoids necessitating a temporary assumption.

 Ancestors (9)

 Incoming links (13)

 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

Wikipedia Bot  1

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.

 Read the full article

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