Editing Interpretability logic (section)

=== Logic ILM ===

The language of ILM extends that of classical propositional logic by adding the unary modal operator <math>\Box</math> and the binary modal operator <math>\triangleright</math> (as always, <math>\Diamond p</math> is defined as <math>\neg \Box\neg p</math>). The arithmetical interpretation of <math>\Box p</math> is “<math>p</math> is provable in [[Peano arithmetic]] (PA)”, and <math>p \triangleright q</math> is understood as “<math>PA+q</math> is interpretable in <math>PA+p</math>”. 

Axiom schemata: 

# All classical tautologies
# <math>\Box(p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q)</math>
# <math>\Box(\Box p \rightarrow p) \rightarrow \Box p</math>
# <math> \Box (p \rightarrow q) \rightarrow (p \triangleright q)</math>
# <math> (p \triangleright q)\rightarrow (\Diamond p \rightarrow \Diamond q) </math>
# <math> (p \triangleright q)\wedge  (q \triangleright r)\rightarrow (p\triangleright r)</math>
# <math> (p \triangleright r)\wedge  (q \triangleright r)\rightarrow ((p\vee q)\triangleright r)</math>
# <math> \Diamond p \triangleright p </math>
# <math> (p \triangleright q)\rightarrow((p\wedge\Box r)\triangleright (q\wedge\Box r)) </math>

Rules of inference: 

# “From <math>p</math> and <math>p\rightarrow q</math> conclude <math>q</math>” 
# “From <math>p</math> conclude <math>\Box p</math>”.

The completeness of ILM with respect to its arithmetical interpretation was independently proven by Alessandro Berarducci and Vladimir Shavrukov.