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.

Examples

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

Axiom schemata:

1. All classical tautologies

2. $\Box(p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q)$

3. $\Box(\Box p \rightarrow p) \rightarrow \Box p$

4. $\Box (p \rightarrow q) \rightarrow (p \triangleright q)$

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

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

7. $(p \triangleright q)\rightarrow (\Diamond p\triangleright\Diamond q)$

8. $\Diamond p \triangleright p$

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

Rules inference:

1. “From $p$ and $p\rightarrow q$ conclude $q$”

2. “From $p$ conclude $\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 $\Diamond$ which is allowed to take any nonempty sequence of arguments. The arithmetical interpretation of $\Diamond( p_1,\ldots,p_n)$ is “$(PA+p_1,\ldots,PA+p_n)$ is a tolerant sequence of theories”.

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

1. All classical tautologies

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

3. $\Diamond (p)\rightarrow \Diamond (p\wedge \neg\Diamond (p))$

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

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

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

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

Rules inference:

1. “From $p$ and $p\rightarrow q$ conclude $q$”

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

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

References

• Giorgi Japaridze and Dick de Jongh, The Logic of Provability. In Handbook of Proof Theory, S.Buss, ed. Elsevier, 1998, pp. 475-546.