 In order to be able to speak in a modal language about important distinctions between theories, researchers have extended provability logic in many different ways. Let us mention a few. One extension is to add a binary modality \(\interprets\), where for a given arithmetical theory \(T\), the modal sentence \(A \interprets B\) is meant to stand for “\(T+B\) is interpretable in \(T+A\)” (Švejdar, 1983). De Jongh and Veltman (1990) investigated modal semantics for several interpretability logics, while De Jongh and Visser (1991) proved the explicit fixed-point property for the most important ones. Visser characterized the interpretability logic of the most common finitely axiomatized theories, and Berarducci and Shavrukov independently characterized the one for PA, which is not finitely axiomatizable. It appears that indeed, the interpretability logic of finitely axiomatizable theories is different from the interpretability logic of Peano Arithmetic (see Montagna 1987; Visser 1990, 1998; Berarducci 1990, Shavrukov 1988; Joosten and Visser 2000).