Explicit fixed points in interpretability logic

The basic theorems of Provability Logic arethree in number. First is the Arithmetical Completeness Theorem. The second place is shared by the theorems affirming the Uniqueness of Fixed Points and the Explicit Definability of Fixed Points. In this paper we consider the problem of Uniqueness and: Explicit Definability of Fixed Points for Interpretability Logic. It turns out that Uniqueness is an immediate corollary of a theorem of Smoryriski, so. most of the paper, is devoted to proving Explicit Definability