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 ${\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 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 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.

References

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