## You are here

HomeL\"ob's theorem

## Primary tabs

# Löb’s theorem

# Löb’s theorem

In this short article we will provide an example where one’s intuition can be faulty, and that strict formalization is always needed when one does mathematics in order to avoid possible hidden intuitive inconsistencies. A striking example is the erroneous but intuitively obvious thesis: ”if a formal system $F$ proves that there exists proof of formula $A$ in $F$, then $F$ has proved $A$” or slightly differently version is this one: ”it must be always provable in all formal systems that from formula saying that there exists proof of $A$ in $F$, indeed follows $A$ in $F$”. Both formulations of this naive intuition concerning basics of math logic severely fail. We will show that a consistent $F$ cannot prove for arbitrary formula $\phi_{{n}}$ that from formula that asserts “exists proof of $\phi_{{n}}$” follows $\phi_{{n}}$. This is a major ingredient of a theorem proved by Löb in 1955.

Löb’s theorem: If $F\vdash\exists xP(x,\check{n})\Rightarrow\phi_{{n}}$, where $x$ is the Gödel number of the proof of the formula with Gödel number $n$, and $\check{n}$ is the numeral of the Gödel number of the formula $\phi_{{n}}$, then $F\vdash\phi_{{n}}$.

The proof presented here follows Karlis Podnieks (2006):

Suppose $F\vdash\exists xP(x,\check{n})\Rightarrow\phi_{{n}}$. Let $F^{{*}}$ be the new proof system that is equal to $F$ plus the new axiom $\neg\phi_{{n}}$. By modus tollens $F^{{*}}\vdash\neg\phi_{{n}}\Rightarrow\neg\exists xP(x,\check{n})$. Since $F^{{*}}$ has as axiom $\neg\phi_{{n}}$ by modus ponens $F^{{*}}\vdash\neg\exists xP(x,\check{n})$. In this case $F^{{*}}$ proves that $\phi_{{n}}$ is not provable in $F$ (and also that $F$ is consistent). This however leads to proof that $F^{{*}}$ is also consistent because it contains only $F$ and $\neg\phi_{{n}}$, and we already know both that $F$ is consistent and that $F$ does not prove $\phi_{{n}}$. Thus $F^{{*}}$ proves its own consistency. According to Gödel’s second theorem however $F^{{*}}$ cannot prove its own consistency unless being inconsistent. Therefore $F+\neg\phi_{{n}}$ must be always inconsistent theory, and we conclude that $F\vdash\phi_{{n}}$.

Now see that the intuitive notion that $\exists xP(x,\check{n})\Rightarrow\phi_{{n}}$ is not provable within arbitrary formal system. If the formal system is inconsistent obviously it proves every formula so the above intuitive
notion will be provable. If however $F$ is consistent it cannot prove $\exists xP(x,\check{n})\Rightarrow\phi_{{n}}$ for arbitrary formula, because *if it could*, for formally refutable formula $\phi_{{k}}\equiv[0=1]$, $F$ *could* prove by modus tollens $\neg\phi_{{k}}\Rightarrow\neg\exists xP(x,\check{k})$, and since $\neg\phi_{{k}}$ is formally provable formula, then the formal system *could* infer its own consistency, or said in ordinary language: from $\neg\phi_{{k}}$, $F$ *could* have proved ”there exists at least one unprovable formula in $F$”, which is impossible according to Gödel’s second theorem.

Corollary: If $F$ is consistent formal system then $F$ cannot prove for arbitrary formula $\phi_{{n}}$ that from formula that asserts “exists proof of $\phi_{{n}}$” follows $\phi_{{n}}$.

The proof of the corollary is straigthforward either directly from Löb’s theorem, or by independent reasoning using the fact that consistent $F$ cannot prove $\exists xP(x,\check{n})\Rightarrow\phi_{{k}}$ for refutable $\phi_{{k}}$.

The relationship between the direct text of Löb’s theorem in the proof provided by Podnieks, and the corrolary is this one: if the system $F$ is consistent, it might be able to prove $\exists xP(x,\check{n})\Rightarrow\phi_{{n}}$ for provable formulas $\phi_{{n}}$, because the provability of $\phi_{{n}}$ taken together with the consistency of $F$ ensure unprovability of $\neg\phi_{{n}}$ and hence modus tollens reversed formula of $\exists xP(x,\check{n})\Rightarrow\phi_{{n}}$ cannot be used for $F$ to prove its own consistency. Also taking into account the second Gödel theorem it is easy to be seen that $F$ should not be able to prove $\exists xP(x,\check{n})\Rightarrow\phi_{{k}}$ for disprovable (refutable) formulas $\phi_{{k}}$, a result that alone is sufficient to prove the corollary. Still the corollary is a weaker result than Löb’s theorem, because the corrolary does not give us clue whether $\exists xP(x,\check{n})\Rightarrow\phi_{{p}}$ is provable for undecidable formulas $\phi_{{p}}$. This was indeed the ”open problem” proposed by Leon Henkin. The Löb’s theorem answers this question, and shows that it is impossible for consistent $F$ to prove $\exists xP(x,\check{n})\Rightarrow\phi_{{p}}$ for undecidable formulas $\phi_{{p}}$. Therefore summarized, Löb’s theorem says that for refutable or undecidable formulas $\phi$, the intuition ”if “exists proof of $\phi$” then $\phi$” is erroneous.

Modus tollens inversed Löb’s theorem: If $F$ is consistent formal system then $F$ cannot prove for any unprovable formula $\phi_{{k}}$ that from formula that asserts “exists proof of $\phi_{{k}}$” follows $\phi_{{k}}$.

Comparing the above theorem with the corrolary shows small but significant difference, which makes it stronger proposition (note: in consistent formal system $F$ unprovable formulas are all refutable (disprovable) formulas, as well as all undecidable formulas).

1. Crossley JN, Brickhill C, Ash C, Stillwell J, Williams
N (1972) *What is mathematical logic?* Oxford University Press.

2. Detlovs V, Podnieks K (2006) *Introduction to
Mathematical Logic*. Hypertextbook for students in mathematical logic

3. Gödel K (1931) Über formal unentscheidbare Sätze der
Principia Mathematica und verwandter Systeme I. *Monatshefte
für Mathematik und Physik* 38: 173-198.

4. Löb MH (1955) Solution of a Problem of Leon Henkin.
*The Journal of Symbolic Logic* 20(2): 115-118.

## Mathematics Subject Classification

03F03*no label found*03F45

*no label found*03F40

*no label found*

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff

## Recent Activity

new question: Prove a formula is part of the Gentzen System by LadyAnne

Mar 30

new question: A problem about Euler's totient function by mbhatia

new problem: Problem: Show that phi(a^n-1), (where phi is the Euler totient function), is divisible by n for any natural number n and any natural number a >1. by mbhatia

new problem: MSC browser just displays "No articles found. Up to ." by jaimeglz

Mar 26

new correction: Misspelled name by DavidSteinsaltz

Mar 21

new correction: underline-typo by Filipe

Mar 19

new correction: cocycle pro cocyle by pahio

Mar 7

new image: plot W(t) = P(waiting time <= t) (2nd attempt) by robert_dodier

new image: expected waiting time by robert_dodier

new image: plot W(t) = P(waiting time <= t) by robert_dodier