Provability logic

The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano 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 as GL (for Gödel–Löb) or L or K4W (W stands for well-foundedness).

It can be obtained by adding the modal version of Löb's theorem to the logic K (or K4).

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.