This book treats modal logic as a theory, with several subtheories, such as completeness theory, correspondence theory, duality theory and transfer theory and is intended as a course in modal logic for students who have had prior contact with modal logic and who wish to study it more deeply. It presupposes training in mathematical or logic. Very little specific knowledge is presupposed, most results which are needed are proved in this book.

We consider the notion of structural completeness with respect to arbitrary (finitary and/or infinitary) inferential rules. Our main task is to characterize structurally complete intermediate logics. We prove that the structurally complete extension of any pure implicational in termediate logic C can be given as an extension of C with a certain family of schematically denned infinitary rules; the same rules are used for each C. The cardinality of the family is continuum and, in the case of (the pure implicational (...) fragment of) intuitionistic logic, the family cannot be reduced to a countable one. It means that the structurally complete extension of the intuitionistic logic is not countably axiomatizable by schematic rules. (shrink)

The paper considers certain properties of intermediate and moda propositional logics.The first part contains a proof of the theorem stating that each intermediate logic is closed under the Kreisel-Putnam rule xyz/(xy)(xz).

We show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.

We show that some common varieties of modal K4-algebras have finitary unification type, thus providing effective best solutions for equations in free algebras. Applications to admissible inference rules are immediate.

We characterize all finitary consequence relations over S4.3, both syntactically, by exhibiting so-called passive rules that extend the given logic, and semantically, by providing suitable strongly adequate classes of algebras. This is achieved by applying an earlier result stating that a modal logic L extending S4 has projective unification if and only if L contains S4.3. In particular, we show that these consequence relations enjoy the strong finite model property, and are finitely based. In this way, we extend the known (...) results by Bull and Fine, from logics, to consequence relations. We also show that the lattice of consequence relations over S4.3 is countable and distributive and it forms a Heyting algebra. (shrink)

A projective unifier for a modal formula A, over a modal logic L, is a unifier σ for A such that the equivalence of σ with the identity map is the consequence of A. Each projective unifier is a most general unifier for A. Let L be a normal modal logic containing S4. We show that every unifiable formula has a projective unifier in L iff L contains S4.3. The syntactic proof is effective. As a corollary, we conclude that all (...) normal modal logics L containing S4.3 are almost structurally complete, i.e. all admissible rules having unifiable premises are derivable in L. Moreover, L is structurally complete iff L contains McKinsey axiom M. (shrink)

We investigate finitarity of unification types in locally finite varieties of Heyting algebras, giving both positive and negative results. We make essential use of finite dualities within a conceptualization for E-unification theory 733–752) relying on the algebraic notion of a projective object.

We characterize (both from a syntactic and an algebraic point of view) the normal K4-logics for which unification is filtering. We also give a sufficient semantic criterion for existence of most general unifiers, covering natural extensions of K4.2⁺ (i.e., of the modal system obtained from K4 by adding to it, as a further axiom schemata, the modal translation of the weak excluded middle principle).

Unification was originally introduced in automated deduction and term rewriting, but has recently also found applications in other fields. In this article, we give a survey of the results on unification obtained in two closely related, yet different, application areas of unification: description logics and modal logics.

We show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations of finitely presented projective algebras.

Prior to investigating the degree of maximality of a propositional logic, as is the notion introduced by Ryszard Wojcicki [8], it is important to determine all structural consequence stronger than the logic considered. This characterization of all structural strengthenings was performed while establishing the degree of maximality for Lukasiewicz and Lukasiewicz-like logics [8], [4], [9], [5]. In these papers the authors used matrix consequences together with certain results concerning this notion and a representation theorem for Lukasiewicz algebras as given by (...) R. S. Grigolia [2]. (shrink)

The aim of this paper is to show that the operations of forming direct products and submatrices suffice to construct exhaustive semantics for all structural strengthenings of the consequence determined by a given class of logical matrices.