Editing Proof theory (section)

==Provability logic==
{{Main|Provability logic}}

''Provability logic'' is a [[modal logic]], in which the box operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich [[theory (mathematical logic)|formal theory]]. As basic axioms of the provability logic GL ([[Kurt Gödel|Gödel]]-[[Martin Hugo Löb|Löb]]), which captures provable in [[Peano Arithmetic]], one takes modal analogues of the Hilbert-Bernays derivability conditions and [[Löb's theorem]] (if it is provable that the provability of A implies A, then A is provable).

Some of the basic results concerning the incompleteness of Peano Arithmetic and related theories have analogues in provability logic. For example, it is a theorem in GL that if a contradiction is not provable then it is not provable that a contradiction is not provable (Gödel's second incompleteness theorem). There are also modal analogues of the fixed-point theorem. [[Robert Solovay]] proved that the modal logic GL is complete with respect to Peano Arithmetic. That is, the propositional theory of provability in Peano Arithmetic is completely represented by the modal logic GL. This straightforwardly implies that propositional reasoning about provability in Peano Arithmetic is complete and decidable.

Other research in provability logic has focused on first-order provability logic, [[Japaridze's polymodal logic|polymodal provability logic]] (with one modality representing provability in the object theory and another representing provability in the meta-theory), and [[interpretability logic]]s intended to capture the interaction between provability and interpretability. Some very recent research has involved applications of graded provability algebras to the ordinal analysis of arithmetical theories.