Provability logic is amodal 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 richformal theory, such asPeano arithmetic.

There are a number of provability logics, some of which are covered in the literature mentioned in§ References. The basic system is generally referred to asGL (forGödel–Löb) orL orK4W (W stands forwell-foundedness). It can be obtained by adding the modal version ofLöb's theorem to thelogicK (orK4).

Namely, theaxioms ofGL are alltautologies of classicalpropositional logic plus all formulas of one of the following forms:

• Distribution axiom:□(p →q) → (□p → □q);
• Löb's axiom:□(□p →p) → □p.

And therules of inference are:

• Modus ponens: Fromp →q andp concludeq;
• Necessitation: From${\displaystyle ⊢}$p conclude${\displaystyle ⊢}$□p.

TheGL model was pioneered byRobert M. Solovay in 1976. Since then, until his death in 1996, the prime inspirer of the field wasGeorge Boolos. Significant contributions to the field have been made bySergei N. Artemov, Lev Beklemishev,Giorgi Japaridze,Dick de Jongh, Franco Montagna, Giovanni Sambin, Vladimir Shavrukov, Albert Visser and others.

Interpretability logics andJaparidze's polymodal logic present natural extensions of provability logic.

• Hilbert–Bernays provability conditions
• Interpretability logic
• Kripke semantics
• Japaridze's polymodal logic
• Löb's theorem
• Doxastic logic

• George Boolos,The Logic of Provability. Cambridge University Press, 1993.
• Giorgi Japaridze and Dick de Jongh,The logic of provability. In:Handbook of Proof Theory, S. Buss, ed. Elsevier, 1998, pp. 475–546.
• Sergei N. Artemov andLev Beklemishev,Provability logic. In:Handbook of Philosophical Logic, D. Gabbay and F. Guenthner, eds., vol. 13, 2nd ed., pp. 189–360. Springer, 2005.
• Per Lindström,Provability logic—a short introduction. Theoria 62 (1996), pp. 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,Provability logic, from theStanford Encyclopedia of Philosophy.

• "Provability logic" entry by Rineke Verbrugge in theStanford Encyclopedia of Philosophy

Thislogic-related article is astub. You can help Wikipedia byexpanding it.

• v
• t
• e

• Provability logic
• Modal logic
• Proof theory
• Logic stubs

• Articles with Stanford Encyclopedia of Philosophy links
• All stub articles