Editing Provability logic

'''Provability logic''' is a [[modal logic]], in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich [[theory (mathematical logic)|formal theory]], such as [[Peano arithmetic]].

==Examples==
There are a number of provability logics, some of which are covered in the literature mentioned in {{sectionlink||References}}. The basic system is generally referred to as '''GL''' (for [[Kurt Gödel|Gödel]]–[[Martin Hugo Löb|Löb]]) or '''L''' or '''K4W''' ('''W''' stands for [[Well-founded relation|well-foundedness]]). It can be obtained by adding the modal version of [[Löb's theorem]] to the [[normal modal logic|logic '''K''']] (or '''K4''').

Namely, the '''axioms''' of '''GL''' are all [[tautology (logic)|tautologies]] of classical [[propositional logic]] plus all formulas of one of the following forms: 
* '''Distribution axiom''': {{math|□(''p'' → ''q'') → (□''p'' → □''q'');}}
* '''Löb's axiom''': {{math|□(□''p'' → ''p'') → □''p''.}}
And the '''rules of inference''' are:
* '''''Modus ponens''''': From ''p'' → ''q'' and ''p'' conclude ''q'';
* '''Necessitation''': From <math>\vdash</math> ''p'' conclude <math>\vdash</math> {{math|□''p''}}.

==History==
The '''GL''' model was pioneered by [[Robert M. Solovay]] in 1976. Since then, until his death in 1996, the prime inspirer of the field was [[George Boolos]]. Significant contributions to the field have been made by [[Sergei N. Artemov]], Lev Beklemishev, [[Giorgi Japaridze]], [[Dick de Jongh]], Franco Montagna, Giovanni Sambin, Vladimir Shavrukov, Albert Visser and others.

==Generalizations==
[[Interpretability logic]]s and [[Japaridze's polymodal logic]] present natural extensions of provability logic.

==See also==
*[[Hilbert–Bernays provability conditions]]
*[[Interpretability logic]]
*[[Kripke semantics]]
*[[Japaridze's polymodal logic]]
*[[Löb's theorem]]
*[[Doxastic logic]]

==References==

*[[George Boolos]], '''[https://books.google.com/books?id=WekaT3OLoUcC&dq=%22The+Logic+of+Provability%22&pg=PR9 The Logic of Provability]'''. Cambridge University Press, 1993.
*[https://web.archive.org/web/20190419120954/http://www.csc.villanova.edu/~japaridz/ Giorgi Japaridze] and Dick de Jongh, [http://www.csc.villanova.edu/~japaridz/Text/prov.pdf ''The logic of provability'']. In: '''Handbook of Proof Theory''', S. Buss, ed. Elsevier, 1998, pp.&nbsp;475–546.
*[[Sergei N. Artemov]] and [https://web.archive.org/web/20050403201724/http://www.phil.uu.nl/~lev/ Lev Beklemishev], [https://web.archive.org/web/20050425014013/http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint234.pdf ''Provability logic'']. In: '''[https://dx.doi.org/10.1007/1-4020-3521-7_3 Handbook of Philosophical Logic]''', D. Gabbay and F. Guenthner, eds.,  vol. 13, 2nd ed., pp.&nbsp;189–360. Springer, 2005.
*[[Per Lindström]], ''Provability logic—a short introduction''. Theoria 62 (1996), pp.&nbsp;19–61.
*Craig Smoryński, '''Self-reference and modal logic'''. Springer, Berlin, 1985.
*[[Robert M. Solovay]], ``Provability Interpretations of Modal Logic``, [[Israel Journal of Mathematics]], Vol. 25 (1976): 287–304.
*[[Rineke Verbrugge]], [http://plato.stanford.edu/entries/logic-provability/ Provability logic], from the [[Stanford Encyclopedia of Philosophy]].

==External links==
* {{SEP|logic-provability|Provability logic|Rineke Verbrugge}}

[[Category:Provability logic| ]]
[[Category:Modal logic]]
[[Category:Proof theory]]

{{logic-stub}}