Rosalie Iemhoff (Utrecht University) – The Löb Formula in Logic and Arithmetic

One of the most famous formulas in modal logic is the Löb formula, which expresses a (true) extension of Gödel's second incompleteness theorem. Besides for its arithmetical interpretation, the formula is well-known for its model theory and proof theory, which have salient properties that set them apart from those of other logics.

The provability logic of an arithmetical theory, such as Peano Arithmetic, consists of the general modal principles that under arithmetical interpretations are provable in the theory. For many standard theories, the Löb formula belongs to their provability logic. Solovay in 1976 showed that the elegant modal logic that was conjectured to be the provability logic of Peano Arithmetic was indeed so, thereby solving a problem that had been open for many years.

As it turns out, provability logic is very stable, meaning that many classical theories of sufficient strength have the same provability logic as Peano Arithmetic. This is no longer the case once constructive theories are considered, theories such as Heyting Arithmetic, which is the constructive analogue of Peano Arithmetic: the provability logic of Heyting Arithmetic is not contained in the provability logic of Peano Arithmetic, but the converse is not true either.

In this talk I will explain what provability logic is and discuss several results in the area, in particular results about constructive theories.