Provability Logic Even though "provability logic" did not come into its own until the early seventies, it has its roots in two older fields: metamathematics and modal logic. In metamathematics, we study what theories can say about...

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...