Under some assumptions on an equational theory S , we give a necessary and sufficient condition so that S admits a model completion. These assumptions are often met by the equational theories arising from logic. They say that the dual of the category of finitely presented S-algebras has some categorical stucture. The results of this paper combined with those of [7] show that all the 8 theories of amalgamable varieties of Heyting algebras [12] admit a model completion. Further applications to (...) varieties of modal algebras are given in [8]. (shrink)

We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, φ, built up from propositional variables (p,q,r,...) and falsity $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula φ there exists a formula Apφ (effectively computable from φ), containing only variables not equal to p which occur in φ, and such that for (...) all formulas ψ not involving $p, \vdash \psi \rightarrow A_p\phi$ if and only if $\vdash \psi \rightarrow \phi$ . Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions. An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra. (shrink)

We give a simple proof of the canonicity of Sahlqvist identities, using methods that were introduced in a paper by Jónsson and Tarski in 1951.

We show that (contrary to the parallel case of intuitionistic logic, see [7], [4]) there does not exist a translation fromS42 (the propositional modal systemS4 enriched with propositional quantifiers) intoS4 that preserves provability and reduces to identity for Boolean connectives and.

With each sentential logic C, identified with a structural consequence operation in a sentential language, the class Matr * (C) of factorial matrices which validate C is associated. The paper, which is a continuation of [2], concerns the connection between the purely syntactic property imposed on C, referred to as Maehara Interpolation Property (MIP), and three diagrammatic properties of the class Matr* (C): the Amalgamation Property (AP), the (deductive) Filter Extension Property (FEP) and Injections Transferable (IT). The main theorem of (...) the paper (Theorem 2.2) is analogous to the Wroski's result for equational classes of algebras [13]. It reads that for a large class of logics the conjunction of (AP) and (FEP) is equivalent to (IT) and that the latter property is equivalent to (MIP). (shrink)

We prove that certain natural sequent systems for bi-intuitionistic logic have the analytic cut property. In the process we show that the (global) subformula property implies the (local) analytic cut property, thereby demonstrating their equivalence. Applying a version of Maehara technique modified in several ways, we prove that bi-intuitionistic logic enjoys the classical Craig interpolation property and Maximova variable separation property; its Halldén completeness follows.

We investigate uniform interpolants in propositional modal logics from the proof-theoretical point of view. Our approach is adopted from Pitts’ proof of uniform interpolationin intuitionistic propositional logic [15]. The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculus for which structural rules are admissible.

In this paper we present a general theory of normal forms, based on a categorial result for the free monoid construction. We shall use the theory mainly for proposictional modal logic, although it seems to have a wider range of applications. We shall formally represent normal forms as combinatorial objects, basically labelled trees and forests. This geometric conceptualization is implicit in and our approach will extend it to other cases and make it more direct: operations of a purely geometric and (...) combinatorial nature will be introduced in order to give a mathematical description of the basic logical/algebraic constructions .We begin by recalling the above-mentioned categorial construction: we need a careful inspection of it because in the various examples considered later we plan to deduce from it in a uniform way the normal forms and the description of finitely generated free algebras. This method always works whenever we can describe the category of algebras corresponding to the logic under consideration as a T-objects category. When this simple description seems not to be available, still the general theory might be of some interest, because a description of the category of algebras as a T-objects category plus equation is possible .The central part of the paper is more advanced and specific: we show how the general approach presented here can provide some insights even in the basic case of the modal system K. Section 4 contains a contribution to the theory of normal forms, namely the description of the uniform substitution. This result will enable us to give a duality theorem for the category of finitely generated free modal algebras and in Section 5 to provide a characterization of the collections of normal forms which happen to be normal forms for a logic, thus giving a description of the lattice of modal logics.Section 6 deals with some applications: we shall show how to use normal forms in order to prove for the modal system K the definability of higher-order propositional quantifiers and of the tense operator F .As to the prerequisites, the paper is almost self-contained. The reader is only assumed to have familiarity with standard techniques in algebraic logic ). Knowledge of the basic facts about adjoint functors is required too, see e.g. McLane or the appendix. (shrink)

In this paper we show that a variety of modal algebras of finite type is semisimple iff it is discriminator iff it is both weakly transitive and cyclic. This fact has been claimed already in [4] (based on joint work by the two authors) but the proof was fatally flawed.