Editing Interpretability logic (section)

=== Logic TOL ===

The language of TOL extends that of classical propositional logic by adding the modal operator <math>\Diamond</math> which is allowed to take any nonempty sequence of arguments. The arithmetical interpretation of <math>\Diamond( p_1,\ldots,p_n)</math> is “<math>(PA+p_1,\ldots,PA+p_n)</math> is a [[tolerant sequence]] of theories”. 
 
Axioms (with <math>p,q</math> standing for any formulas,  <math>\vec{r},\vec{s}</math> for any sequences of formulas, and <math>\Diamond()</math> identified with ⊤): 

# All classical tautologies
# <math>\Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r}, p\wedge\neg q,\vec{s})\vee \Diamond (\vec{r}, q,\vec{s}) </math>
# <math>\Diamond (p)\rightarrow \Diamond (p\wedge \neg\Diamond (p)) </math>
# <math>\Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r},\vec{s})</math>
# <math>\Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r},p,p,\vec{s})</math>
# <math>\Diamond (p,\Diamond(\vec{r}))\rightarrow \Diamond (p\wedge\Diamond(\vec{r}))</math>
# <math>\Diamond (\vec{r},\Diamond(\vec{s}))\rightarrow \Diamond (\vec{r},\vec{s})</math>

Rules of inference: 

# “From <math>p</math> and <math>p\rightarrow q</math> conclude <math>q</math>” 
# “From <math>\neg p</math> conclude <math>\neg \Diamond( p)</math>”.

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