 Home

Codex Wiki

Mathematics

Area of mathematics

Foundations of mathematics

Mathematical logic

First-order logic

First-order theory

Gödel numbering

Arithmetical provability predicate

Löb's theorem

{c}
{title2=$T\vdash\Box(\Box A\to A)\to\Box A$}

In the <Löb's theorem> proof, $T\vdash\Box D\to\Box A$ is obtained before any reflection assumption. Put $H=(\Box A\to A)$. Propositional reasoning and the diagonal equation give $T\vdash H\to D$. Necessitation and distribution yield $T\vdash\Box H\to\Box 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.

Internal form of Löb's theorem

Arithmetical soundness of GL

Necessitation rule

Past exam of the Gödel's incompleteness theorems course of the University of Oxford / 2011 / 2 / a / Solution

Past exam of the Gödel's incompleteness theorems course of the University of Oxford / 2011 / 3 / b / Solution

Provability logic

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

 Ancestors (10)

 Incoming links (5)

 Discussion (0) New discussion

 Articles by others on the same topic (0)

Internal form of Löb's theorem (T⊢□(□A→A)→□A)

 Ancestors (10)

 Incoming links (5)

 Discussion (0)  Subscribe (1) New discussion

 Articles by others on the same topic (0)

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

 Discussion (0) New discussion