Interpretability logic

Interpretability logics comprise a family of modal logics that extend provability logic to describe interpretability or various related metamathematical properties and relations such as weak interpretability, Π₁-conservativity, cointerpretability, tolerance, cotolerance, and arithmetic complexities.

Main contributors to the field are Alessandro Berarducci, Petr Hájek, Konstantin Ignatiev, Giorgi Japaridze, Franco Montagna, Vladimir Shavrukov, Rineke Verbrugge, Albert Visser, and Domenico Zambella.

Axiom schemata:

1. All classical tautologies

2. ${\displaystyle \Box (p\rightarrow q)\rightarrow (\Box p\rightarrow \Box q)}$

3. ${\displaystyle \Box (\Box p\rightarrow p)\rightarrow \Box p}$

...
Wikipedia