Definable fixed points in modal and temporal logics — a survey
---
paper_title: The uniqueness of the fixed-point in every diagonalizable algebra

paper_content:

It is well known that, in Peano arithmetic, there exists a formulaTheor (x) which numerates the set of theorems. By Godel's and Lob's results, we have that ::: Open image in new window ::: Therefore, the considered «equations» admit, up to provable equivalence, only one solution.
---
paper_title: Admissibility of Logical Inference Rules

paper_content:

Preface and acknowledgments. Introduction. Syntaxes and Semantics. Syntax of formal logic systems. First-order semantics and universal algebra. Algebraic semantics for propositional logics. Admissible rules in algebraic logics. Logical consequence relations. Algebraizable consequence relations. Admissibility for consequence relations. Lattices of logical consequences. Semantics for Non-Standard Logics. Algebraic semantics for intuitionistic logic. Algebraic semantics, modal and tense logics. Kripke semantics for modal and temporal logic. Kripke semantics for intuitionistic logic. Stone's theory and Kripke semantics. The finite model property. Relation of intuitionistic and modal logics. Advanced tools for the finite model property. Kripke incomplete logics. Advanced tools for Kripke completeness.Criteria for Admissibility. Reduced forms. T--translation of inference rules. Semantic criteria for admissibility. Some technical lemmas. Criteria for determining admissibility. Elementary theories of free algebras. Scheme--logics of first--order theories. Some counterexamples. Admissibility through reduced forms. Bases for Inference Rules. Initial auxiliary results. The absence of finite bases. Bases for some strong logics. Bases for valid rules of tabular logics. Tabular logics without independent bases. Structural Completeness. General properties, descriptions. Quasi--characteristic inference rules. Some preliminary technical results. Hereditary structural completeness. Structurally complete fragments. Related Questions. Rules with meta--variables. The preservation of admissible for S4 rules. The preservation of admissibility for H. Non-compact modal logics. Decidable Kripke non--compact logics. Non--compact superintuitionistic logics. Index. Bibliography.
---
paper_title: Fixed Points in Tense Models

paper_content:

We study into definability of least fixed points in tense logic. It is proved that least fixed points of tense positive Σ-operators are definable in transitive linear models. Examples are furnished showing that the least fixed points of tense positive operators may fail to be definable in the class of finite linearly ordered models, and the class of finite strictly linearly ordered models. Moreover, in dealing with the modal case, we point out examples of the non-definable inflationary points in the model classes mentioned.
---
paper_title: An effective fixed-point theorem in intuitionistic diagonalizable algebras

paper_content:

Within the technical frame supplied by the algebraic variety of diagonalizable algebras, defined by R. Magari in [2], we prove the following:
---
paper_title: An Introduction to Inductive Definitions

paper_content:

Publisher Summary Inductive definitions of sets are often informally presented by giving some rules for generating elements of the set and then adding that an object is to be in the set only if it has been generated according to the rules. An equivalent formulation is to characterize the set as the smallest set closed under the rules. This chapter discusses monotone induction and its role in extensions of recursion theory. The chapter reviews some of the work on non-monotone induction and outlines the separate motivation that has led to its development. The chapter briefly considers inductive definitions in a more general context.
---
paper_title: Results on the Propositional µ-Calculus

paper_content:

We define a propositional version of the µ-calculus, and give an exponential-time decision procedure, small model property, and complete deductive system. We also show that it is strictly more expressive than PDL. Finally we give an algebraic semantics and prove a representation theorem.
---
paper_title: Inflationary fixed points in modal logic

paper_content:

We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal μ-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed-point operators have been studied and compared in other contexts, particularly in finite model theory, where it is known that the logics IFP and LFP that result from adding such fixed-point operators to first-order logic have equal expressive power. As we show, the situation in modal logic is quite different, as the modal iteration calculus (MIC), we introduce has much greater expressive power than the μ-calculus. Greater expressive power comes at a cost: the calculus is algorithmically much less manageable.
---
paper_title: Inflationary Fixed Points in Modal Logic

paper_content:

We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal µ-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed point operators have been studied and compared in other contexts, particularly in finite model theory, where it is known that the logics IFP and LFP that result from adding such fixed point operators to first order logic have equal expressive power. As we show, the situation in modal logic is quite different, as the modal iteration calculus (MIC) we introduce has much greater expressive power than the µ-calculus. Greater expressive power comes at a cost: the calculus is algorithmically much less manageable.
---
paper_title: Admissibility of Logical Inference Rules

paper_content:

Preface and acknowledgments. Introduction. Syntaxes and Semantics. Syntax of formal logic systems. First-order semantics and universal algebra. Algebraic semantics for propositional logics. Admissible rules in algebraic logics. Logical consequence relations. Algebraizable consequence relations. Admissibility for consequence relations. Lattices of logical consequences. Semantics for Non-Standard Logics. Algebraic semantics for intuitionistic logic. Algebraic semantics, modal and tense logics. Kripke semantics for modal and temporal logic. Kripke semantics for intuitionistic logic. Stone's theory and Kripke semantics. The finite model property. Relation of intuitionistic and modal logics. Advanced tools for the finite model property. Kripke incomplete logics. Advanced tools for Kripke completeness.Criteria for Admissibility. Reduced forms. T--translation of inference rules. Semantic criteria for admissibility. Some technical lemmas. Criteria for determining admissibility. Elementary theories of free algebras. Scheme--logics of first--order theories. Some counterexamples. Admissibility through reduced forms. Bases for Inference Rules. Initial auxiliary results. The absence of finite bases. Bases for some strong logics. Bases for valid rules of tabular logics. Tabular logics without independent bases. Structural Completeness. General properties, descriptions. Quasi--characteristic inference rules. Some preliminary technical results. Hereditary structural completeness. Structurally complete fragments. Related Questions. Rules with meta--variables. The preservation of admissible for S4 rules. The preservation of admissibility for H. Non-compact modal logics. Decidable Kripke non--compact logics. Non--compact superintuitionistic logics. Index. Bibliography.
---
paper_title: Convergence of positive schemes in S4 and int

paper_content:

A condition to be imposed on a model is proposed that is sufficient for a modal positive scheme in the logic S4 to converge in a finite number of steps. As a consequence, it is inferred that in intuitionistic logic, positive schemes converge in a finite number of steps.
---
paper_title: A new proof of the fixed-point theorem of provability logic

paper_content:

We give a simple semantic proof of the fixed-point theorem of the modal system G (also known as GL, PRL, L, and K4W). It is modeled after a syntactic proof of Sambin, yet is simpler than his, due to our taking advantage of the Kripke semantics for G. The advantages of this particular version are that it is les complicated and the fixed-point so obtained has the same general «appearance» as the original formula
---
paper_title: Admissibility of Logical Inference Rules

paper_content:

Preface and acknowledgments. Introduction. Syntaxes and Semantics. Syntax of formal logic systems. First-order semantics and universal algebra. Algebraic semantics for propositional logics. Admissible rules in algebraic logics. Logical consequence relations. Algebraizable consequence relations. Admissibility for consequence relations. Lattices of logical consequences. Semantics for Non-Standard Logics. Algebraic semantics for intuitionistic logic. Algebraic semantics, modal and tense logics. Kripke semantics for modal and temporal logic. Kripke semantics for intuitionistic logic. Stone's theory and Kripke semantics. The finite model property. Relation of intuitionistic and modal logics. Advanced tools for the finite model property. Kripke incomplete logics. Advanced tools for Kripke completeness.Criteria for Admissibility. Reduced forms. T--translation of inference rules. Semantic criteria for admissibility. Some technical lemmas. Criteria for determining admissibility. Elementary theories of free algebras. Scheme--logics of first--order theories. Some counterexamples. Admissibility through reduced forms. Bases for Inference Rules. Initial auxiliary results. The absence of finite bases. Bases for some strong logics. Bases for valid rules of tabular logics. Tabular logics without independent bases. Structural Completeness. General properties, descriptions. Quasi--characteristic inference rules. Some preliminary technical results. Hereditary structural completeness. Structurally complete fragments. Related Questions. Rules with meta--variables. The preservation of admissible for S4 rules. The preservation of admissibility for H. Non-compact modal logics. Decidable Kripke non--compact logics. Non--compact superintuitionistic logics. Index. Bibliography.
---
paper_title: Admissibility of Logical Inference Rules

paper_content:

Preface and acknowledgments. Introduction. Syntaxes and Semantics. Syntax of formal logic systems. First-order semantics and universal algebra. Algebraic semantics for propositional logics. Admissible rules in algebraic logics. Logical consequence relations. Algebraizable consequence relations. Admissibility for consequence relations. Lattices of logical consequences. Semantics for Non-Standard Logics. Algebraic semantics for intuitionistic logic. Algebraic semantics, modal and tense logics. Kripke semantics for modal and temporal logic. Kripke semantics for intuitionistic logic. Stone's theory and Kripke semantics. The finite model property. Relation of intuitionistic and modal logics. Advanced tools for the finite model property. Kripke incomplete logics. Advanced tools for Kripke completeness.Criteria for Admissibility. Reduced forms. T--translation of inference rules. Semantic criteria for admissibility. Some technical lemmas. Criteria for determining admissibility. Elementary theories of free algebras. Scheme--logics of first--order theories. Some counterexamples. Admissibility through reduced forms. Bases for Inference Rules. Initial auxiliary results. The absence of finite bases. Bases for some strong logics. Bases for valid rules of tabular logics. Tabular logics without independent bases. Structural Completeness. General properties, descriptions. Quasi--characteristic inference rules. Some preliminary technical results. Hereditary structural completeness. Structurally complete fragments. Related Questions. Rules with meta--variables. The preservation of admissible for S4 rules. The preservation of admissibility for H. Non-compact modal logics. Decidable Kripke non--compact logics. Non--compact superintuitionistic logics. Index. Bibliography.
---
paper_title: Negative modal schemes

paper_content:

We deal with the question of whether solutions of modal propositional negative schemes are definable on Kripke models. It is shown that there exists a formula by which a solution of such a scheme is defined in every Kripke model with the ascending chain condition, in which the solution exists. We present an algorithm for constructing such a defining formula.
---
paper_title: Inflationary fixed points in modal logic

paper_content:

We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal μ-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed-point operators have been studied and compared in other contexts, particularly in finite model theory, where it is known that the logics IFP and LFP that result from adding such fixed-point operators to first-order logic have equal expressive power. As we show, the situation in modal logic is quite different, as the modal iteration calculus (MIC), we introduce has much greater expressive power than the μ-calculus. Greater expressive power comes at a cost: the calculus is algorithmically much less manageable.
---
paper_title: Inflationary Fixed Points in Modal Logic

paper_content:

We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal µ-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed point operators have been studied and compared in other contexts, particularly in finite model theory, where it is known that the logics IFP and LFP that result from adding such fixed point operators to first order logic have equal expressive power. As we show, the situation in modal logic is quite different, as the modal iteration calculus (MIC) we introduce has much greater expressive power than the µ-calculus. Greater expressive power comes at a cost: the calculus is algorithmically much less manageable.
---
paper_title: Fixed Points in Tense Models

paper_content:

We study into definability of least fixed points in tense logic. It is proved that least fixed points of tense positive Σ-operators are definable in transitive linear models. Examples are furnished showing that the least fixed points of tense positive operators may fail to be definable in the class of finite linearly ordered models, and the class of finite strictly linearly ordered models. Moreover, in dealing with the modal case, we point out examples of the non-definable inflationary points in the model classes mentioned.
---
paper_title: Uniform interpolation, automata and the modal µ-calculus

paper_content:

A logic has interpolation if whenever we have two formulas and such that j then there is a formula I in the common language of and and in our logic of course such that j I j This intermediate formula is called the interpolant By the language of a formula we mean the non logical symbols i e the atomic actions and propositional constants that occur in it This notion is familiar from rst order logic and is known there as Craig Interpolation
---
paper_title: Automata for the µcalculus and Related Results

paper_content:

The propositional Μ-calculus as introduced by Kozen in [4] is considered. The notion of disjunctive formula is defined and it is shown that every formula is semantically equivalent to a disjunctive formula. For these formulas many difficulties encountered in the general case may be avoided. For instance, satisfiability checking is linear for disjunctive formulas. This kind of formula gives rise to a new notion of finite automaton which characterizes the expressive power of the Μ-calculus over all transition systems.
---

Title: Definable fixed points in modal and temporal logics — a survey

Section 1: Introduction
Description 1: Introduce the general background, problem definition, and purpose of the survey.

Section 2: The least fixed points
Description 2: Discuss the conditions under which the least fixed points are definable in modal logic and provide examples.

Section 3: E-frames
Description 3: Define E-frames and provide examples of E-frames in which least fixed points are definable.

Section 4: SE-frames
Description 4: Discuss SE-frames and the conditions for definability of least fixed points within these frames.

Section 5: IRE-frames
Description 5: Introduce IRE-frames and explore their properties related to fixed point definability.

Section 6: Switches of truth values
Description 6: Examine how switches of truth values affect the definability of least fixed points in Kripke models.

Section 7: Σ-and Π-formulas
Description 7: Explore the roles of Σ and Π formulas in defining least fixed points in modal logic.

Section 8: Partial orders with the ascending chain condition
Description 8: Discuss the definability of least fixed points in partially ordered Kripke models with the ascending chain condition.

Section 9: C-frames
Description 9: Define C-frames and discuss their importance in the study of definable fixed points.

Section 10: SC-frames
Description 10: Introduce SC-frames and explore their relationship with definable fixed points.

Section 11: Negative operators
Description 11: Investigate the fixed points of negative operators and their uniqueness in various models.

Section 12: Temporal positive operators
Description 12: Analyze the definability of least fixed points for temporal positive operators in temporal logic.

Section 13: Inflationary fixed points
Description 13: Discuss the concept of inflationary fixed points and their relationship to definable fixed points in modal logics.

Section 14: Graded modalities
Description 14: Explore graded modalities and their role in the definability of least fixed points.

Section 15: Problems
Description 15: Present open problems and remaining challenges related to definable fixed points in modal and temporal logics.