Uniform interpolation for propositional and modal team logics

In this paper we consider modal team logic, a generalization of classical modal logic in which it is possible to describe dependence phenomena between data. We prove that most known fragments of full modal team logic allow the elimination of the so called ‘existential bisimulation quantifiers’, where the existence of a certain set is required only modulo bisimulation (i.e. not in the model itself but possibly in a bisimilar model). As a consequence, we prove that these fragments enjoy the uniform interpolation property.

NORMAL DERIVABILITY IN CLASSICAL NATURAL DEDUCTION

A normalization procedure is given for classical natural deduction with the standard rule of indirect proof applied to arbitrary formulas. For normal derivability and the subformula property, it is sufficient to permute down instances of indirect proof whenever they have been used for concluding a major premiss of an elimination rule. The result applies even to natural deduction for classical modal logic.

A new S4 classical modal logic in natural deduction

We show, first, that the normalization procedure for S4 modal logic presented by Dag Prawitz in [5] does not work. We then develop a new natural deduction system for S4 classical modal logic that is logically equivalent to that of Prawitz, and we show that every derivation in this new system can be transformed into a normal derivation.

Intuitionistic tense and modal logic

In this article we shall construct intuitionistic analogues to the main systems of classical tense logic. Since each classical modal logic can be gotten from some tense logic by one of the definitions(i) □ p ≡ p ∧ Gp ∧ Hp, ◇p ≡ p ∨ Fp ∨ Pp; or,(ii) □ p ≡ p ∧ Gp, ◇p = p ∨ Fp(see [5]), we shall find that our intuitionistic tense logics give us analogues to the classical modal logics as well.We shall not here discuss the philosophical issues raised by our logics. Readers interested in the intuitionistic view of time and modality should see [2] for a detailed discussion.In §2 we define the Kripke models for IKt, the intuitionistic analogue to Lemmon's system Kt. We then prove the completeness and decidability of this system (§§3–5). Finally, we extend our results to other sorts of tense logic and to modal logic.In the language of IKt, we have: sentence-letters p, q, r, etc.; the (intuitionistic) connectives ∧, ∨, →, ¬; and unary operators P (“it was the case”), F (it will be the case”), H (“it has always been the case”) and G (“it will always be the case”). Formulas are defined inductively: all sentence-letters are formulas; if X is a formula, so are ¬X, PX, FX, HX, and GX; if X and Y are formulas, so are X ∧ Y, X ∨ Y, and X → Y. We shall see that, in contrast to classical tense logic, F and P cannot be defined in terms of G and H.

Algebraic semantics for quasi-classical modal logics

A well-known result, going back to the twenties, states that, under some reasonable assumptions, any logic can be characterized as the set of formulas satisfied by a matrix 〈, F〉, where is an algebra of the appropriate type, and F a subset of the domain of , called the set of designated elements. In particular, every quasi-classical modal logic—a set of modal formulas, containing the smallest classical modal logic E, which is closed under the inference rules of substitution and modus ponens—is characterized by such a matrix, where now is a modal algebra, and F is a filter of . If the modal logic is in fact normal, then we can do away with the filter; we can study normal modal logics in the setting of varieties of modal algebras. This point of view was adopted already quite explicitly in McKinsey and Tarski [8]. The observation that the lattice of normal modal logics is dually isomorphic to the lattice of subvarieties of a variety of modal algebras paved the road for an algebraic study of normal modal logics. The algebraic approach made available some general results from Universal Algebra, notably those obtained by Jónsson [6], and thereby was able to contribute new insights in the realm of normal modal logics [2], [3], [4], [10].The requirement that a modal logic be normal is rather a severe one, however, and many of the systems which have been considered in the literature do not meet it. For instance, of the five celebrated modal systems, S1–S5, introduced by Lewis, S4 and S5 are the only normal ones, while only SI fails to be quasi-classical. The purpose of this paper is to generalize the algebraic approach so as to be applicable not just to normal modal logics, but to quasi-classical modal logics in general.