Supriya Ghosh (Editor)

Interpretability logic

Updated on
Edit
Like
Comment
Share on FacebookTweet on TwitterShare on LinkedInShare on Reddit

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 ◻ and the binary modal operator ▹ (as always, ◊ p is defined as ¬ ◻ ¬ p ). The arithmetical interpretation of ◻ p is “ p is provable in Peano Arithmetic PA”, and p ▹ q is understood as “ P A + q is interpretable in P A + p ”.

    • Axiom schemata:

    1. All classical tautologies

    2. ◻ ( p → q ) → ( ◻ p → ◻ q )

    3. ◻ ( ◻ p → p ) → ◻ p

    4. ◻ ( p → q ) → ( p ▹ q )

    5. ( p ▹ q ) ∧ ( q ▹ r ) → ( p ▹ r )

    6. ( p ▹ r ) ∧ ( q ▹ r ) → ( ( p ∨ q ) ▹ r )

    7. ( p ▹ q ) → ( ◊ p ▹ ◊ q )

    8. ◊ p ▹ p

    9. ( p ▹ q ) → ( ( p ∧ ◻ r ) ▹ ( q ∧ ◻ r ) )

    Rules inference:

    1. “From p and p → q conclude q ”

    2. “From p conclude ◻ 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 ◊ which is allowed to take any nonempty sequence of arguments. The arithmetical interpretation of ◊ ( p 1 , … , p n ) is “ ( P A + p 1 , … , P A + p n ) is a tolerant sequence of theories”.

    • Axioms (with p , q standing for any formulas, r → , s → for any sequences of formulas, and ◊ ( ) identified with ⊤):

    1. All classical tautologies

    2. ◊ ( r → , p , s → ) → ◊ ( r → , p ∧ ¬ q , s → ) ∨ ◊ ( r → , q , s → )

    3. ◊ ( p ) → ◊ ( p ∧ ¬ ◊ ( p ) )

    4. ◊ ( r → , p , s → ) → ◊ ( r → , s → )

    5. ◊ ( r → , p , s → ) → ◊ ( r → , p , p , s → )

    6. ◊ ( p , ◊ ( r → ) ) → ◊ ( p ∧ ◊ ( r → ) )

    7. ◊ ( r → , ◊ ( s → ) ) → ◊ ( r → , s → )

    Rules inference:

    1. “From p and p → q conclude q ”

    2. “From ¬ p conclude ¬ ◊ ( p ) ”.

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

    References

    Interpretability logic Wikipedia
    (Text) CC BY-SA