Interpretability logic explained

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.

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,

\Diamondp

is defined as

\neg\Box\negp

). The arithmetical interpretation of

\Boxp

is “

p

is provable in Peano arithmetic (PA)”, and

p\trianglerightq

is understood as “

PA+q

is interpretable in

PA+p

”.

Axiom schemata:

  1. All classical tautologies

\Box(pq)(\Boxp\Boxq)

\Box(\Boxpp)\Boxp

\Box(pq)(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:

  1. “From

p

and

pq

conclude

q

  1. “From

p

conclude

\Boxp

”.

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(p1,\ldots,pn)

is “

(PA+p1,\ldots,PA+pn)

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

\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:

  1. “From

p

and

pq

conclude

q

  1. “From

\negp

conclude

\neg\Diamond(p)

”.

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

References