On the share of closed \(\mathsf {IL}\) formulas which are also in \(\mathsf {GL}\) (Q892132)

\(\mathsf{IL}\) is one of the basic systems in the family of interpretability logics which were founded on the analogy with Gödel and Löb provability logic \(\mathsf{GL}\). Whereas the latter introduces an unary modal operator formalizing provability, the former use a binary operator of interpretability. Thus we may evaluate not only an absolute strength of a formula against a theory but a relative strength with respect to some added formula. Researches on \(\mathsf{GL}\) profitably use methods devised for investigations on modal logics. Similarly, it seems that in the research on \(\mathsf{IL}\) it is valuable to use techniques applied sucessfully to \(\mathsf{GL}\). In particular, one of the nice features of \(\mathsf{GL}\) is the existence of regular normal forms for every closed formula. It was already shown by the first author and \textit{M. Vuković} [Math. Commun. 17, No. 1, 195--204 (2012; Zbl 1252.03138)] that such a result holds for a wide classes of \(\mathsf{IL}\) formulas; the main result of that work is recalled in Section 3. The aim of this article is to establish precisely how wide these classes are. In a purely syntactic way, the authors show that the ``majority'' of closed \(\mathsf{IL}\) formulas has equivalents in \(\mathsf{GL}\) and, consequently, the same normal forms as respective \(\mathsf{GL}\) formulas. Moreover, a convenient way of computing asymptotic behaviours of some general classes of formulas is provided; all considered classes are summarised in the tables closing the paper. The method of computation proposed by the authors seems to be of quite general use, in fact it is first described in Section 2 with no special reference to \(\mathsf{IL}\).