Provability logic
|
|
Provability logic is a modal logic where the box (or "necessity") operator is interpreted as 'it is provable that', capturing the notion of a proof predicate of a reasonably rich formal theory such as Peano arithmetic. The system is generally referred to as GL (for Gödel-Löb) or L or K4W. It is obtained by adding the modal version of Löb's theorem to the logic K4. It was pioneered by Robert Solovay in 1976. Since then until his passing in 1996 the prime inspirer of the field was George Boolos. Significant contributions to the field have been made by Sergei Artemov, Lev Beklemishev, Giorgi Japaridze, Dick de Jongh, Franco Montagna, Vladimir Shavrukov, Albert Visser and others. Interpretability logics present natural extensions of provability logic.
References
- Provability logic (http://plato.stanford.edu/entries/logic-provability/), from the Stanford Encyclopedia of Philosophy.
- George Boolos, The Logic of Provability. Cambridge University Press, 1993.
- Giorgi Japaridze (http://www.csc.villanova.edu/~japaridz/) and Dick de Jongh, The logic of Provability. In: Handbook of Proof Theory, S.Buss, ed. Elsevier, 1998, pp. 475-546.
- Sergei Artemov and Lev Beklemishev (http://www.phil.uu.nl/~lev/), Provability logic (http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint234.pdf), In: Handbook of Philosophical Logic, D. Gabbay and F. Guenthner, eds., vol. 13, 2nd ed., pp. 229-403. Kluwer, Dordrecht, 2004.