Provability logic

Remarks

Solovay's theorem (1976) says: a modal formula $\varphi$ is in $\mathrm{GL}$ if and only if Peano arithmetic proves $\varphi^*$ for every arithmetical realization $*$.

Example: $\square p \to \square\square p$ is in $\mathrm{GL}$. Its realizations are instances of the fact that Peano arithmetic proves "if $\sigma$ is provable, then it is provable that $\sigma$ is provable".

Non-example: $\square p \to p$ is not in $\mathrm{GL}$. Under a realization with $p^* = (0 = 1)$, it becomes the consistency statement of Peano arithmetic, which Peano arithmetic does not prove by Gödel's second incompleteness theorem.

On Kripke frames, $\mathrm{GL}$ is the logic of the finite transitive irreflexive frames. The name "provability logic" also covers the study of related systems for other theories and other provability notions.