Characters and fixed points in provability logic (Q749521)

This paper is devoted to study provability logic mainly by model- theoretic methods. Authors give a new proof of the fixed point theorem in the Gödel-Löb provability system GL, as well as the theorem on the joint satisfiability of formulas. From the last result, Craig's interpolation theorem is easily extracted. Beth's definability theorem is also among the corollaries of this theorem. The complexity of models for formulas of special kind, which describe the arrangement of worlds in Kripke models, are investigated.