A new proof of the fixed-point theorem of provability logic (Q923072)

A semantic proof of the fixed-point theorem for the modal logic G of provability is given, modeled after Sambin's syntactic proof, which is rather complicated but provides algorithms for the explicit calculation of fixed-points. The new proof featuring Kripke models is simple and shows an algorithm for fixed-point calculation as well, with which the fixed-point is obtained in the same general appearance as the original formula. Some examples of fixed-point calculations are also given.