词条 | Provability logic |
释义 |
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. ExamplesThere 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-Löb) or L or K4W. 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:
And the rules of inference are:
HistoryThe 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. GeneralizationsInterpretability logics and Japaridze's polymodal logic present natural extensions of provability logic. See also
References
3 : Modal logic|Proof theory|Provability logic |
随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识,基本涵盖了大多数领域的百科知识,是一部内容自由、开放的电子版国际百科全书。