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.
The language of ILM extends that of classical propositional logic by adding the unary modal operator
\Box
\triangleright
\Diamondp
\neg\Box\negp
\Boxp
p
p\trianglerightq
PA+q
PA+p
Axiom schemata:
\Box(p → q) → (\Boxp → \Boxq)
\Box(\Boxp → p) → \Boxp
\Box(p → q) → (p\trianglerightq)
(p\trianglerightq)\wedge(q\trianglerightr) → (p\trianglerightr)
(p\trianglerightr)\wedge(q\trianglerightr) → ((p\veeq)\trianglerightr)
(p\trianglerightq) → (\Diamondp → \Diamondq)
\Diamondp\trianglerightp
(p\trianglerightq) → ((p\wedge\Boxr)\triangleright(q\wedge\Boxr))
Rules of inference:
p
p → q
q
p
\Boxp
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
\Diamond
\Diamond(p1,\ldots,pn)
(PA+p1,\ldots,PA+pn)
p,q
\vec{r},\vec{s}
\Diamond
\Diamond(\vec{r},p,\vec{s}) → \Diamond(\vec{r},p\wedge\negq,\vec{s})\vee\Diamond(\vec{r},q,\vec{s})
\Diamond(p) → \Diamond(p\wedge\neg\Diamond(p))
\Diamond(\vec{r},p,\vec{s}) → \Diamond(\vec{r},\vec{s})
\Diamond(\vec{r},p,\vec{s}) → \Diamond(\vec{r},p,p,\vec{s})
\Diamond(p,\Diamond(\vec{r})) → \Diamond(p\wedge\Diamond(\vec{r}))
\Diamond(\vec{r},\Diamond(\vec{s})) → \Diamond(\vec{r},\vec{s})
Rules of inference:
p
p → q
q
\negp
\neg\Diamond(p)
The completeness of TOL with respect to its arithmetical interpretation was proven by Giorgi Japaridze.