We present a sequent calculus for the Grzegorczyk modal logic $\mathsf {Grz}$ allowing cyclic and other non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elimination mapping acting on these proofs. As an application, we establish the Lyndon interpolation property for the logic $\mathsf {Grz}$ proof-theoretically.

We consider Hilbert-style non–well-founded derivations in the Gödel-Löb provability logic GL and establish that GL with the obtained derivability relation is globally complete for algebraic and neighbourhood semantics.

For the modal logic |$\textsf {S4}^{C}_{I}$|⁠, we identify the class of completable |$\textsf {S4}^{C}_{I}$|-algebras and prove for them a Stone-type representation theorem. As a consequence, we obtain strong algebraic and topological completeness of the logic |$\textsf {S4}^{C}_{I}$| in the case of local semantic consequence relations. In addition, we consider an extension of the logic |$\textsf {S4}^{C}_{I}$| with certain infinitary derivations and establish the corresponding strong completeness results for the enriched system in the case of global semantic consequence relations.