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, Π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

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.


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

This article is issued from Wikipedia - version of the Thursday, November 19, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.