# Philosophy: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, Π1-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.

## Examples

### Logic ILM

The language of ILM extends that of classical propositional logic by adding the unary modal operator $\displaystyle{ \Box }$ and the binary modal operator $\displaystyle{ \triangleright }$ (as always, $\displaystyle{ \Diamond p }$ is defined as $\displaystyle{ \neg \Box\neg p }$). The arithmetical interpretation of $\displaystyle{ \Box p }$ is “$\displaystyle{ p }$ is provable in Peano arithmetic (PA)”, and $\displaystyle{ p \triangleright q }$ is understood as “$\displaystyle{ PA+q }$ is interpretable in $\displaystyle{ PA+p }$”.

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 }$

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

5. $\displaystyle{ (p \triangleright q)\wedge (q \triangleright r)\rightarrow (p\triangleright r) }$

6. $\displaystyle{ (p \triangleright r)\wedge (q \triangleright r)\rightarrow ((p\vee q)\triangleright r) }$

7. $\displaystyle{ (p \triangleright q)\rightarrow (\Diamond p \rightarrow \Diamond q) }$

8. $\displaystyle{ \Diamond p \triangleright p }$

9. $\displaystyle{ (p \triangleright q)\rightarrow((p\wedge\Box r)\triangleright (q\wedge\Box r)) }$

Rules of inference:

1. “From $\displaystyle{ p }$ and $\displaystyle{ p\rightarrow q }$ conclude $\displaystyle{ q }$

2. “From $\displaystyle{ p }$ conclude $\displaystyle{ \Box p }$”.

The completeness of ILM with respect to its arithmetical interpretation was independently proven by Alessandro Berarducci and Vladimir Shavrukov.

### Logic TOL

The language of TOL extends that of classical propositional logic by adding the modal operator $\displaystyle{ \Diamond }$ which is allowed to take any nonempty sequence of arguments. The arithmetical interpretation of $\displaystyle{ \Diamond( p_1,\ldots,p_n) }$ is “$\displaystyle{ (PA+p_1,\ldots,PA+p_n) }$ is a tolerant sequence of theories”.

Axioms (with $\displaystyle{ p,q }$ standing for any formulas, $\displaystyle{ \vec{r},\vec{s} }$ for any sequences of formulas, and $\displaystyle{ \Diamond() }$ identified with ⊤):

1. All classical tautologies

2. $\displaystyle{ \Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r}, p\wedge\neg q,\vec{s})\vee \Diamond (\vec{r}, q,\vec{s}) }$

3. $\displaystyle{ \Diamond (p)\rightarrow \Diamond (p\wedge \neg\Diamond (p)) }$

4. $\displaystyle{ \Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r},\vec{s}) }$

5. $\displaystyle{ \Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r},p,p,\vec{s}) }$

6. $\displaystyle{ \Diamond (p,\Diamond(\vec{r}))\rightarrow \Diamond (p\wedge\Diamond(\vec{r})) }$

7. $\displaystyle{ \Diamond (\vec{r},\Diamond(\vec{s}))\rightarrow \Diamond (\vec{r},\vec{s}) }$

Rules of inference:

1. “From $\displaystyle{ p }$ and $\displaystyle{ p\rightarrow q }$ conclude $\displaystyle{ q }$

2. “From $\displaystyle{ \neg p }$ conclude $\displaystyle{ \neg \Diamond( p) }$”.

The completeness of TOL with respect to its arithmetical interpretation was proven by Giorgi Japaridze.