Editing Löb's theorem

{{Short description|Provability logic}}
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. If Prov(''P'') is the assertion that the formula ''P'' is provable in PA, we may express this more formally as

:If 
:<math>\mathit{PA} \vdash {\mathrm{Prov}(P) \rightarrow P}</math>
:then 
:<math>\mathit{PA} \vdash P</math>.

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 <math>1+1=3</math> is provable in PA, then <math>1+1=3</math>" is not provable in PA.<ref>Unless PA is inconsistent (in which case every statement is provable, including <math>1+1=3</math>).</ref>

Löb's theorem is named for [[Martin Löb|Martin Hugo Löb]], who formulated it in 1955.{{sfn|Löb|1955}} It is related to [[Curry's paradox]].<ref>{{cite web |last1=Neel |first1=Krishnaswami |title=Löb's theorem is (almost) the Y combinator |url=https://semantic-domain.blogspot.com/2016/05/lobs-theorem-is-almost-y-combinator.html |website=Semantic Domain |date=9 May 2016 |access-date=9 April 2024 |ref=neel}}</ref>

==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 <math>\phi</math> in the given system in the language of [[modal logic]], by means of the modality {{tooltip|<math>\Box \phi</math>|The box is intended to be a box; it is not your browser failing to display another glyph.}}. That is, when <math>\phi</math> is a logical formula, another formula can be formed by placing a box in front of <math>\phi</math>, and is intended to mean that <math>\phi</math> is provable.

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

:<math>\Box(\Box P\rightarrow P)\rightarrow \Box P,</math>

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

:If
:<math>\vdash \Box P \rightarrow P</math>
:then
:<math>\vdash P</math>.

The provability logic '''GL''' that results from taking the [[modal logic]] '''K4''' (or '''K''', since the axiom schema 4, <math>\Box A\rightarrow\Box\Box A</math>, 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 [[normal 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 (mathematics)|grammar]] for formulas:
# If <math>X</math> is a [[propositional variable]], then <math>X</math> is a formula.
# If <math>K</math> is a propositional constant, then <math>K</math> is a formula.
# If <math>A</math> is a formula, then <math>\Box A</math> is a formula.
# If <math>A</math> and <math>B</math> are formulas, then so are <math>\neg A</math>, <math>A \rightarrow B</math>, <math>A \wedge B</math>, <math>A \vee B</math>, and <math>A \leftrightarrow B</math>

A modal sentence is a formula in this syntax that contains no propositional variables. The notation <math>\vdash A</math> is used to mean that <math>A</math> is a theorem.

===Modal fixed points===
If <math>F(X)</math> is a modal formula with only one propositional variable <math>X</math>, then a modal fixed point of <math>F(X)</math> is a sentence <math>\Psi</math> such that
:<math>\vdash \Psi \leftrightarrow F(\Box \Psi)</math>

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 <math>\Box</math> 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 <math>\Box</math>, known as [[Hilbert–Bernays provability conditions]]:

# '''(necessitation)''' From <math>\vdash A</math> conclude <math>\vdash \Box A</math>: Informally, this says that if A is a theorem, then it is provable.
# '''(internal necessitation)''' <math>\vdash \Box A \rightarrow \Box \Box A</math>: If A is provable, then it is provable that it is provable.
# '''(box distributivity)''' <math>\vdash \Box (A \rightarrow B) \rightarrow (\Box A \rightarrow \Box B)</math>:  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===

Much of the proof does not make use of the assumption <math>\Box P \to P</math>, so for ease of understanding, the proof below is subdivided to leave the parts depending on <math>\Box P \to P</math> until the end.  

Let <math>P</math> be any modal sentence.

# Apply the existence of modal fixed points to the formula <math>F(X) = X \rightarrow P</math>. It then follows that there exists a sentence <math>\Psi</math> such that <br><math>\vdash \Psi \leftrightarrow (\Box \Psi \rightarrow P)</math>.
# <math>\vdash \Psi \rightarrow (\Box \Psi \rightarrow P)</math>, from 1.
# <math>\vdash \Box(\Psi \rightarrow (\Box \Psi \rightarrow P))</math>, from 2 by the necessitation rule.
# <math>\vdash \Box\Psi \rightarrow \Box(\Box \Psi \rightarrow P)</math>, from 3 and the box distributivity rule.
# <math>\vdash \Box(\Box \Psi \rightarrow P) \rightarrow (\Box\Box\Psi \rightarrow \Box P)</math>, box distributivity rule " <math>\vdash \Box(A \rightarrow B) \rightarrow (\Box A \rightarrow \Box B)</math> " with <math> A = \Box \Psi </math> and <math> B= P</math>.
# <math>\vdash \Box \Psi \rightarrow (\Box\Box\Psi \rightarrow \Box P)</math>, from 4 and 5.
# <math>\vdash \Box \Psi \rightarrow \Box \Box \Psi</math>, internal necessitation rule.
# <math>\vdash \Box \Psi \rightarrow \Box P</math>, from 6 and 7.<br><br>Now comes the part of the proof where the hypothesis is used.<br><br>
# Assume that <math>\vdash \Box P \rightarrow P</math>.  Roughly speaking, it is a theorem that if <math>P</math> is provable, then it is, in fact true.  This is a claim of ''soundness''.
# <math>\vdash \Box \Psi \rightarrow P</math>, from 8 and 9.
# <math>\vdash (\Box \Psi \rightarrow P) \rightarrow \Psi</math>, from 1.
# <math>\vdash \Psi</math>, from 10 and 11.
# <math>\vdash \Box \Psi</math>, from 12 by the necessitation rule.
# <math>\vdash P</math>, from 13 and 10.
More informally, we can sketch out the proof as follows.

# Since <math>\mathit{PA} \vdash {\mathrm{Prov}_{PA}(P) \rightarrow P}</math> by assumption, we also have <math>\mathit{PA} \vdash {\neg P \rightarrow \neg \mathrm{Prov}_{PA}(P)} </math>, which implies <math>\{ \mathit{PA},  \neg P\} \vdash { \neg \mathrm{Prov}_{PA} (P)}   </math>.
# Now, the hybrid theory <math>\{ \mathit{PA},  \neg P\}  </math> can reason as follows: 
## Suppose <math>\{ \mathit{PA},  \neg P\}  </math> is inconsistent, then PA proves <math>\neg P \to \bot{} </math>, which is the same as <math>P </math>.
## However, <math>\{ \mathit{PA},  \neg P\}  </math> already knows that <math>\neg \mathrm{Prov}_{PA} (P)  </math>, a contradiction.
## Therefore, <math>\{ \mathit{PA},  \neg P\}  </math> is consistent.
# By Godel's second incompleteness theorem, this implies <math>\{ \mathit{PA},  \neg P\}  </math> is inconsistent. 
# Thus, PA proves <math>\neg P \to \bot{} </math>, which is the same as <math>P </math>.

==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 <math>1+1=3</math> is provable in PA, then <math>1+1=3</math>" is not provable in PA, as <math>1+1=3</math> is not provable in PA (as it is false).
* "If <math>1+1=2</math> is provable in PA, then <math>1+1=2</math>" is provable in PA, as is any statement of the form "If X, then <math>1+1=2</math>".
* "If [[Paris–Harrington theorem#The strengthened finite Ramsey theorem|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 ''[[Doxastic logic#Types of reasoners|reflexive]]'' "[[Doxastic logic#Increasing levels of rationality|type 4]]" reasoner must also be "''modest''": such a reasoner can never believe "my belief in P would imply that P is true", without also believing that P is true.{{sfn|Smullyan|1986}}

Gödel's second incompleteness theorem follows from Löb's theorem by substituting the false statement <math>\bot</math> 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) <math>p\leftrightarrow A(p)</math> for any formula ''A''(''p'')'' modalized in p'' can be derived.{{sfn|Lindström|2006}} Thus in [[normal modal logic]], Löb's axiom is equivalent to the conjunction of the axiom schema '''4''', <math>(\Box A\rightarrow \Box\Box A)</math>, and the existence of modal fixed points.

==Notes==
{{Reflist}}

==References==
* {{cite book | last = Boolos | first = George S. | author-link = George Boolos | title = The Logic of Provability | publisher = [[Cambridge University Press]] | year = 1995 | isbn = 978-0-521-48325-4 | url-access = registration | url = https://archive.org/details/logicofprovabili0000bool }}
* {{cite book | last = Hinman | first = P. | title = Fundamentals of Mathematical Logic | publisher = A K Peters | year = 2005 | isbn = 978-1-56881-262-5 }}
* {{cite book | last1 = Japaridze | first1 = Giorgi | last2 = De Jongh | first2 = Dick | year = 1998 | chapter = Chapter VII - The Logic of Provability | title = Handbook of Proof Theory | series = Studies in Logic and the Foundations of Mathematics | editor-last = Buss | editor-first = Samuel R. | editor-link = Samuel Buss | publisher = [[Elsevier]] | volume = 137 | pages = 475–546 | doi = 10.1016/S0049-237X(98)80022-0 | doi-access = free | isbn = 978-0-444-89840-1 }}
* {{cite journal | last = Lindström | first = Per | author-link = Per Lindström | date = June 2006 | volume = 35 | issue = 3 | pages = 225–230 | title = Note on Some Fixed Point Constructions in Provability Logic | doi = 10.1007/s10992-005-9013-8 | journal = [[Journal of Philosophical Logic]] | s2cid = 11038803 }}
* {{cite journal | last = Löb | first = Martin | author-link = Martin Löb | title = Solution of a Problem of Leon Henkin | journal = [[Journal of Symbolic Logic]] | volume = 20 | issue = 2 | year = 1955 | pages = 115–118 | doi = 10.2307/2266895 | jstor = 2266895 | s2cid = 250348262 }}
* {{cite conference | last = Smullyan |first = Raymond M. | author-link = Raymond Smullyan | year = 1986 | title = Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge, Monterey (CA) | publisher = Morgan Kaufmann Publishers Inc. | location = San Francisco (CA) | pages = 341–352 | chapter-url = https://dl.acm.org/doi/pdf/10.5555/1029786.1029818 | chapter = Logicians who reason about themselves | doi = 10.1016/B978-0-934613-04-0.50028-4 | isbn=9780934613040 }}

==External links==
* {{Cite web
|url= https://planetmath.org/lobstheorem
|title= Löb's theorem
|date= 22 March 2013
|at= [[PlanetMath]]
|access-date= 14 December 2023
}}
* {{SEP|logic-provability|Provability Logic|Rineke (L.C.) Verbrugge|2017}}

{{DEFAULTSORT:Lob's theorem}}
[[Category:Mathematical logic]]
[[Category:Theorems in the foundations of mathematics]]
[[Category:Metatheorems]]
[[Category:Provability logic]]
[[Category:Mathematical axioms]]
[[Category:Modal logic]]