X؍(R, ÓT_), Provability and interpretability logics
------------------------------------------------------------
Provability logic GL is one of the normal modal logics, which is obtained from the
smallest normal modal logic K by adding L\"ob's axiom.  The name ``provability logic''
derives from Solovay's theorem.  He proved that GL is complete for the formal provability
interpretation in Peano arithmetic PA.  So, GL has been considered as one of the most
important modal logics.
Interpretability logics were introduced by Albert Visser in 1990 as extensions of
the provability logic GL with a binary modality \rhd.  The arithmetic realization of
A \rhd B in a theory T will be that T plus the realization of B is interpretable in T
plus the realization of A (T+A interprets T+B).  More precisely, there exists a function
f(the relative interpretation) on the formulas of the language of T such that T+B \vdash C
implies T+A \vdash f(C).
Here, we describe some results on these logics in a recent few years.
--------------------------------------------------------------