Löb's theorem

The set of Loeb is a result of mathematical logic , that of Martin Loeb was proved 1955th It says that in a theory T , which fulfills certain simple properties and can represent the provability in T , for every formula P the statement “if P is provable, then P ” is only provable if P is provable. Formally:

if then ${\displaystyle T\vdash (Bew_{T}(\#P)\rightarrow P)}$ ${\displaystyle T\vdash P}$

where means that the formula P can be proven in T. (#P is the term assigned to the Gödel number of P. ) The prerequisites of the theorem are fulfilled in all sufficiently powerful mathematical theories such as Peano arithmetic and Zermelo-Fraenkel set theory . The proposition plays an important role in the logic of provability . ${\displaystyle Bew_{T}(\#P)}$

proof

requirements

Instead of considering provability in a certain theory, Löb's theorem can be shown starting from a few abstract properties of provability. A predicate B is called a provability predicate for a theory T if it fulfills the following three conditions for all formulas : ${\displaystyle \varphi ,\psi }$

1. If then ${\displaystyle T\vdash \varphi }$ ${\displaystyle T\vdash B(\#\varphi )}$
2. ${\displaystyle T\vdash B(\#(\varphi \rightarrow \psi ))\rightarrow (B(\#\varphi )\rightarrow B(\#\psi ))}$
3. ${\displaystyle T\vdash B(\#\varphi )\rightarrow B(\#B(\#\varphi ))}$

It can be shown that a standard representation of provability in a theory like Peano arithmetic or set theory fulfills these three requirements and is therefore a provability predicate.

Now let T be a theory that has the following properties:

• T has a Beweisbarkeitsprädikat B .
• Diagonalization: In T, every formula with a free variable has a fixed point in the following sense: If a formula with a free variable x , then there is a formula such that:, that is, has the intuitive meaning "I have the property ." ${\displaystyle \varphi (x)}$ ${\displaystyle \psi }$ ${\displaystyle T\vdash \psi \leftrightarrow \varphi (\#\psi )}$ ${\displaystyle \psi }$ ${\displaystyle \varphi (x)}$

proof

With the given conditions, Löb's theorem can be proven as follows:

1. Be a formula with ${\displaystyle \varphi }$ ${\displaystyle T\vdash B(\#\varphi )\rightarrow \varphi }$
2. By diagonalization, the formula is converted into a formula with ${\displaystyle (B(x)\rightarrow \varphi )}$ ${\displaystyle \psi }$ ${\displaystyle T\vdash \psi \leftrightarrow (B(\#\psi )\rightarrow \varphi )}$
3. Because of axiom 1 is ${\displaystyle T\vdash B(\#(\psi \rightarrow (B(\#\psi )\rightarrow \varphi )))}$
4. Because of axiom 2 is ${\displaystyle T\vdash B(\#(\psi \rightarrow (B(\#\psi )\rightarrow \varphi )))\rightarrow (B(\#\psi )\rightarrow B(\#B(\#\psi )\rightarrow \varphi ))}$
5. From 3 and 4 it follows: ${\displaystyle T\vdash B(\#\psi )\rightarrow B(\#(B(\#\psi )\rightarrow \varphi )))}$
6. Because of 2 and axiom 2: ${\displaystyle T\vdash B(\#(B(\#\psi )\rightarrow \varphi ))\rightarrow (B(\#B(\#\psi ))\rightarrow B(\#\varphi ))}$
7. From 5 and 6 it follows: ${\displaystyle T\vdash B(\#\psi )\rightarrow (B(\#B(\#\psi ))\rightarrow B(\#\varphi ))}$
8. Because of axiom 3: ${\displaystyle T\vdash B(\#\psi )\rightarrow B(\#B(\#\psi ))}$
9. From 7 and 8 it follows: ${\displaystyle T\vdash B(\#\psi )\rightarrow B(\#\varphi )}$
10. From 1 and 9 it follows: ${\displaystyle T\vdash B(\#\psi )\rightarrow \varphi }$
11. From 2 and 10 it follows: ${\displaystyle T\vdash \psi }$
12. Because of axiom 1: ${\displaystyle T\vdash B(\#\psi )}$
13. From 10 and 12 it now follows: ${\displaystyle T\vdash \varphi }$

Applications

• A Henkinsatz is a sentence that expresses its own provability. Löb's theorem shows that every Henkinsatz (insofar as it can be proven that it is one) is provable. Because if there is a Henkinsatz , then according to Löb's theorem . ${\displaystyle \varphi }$ ${\displaystyle T\vdash \varphi \leftrightarrow Bew_{T}(\#\varphi )}$ ${\displaystyle T\vdash \varphi }$
• P is a truth predicate if for all formulas applies: . It can easily be shown that P is also a provability predicate for T. According to Löb's theorem, then applies to all formulas : and T is inconsistent. So no consistent theory has a truth predicate. ${\displaystyle \varphi }$ ${\displaystyle T\vdash P(\#\varphi )\leftrightarrow \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle T\vdash \varphi }$
• Gödel's second theorem of incompleteness says that a sufficiently strong and consistent formal system cannot prove its own consistency. This can be deduced from Löb's theorem as follows. Suppose it proves its own consistency, ie . This is equivalent to . According to Löb's theorem, is and is inconsistent. ${\displaystyle T}$ ${\displaystyle T\vdash \neg Bew_{T}(\#\bot )}$ ${\displaystyle T\vdash (Bew(\#\bot )\rightarrow \bot )}$ ${\displaystyle T\vdash \bot }$ ${\displaystyle T}$

literature

• George Boolos , John P. Burgess, and Richard Jeffrey: Computability and Logic . 4th edition. Cambridge University Press, 2002, ISBN 0-521-70146-5 .
• Martin Hugo Löb: Solution of a Problem of Leon Henkin . In: Journal of Symbolic Logic . tape 20 , 1955, pp. 115-118 .

Web links

• Löb's theorem at PlanetMath
• The Cartoon Guide to Löb's Theorem, by Eliezer Yudkowsky

Individual evidence

1. ↑ Boolos et al. 2002, pages 236-237
2. ↑ Boolos et al. 2002, page 235
3. ↑ Boolos et al. 2002, page 237