Interpretability logic

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 usual, ${\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)\rightarrow (\Diamond p\rightarrow \Diamond q)}$
6. ${\displaystyle (p\triangleright q)\wedge (q\triangleright r)\rightarrow (p\triangleright r)}$
7. ${\displaystyle (p\triangleright r)\wedge (q\triangleright r)\rightarrow ((p\vee q)\triangleright r)}$
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.

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.

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