Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Provability logic
Summary
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 formal theory, such as Peano arithmetic.
There are a number of provability logics, some of which are covered in the literature mentioned in . 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).
Namely, the axioms of GL are all tautologies of classical propositional logic plus all formulas of one of the following forms:
Distribution axiom: □(p → q) → (□p → □q);
Löb's axiom: □(□p → p) → □p.
And the rules of inference are:
Modus ponens: From p → q and p conclude q;
Necessitation: From p conclude □p.
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.
Interpretability logics and Japaridze's polymodal logic present natural extensions of provability logic.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.