On the absence of finite approximation relative to model completeness in propositional provability logic

In the present paper we consider the expressibility of formulas in the provability logic $GL$ and related to it questions of the model completeness of system of formulas. We prove the absence of a finite approximation relative to model completeness in $GL$.