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.
Logic ILM.
The language of ILM extends that of classical propositional logic by adding the unary modal operator formula_1 and the binary modal operator formula_2 (as always, formula_3 is defined as formula_4). The arithmetical interpretation of formula_5 is “formula_6 is provable in Peano arithmetic (PA)”, and formula_7 is understood as “formula_8 is interpretable in formula_9”. 
Axiom schemata: 
1. All classical tautologies
2. formula_10
3. formula_11
4. formula_12
5. formula_13
6. formula_14
7. formula_15
8. formula_16
9. formula_17
Rules of inference: 
1. “From formula_6 and formula_19 conclude formula_20” 
2. “From formula_6 conclude formula_5”.
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 formula_23 which is allowed to take any nonempty sequence of arguments. The arithmetical interpretation of formula_24 is “formula_25 is a tolerant sequence of theories”. 
Axioms (with formula_26 standing for any formulas, formula_27 for any sequences of formulas, and formula_28 identified with ⊤): 
1. All classical tautologies
2. formula_29
3. formula_30
4. formula_31
5. formula_32
6. formula_33
7. formula_34
Rules of inference: 
1. “From formula_6 and formula_19 conclude formula_20” 
2. “From formula_38 conclude formula_39”.
The completeness of TOL with respect to its arithmetical interpretation was proven by Giorgi Japaridze. 