Löb's theorem

From Wikipedia, the free encyclopedia
Jump to: navigation, search

In mathematical logic, Löb's theorem states that in a theory with Peano arithmetic, for any formula P, if it is provable that "if P is provable then P is true", then P is provable. I.e.

\mathrm{if}\ PA \vdash (Bew(\# P) \rightarrow P)\mathrm{, then}\ PA \vdash P

where Bew(#P) means that the formula P with Gödel number #P is provable.

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

Löb's theorem in provability logic[edit]

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 formalised 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 and adding the above axiom GL is the most intensely investigated system in provability logic.

Modal Proof of Löb's theorem[edit]

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

Modal Formulas[edit]

We will assume the following grammar for formulas:

  1. If X is a propositional variable, then X is a formula.
  2. If K is a propositional constant, then K is a formula.
  3. If A is a formula, then \Box A is a formula.
  4. 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[edit]

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 is in fact true.

Modal Rules of Inference[edit]

In addition to the existence of modal fixed points, we assume the following rules of inference for the provability operator \Box:

  1. From \vdash A conclude \vdash \Box A: Informally, this says that if A is a theorem, then it is provable.
  2. \vdash \Box A \rightarrow \Box \Box A: If A is provable, then it is provable that it is provable.
  3. \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[edit]

  1. 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.
  2. Let \Psi be a sentence such that \vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P).
    The existence of such a sentence follows the existence of a fixed point of the formula F(X) \leftrightarrow (X \rightarrow P).
  3. From 2, it follows that \vdash \Psi \rightarrow (\Box \Psi \rightarrow P).
  4. From rule of inference 1, it follows that \vdash \Box(\Psi \rightarrow (\Box \Psi \rightarrow P)).
  5. From 4 and rule of inference 3, it follows that \vdash \Box\Psi \rightarrow \Box(\Box \Psi \rightarrow P).
  6. From rule of inference 3, it follows that \vdash \Box(\Box \Psi \rightarrow P) \rightarrow (\Box\Box\Psi \rightarrow \Box P).
  7. From 5 and 6, it follows that \vdash \Box \Psi \rightarrow (\Box\Box\Psi \rightarrow \Box P).
  8. From rule of inference 2, it follows that \vdash \Box \Psi \rightarrow \Box \Box \Psi.
  9. From 7 and 8, it follows that \vdash \Box \Psi \rightarrow \Box P.
  10. From 1 and 9, it follows that \vdash \Box \Psi \rightarrow P.
  11. From 2, it follows that \vdash   (\Box \Psi \rightarrow P) \rightarrow \Psi.
  12. From 10 and 11, it follows that \vdash \Psi
  13. From 12 and rule of inference 1, it follows that \vdash \Box \Psi.
  14. From 13 and 10, it follows that \vdash P.

References[edit]

  • Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0. 
  • Boolos, George S. (1995). The Logic of Provability. Cambridge University Press. ISBN 0-521-48325-5. 

External links[edit]

University of Colorado Boulder, Boulder,CO April 13-14, 2013 (Saturday-Sunday) Meeting #1089

  • [2]
  • [3] Fall Southeastern Sectional Meeting University of Louisville, Louisville, KY October 5-6, 2013 (Saturday - Sunday) Meeting #1092