Axiomatizing fixpoint logics (Q1190508)

An approach to axiomatize fixpoint logics is presented. Here fixpoint logics are considered to set the methodological environment for the semantics of multimodal logics definable by fixpoint equations. There are two main differences between this approach to be outlined and the approach based upon the \(\mu\)-calculus: (1) Functionals are required to be continuous, wheras in \(\mu\)-calculus only their monotonicity is assumed. (2) No particular language of the logics characterized is considered. The second point is of little avail to the strength of fixpoint logics, but, from a purely theoretical point of view, the required continuity of functionals weakens the fixpoint approach. However, reasonable assumptions about the nature of practical computations performed by computers make up for this weakness. This sets the stage for the presentation of logics that meet the following prerequisites: (a) The logic in question is a set of well-formed formulas. (b) There are admissible interpretations. (c) The logic in question is an extension of classical first-order logic and has model-theoretic semantics. (d) Nonclassical connectives are definable at a meta-level by fixpoints of continuous functionals. Algorithmic logic, dynamic logic and temporal logic are subjected to this approach with rewarding return.