Provability logic is a modal logic

Modal logic

Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...

, 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 formal theory

Formal theory

Formal theory can refer to:* Another name for a theory which is expressed in formal language.* An axiomatic system, something representable by symbols and its operators...

, such as Peano arithmetic.

There are a number of provability logics, some of which are covered in the literature mentioned in the References section. The basic system is generally referred to as GL (for Gödel

Kurt Gödel

Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...

-Löb) or L or K4W. It can be obtained by adding the modal version of Löb's theorem

Löb's theorem

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", then P is provable...

 to the logic K (or K4). It was pioneered by Robert M. Solovay

Robert M. Solovay

Robert Martin Solovay is an American mathematician specializing in set theory.Solovay earned his Ph.D. from the University of Chicago in 1964 under the direction of Saunders Mac Lane, with a dissertation on A Functorial Form of the Differentiable Riemann–Roch theorem...

 in 1976. Since then until his passing in 1996 the prime inspirer of the field was George Boolos

George Boolos

George Stephen Boolos was a philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology.- Life :...

. Significant contributions to the field have been made by Sergei Artemov, Lev Beklemishev, Giorgi Japaridze

Giorgi Japaridze

Giorgi Japaridze is a logician, at Villanova University in Villanova, Pennsylvania. In the past his contributions were primarily into the areas of provability logic and interpretability logic...

, Dick de Jongh

Dick de Jongh

Dick H. J. de Jongh is a Dutch logician and mathematician and a retired professor at the University of Amsterdam.He received his PhD degree in 1968 from the University of Wisconsin–Madison under supervision of Stephen Kleene with a dissertation entitled Investigations on the Intuitionistic...

, Franco Montagna, Vladimir Shavrukov, Albert Visser and others. Interpretability logic

Interpretability logic

Interpretability logics comprise a family of modal logics that extend provability logic to describe interpretability and/or various related metamathematical properties and relations such as weak interpretability, Π1-conservativity, cointerpretability, tolerance, cotolerance and arithmetic...

s present natural extensions of provability logic.