Löb's theorem

In mathematical logic, Löb's theorem states that in Peano arithmetic (PA) (or any formal system including PA), for any formula P, if it is provable in PA that "if P is provable in PA then P is true", then P is provable in PA. More formally, if Prov(P) means that the formula P is provable, then

\mathrm {if} \ PA\vdash ({\rm {Prov}}(P)\rightarrow P)\mathrm {,then} \ PA\vdash P,

or

{\dfrac {PA\vdash {\rm {Prov}}(P)\rightarrow P}{PA\vdash P}}.

An immediate corollary (the contrapositive) of Löb's theorem is that, if P is not provable in PA, then "if P is provable in PA, then P is true" is not provable in PA. For example, "If $1+1=3$ is provable in PA, then $1+1=3$ " is not provable in PA.[note 1]

Löb's theorem is named for Martin Hugo Löb, who formulated it in 1955.

Löb's theorem in provability logic

Provability logic abstracts away from the details of encodings used in Gödel's incompleteness theorems by expressing the provability of $\phi$ in the given system in the language of modal logic, by means of the modality $\Box \phi$ .

Then we can formalize Löb's theorem by the axiom

\Box (\Box P\rightarrow P)\rightarrow \Box P,

known as axiom GL, for Gödel–Löb. This is sometimes formalized by means of an inference rule that infers

P

from

\Box P\rightarrow P.

The provability logic GL that results from taking the modal logic K4 (or K, since the axiom schema 4, $\Box A\rightarrow \Box \Box A$ , then becomes redundant) and adding the above axiom GL is the most intensely investigated system in provability logic.

Modal proof of Löb's theorem

Löb's theorem can be proved within modal logic using only some basic rules about the provability operator (the K4 system) plus the existence of modal fixed points.

Modal formulas

We will assume the following grammar for formulas:

If $X$ is a propositional variable, then $X$ is a formula.
If $K$ is a propositional constant, then $K$ is a formula.
If $A$ is a formula, then $\Box A$ is a formula.
If $A$ and $B$ are formulas, then so are $\neg A$ , $A\rightarrow B$ , $A\wedge B$ , $A\vee B$ , and $A\leftrightarrow B$

A modal sentence is a modal formula that contains no propositional variables. We use $\vdash A$ to mean $A$ is a theorem.

Modal fixed points

If $F(X)$ is a modal formula with only one propositional variable $X$ , then a modal fixed point of $F(X)$ is a sentence $\Psi$ such that

\vdash \Psi \leftrightarrow F(\Box \Psi )

We will assume the existence of such fixed points for every modal formula with one free variable. This is of course not an obvious thing to assume, but if we interpret $\Box$ as provability in Peano Arithmetic, then the existence of modal fixed points follows from the diagonal lemma.

Modal rules of inference

In addition to the existence of modal fixed points, we assume the following rules of inference for the provability operator $\Box$ , known as Hilbert–Bernays provability conditions:

(necessitation) From $\vdash A$ conclude $\vdash \Box A$ : Informally, this says that if A is a theorem, then it is provable.
(internal necessitation) $\vdash \Box A\rightarrow \Box \Box A$ : If A is provable, then it is provable that it is provable.
(box distributivity) $\vdash \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)$ : This rule allows you to do modus ponens inside the provability operator. If it is provable that A implies B, and A is provable, then B is provable.

Proof of Löb's theorem

Assume that there is a modal sentence $P$ such that $\vdash \Box P\rightarrow P$ .
Roughly speaking, it is a theorem that if $P$ is provable, then it is, in fact true.
This is a claim of soundness.
From the existence of modal fixed points for every formula (in particular, the formula $X\rightarrow P$ ) it follows there exists a sentence $\Psi$ such that $\vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P)$ .
From 2, it follows that $\vdash \Psi \rightarrow (\Box \Psi \rightarrow P)$ .
From the necessitation rule, it follows that $\vdash \Box (\Psi \rightarrow (\Box \Psi \rightarrow P))$ .
From 4 and the box distributivity rule, it follows that $\vdash \Box \Psi \rightarrow \Box (\Box \Psi \rightarrow P)$ .
Applying the box distributivity rule with $A=\Box \Psi$ and $B=P$ gives us $\vdash \Box (\Box \Psi \rightarrow P)\rightarrow (\Box \Box \Psi \rightarrow \Box P)$ .
From 5 and 6, it follows that $\vdash \Box \Psi \rightarrow (\Box \Box \Psi \rightarrow \Box P)$ .
From the internal necessitation rule, it follows that $\vdash \Box \Psi \rightarrow \Box \Box \Psi$ .
From 7 and 8, it follows that $\vdash \Box \Psi \rightarrow \Box P$ .
From 1 and 9, it follows that $\vdash \Box \Psi \rightarrow P$ .
From 2, it follows that $\vdash (\Box \Psi \rightarrow P)\rightarrow \Psi$ .
From 10 and 11, it follows that $\vdash \Psi$
From 12 and the necessitation rule, it follows that $\vdash \Box \Psi$ .
From 13 and 10, it follows that $\vdash P$ .

Examples

An immediate corollary of Löb's theorem is that, if P is not provable in PA, then "if P is provable in PA, then P is true" is not provable in PA. Given we know PA is consistent (but PA does not know PA is consistent), here are some simple examples:

"If $1+1=3$ is provable in PA, then $1+1=3$ " is not provable in PA, as $1+1=3$ is not provable in PA (as it is false).
"If $1+1=2$ is provable in PA, then $1+1=2$ " is provable in PA, as is any statement of the form "If X, then $1+1=2$ ".
"If the strengthened finite Ramsey theorem is provable in PA, then the strengthened finite Ramsey theorem is true" is not provable in PA, as "The strengthened finite Ramsey theorem is true" is not provable in PA (despite being true).

In Doxastic logic, Löb's theorem shows that any system classified as a reflexive "type 4" reasoner must also be "modest": such a reasoner can never believe "my belief in P would imply that P is true", without first believing that P is true.[1]

Gödel's second incompleteness theorem follows from Löb's theorem by substituting the false statement $\bot$ for P.

Converse: Löb's theorem implies the existence of modal fixed points

Not only does the existence of modal fixed points imply Löb's theorem, but the converse is valid, too. When Löb's theorem is given as an axiom (schema), the existence of a fixed point (up to provable equivalence) $p\leftrightarrow A(p)$ for any formula A(p) modalized in p can be derived.[2] Thus in normal modal logic, Löb's axiom is equivalent to the conjunction of the axiom schema 4, $(\Box A\rightarrow \Box \Box A)$ , and the existence of modal fixed points.

Notes

Unless PA is inconsistent (in which case every statement is provable, including $1+1=3$ ).

Citations

Smullyan, Raymond M., (1986) Logicians who reason about themselves, Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge, Monterey (CA), Morgan Kaufmann Publishers Inc., San Francisco (CA), pp. 341-352
Per Lindström (June 2006). "Note on Some Fixed Point Constructions in Provability Logic". Journal of Philosophical Logic. 35 (3): 225–230. doi:10.1007/s10992-005-9013-8.

References

Boolos, George S. (1995). The Logic of Provability. Cambridge University Press. ISBN 978-0-521-48325-4.
Löb, Martin (1955), "Solution of a Problem of Leon Henkin", Journal of Symbolic Logic, 20 (2): 115–118, JSTOR 2266895
Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 978-1-56881-262-5.
Verbrugge, Rineke (L.C.) (1 January 2016). "Provability Logic". The Stanford Encyclopedia of Philosophy. Retrieved 6 April 2016.

External links

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

[1] Unless PA is inconsistent (in which case every statement is provable, including $1+1=3$ ).

[2] Smullyan, Raymond M., (1986) Logicians who reason about themselves, Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge, Monterey (CA), Morgan Kaufmann Publishers Inc., San Francisco (CA), pp. 341-352

[3] Per Lindström (June 2006). "Note on Some Fixed Point Constructions in Provability Logic". Journal of Philosophical Logic. 35 (3): 225–230. doi:10.1007/s10992-005-9013-8.