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.

This paper exhibits a general and uniform method to prove axiomatic completeness for certain modal fixpoint logics. Given a set Γ of modal formulas of the form γ, where x occurs only positively in γ, we obtain the flat modal fixpoint language by adding to the language of polymodal logic a connective γ for each γΓ. The term γ is meant to be interpreted as the least fixed point of the functional interpretation of the term γ. We consider the following (...) problem: given Γ, construct an axiom system which is sound and complete with respect to the concrete interpretation of the language on Kripke structures. We prove two results that solve this problem.First, let be the logic obtained from the basic polymodal by adding a Kozen–Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective γ. Provided that each indexing formula γ satisfies a certain syntactic criterion, we prove this axiom system to be complete.Second, addressing the general case, we prove the soundness and completeness of an extension of . This extension is obtained via an effective procedure that, given an indexing formula γ as input, returns a finite set of axioms and derivation rules for γ, of size bounded by the length of γ. Thus the axiom system is finite whenever Γ is finite. (shrink)