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.