ABSTRACT A spatial logic is a modal logic of which the models are the mathematical models of space. Successively considering the mathematical models of space that are the incidence geometry and the projective geometry, we will successively establish the language, the semantical basis, the axiomatical presentation, the proof of the decidability and the proof of the completeness of INC, the modal multilogic of incidence geometry, and PRO, the modal multilogic of projective geometry.

A Mathematical Introduction to Logic, Second Edition, offers increased flexibility with topic coverage, allowing for choice in how to utilize the textbook in a course. The author has made this edition more accessible to better meet the needs of today's undergraduate mathematics and philosophy students. It is intended for the reader who has not studied logic previously, but who has some experience in mathematical reasoning. Material is presented on computer science issues such as computational complexity and database queries, with additional (...) coverage of introductory material such as sets. Increased flexibility of the text, allowing instructors more choice in how they use the textbook in courses. Reduced mathematical rigour to fit the needs of undergraduate students. (shrink)

In the pioneering article and two papers, written jointly with McKinsey, Tarski developed the so-called algebraic and topological frameworks for the Intuitionistic Logic and the Lewis modal system. In this paper, we present an outline of modern systems with a topological tinge. We consider topological interpretation of basic systems GL and G of the provability logic in terms of the Cantor derivative and the Hausdorff residue.

In this paper we introduce a new natural deduction system for the logic of lattices, and a number of extensions of lattice logic with different negation connectives. We provide the class of natural deduction proofs with both a standard inductive definition and a global graph-theoretical criterion for correctness, and we show how normalisation in this system corresponds to cut elimination in the sequent calculus for lattice logic. This natural deduction system is inspired both by Shoesmith and Smiley's multiple conclusion systems (...) for classical logic and Girard's proofnets for linear logic. (shrink)

We identify the computational complexity of the satisfiability problem for FO 2 , the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it has a finite (...) model. Moreover, Mortimer showed that every satisfiable FO 2 -sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO 2 -sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO 2 is NEXPTIME-complete. (shrink)

Algebraic work [9] shows that the deep theory of possible world semantics is available in the more general setting of substructural logics, at least in an algebraic guise. The question is whether it is also available in a relational form.This article seeks to set the stage for answering this question. Guided by the algebraic theory, but purely relationally we introduce a new type of frames. These structures generalize Kripke structures but are two-sorted, containing both worlds and co-worlds. These latter points (...) may be viewed as modelling irreducible increases in information where worlds model irreducible decreases in information. Based on these structures, a purely model theoretic and uniform account of completeness for the implication-fusion fragment of various substructural logics is given. Completeness is obtained via a generalization of the standard canonical model construction in combination with correspondence results. (shrink)

This first textbook on formal concept analysis gives a systematic presentation of the mathematical foundations and their relations to applications in computer science, especially in data analysis and knowledge processing. Above all, it presents graphical methods for representing conceptual systems that have proved themselves in communicating knowledge. The mathematical foundations are treated thoroughly and are illuminated by means of numerous examples, making the basic theory readily accessible in compact form.

This paper is a survey of results concerning embeddings of intuitionistic propositional logic and its extensions into various classical modal systems.

The contribution of this paper lies with providing a systematically specified and intuitive interpretation pattern and delineating a class of relational structures and models providing a natural interpretation of logical operators on an underlying propositional calculus of Positive Lattice Logic and subsequently proving a generic completeness theorem for the related class of logics, sometimes collectively referred to as Generalized Galois Logics.

We introduce the bimodal logic , which is the extension of Bennett’s bimodal logic by Grzegorczyk’s axiom □→p)→p and show that the lattice of normal extensions of the intuitionistic modal logic WS5 is isomorphic to the lattice of normal extensions of , thus generalizing the Blok–Esakia theorem. We also introduce the intuitionistic modal logic WS5.C, which is the extension of WS5 by the axiom →, and the bimodal logic , which is the extension of Shehtman’s bimodal logic by Grzegorczyk’s axiom, (...) and show that the lattice of normal extensions of WS5.C is isomorphic to the lattice of normal extensions of. (shrink)

This article presents an approach to the semantics of non-distributive propositional logics that is based on a lattice representation theorem that delivers a canonical extension of the lattice. Our approach supports both a plain Kripke-style semantics and, by restriction, a general frame semantics. Unlike the framework of generalized Kripke frames, the semantic approach presented in this article is suitable for modeling applied logics, as it respects the intended interpretation of the logical operators. This is made possible by restricting admissible interpretations.

This article addresses and resolves some issues of relational, Kripke-style, semantics for the logics of bounded lattice expansions with operators of well-defined distribution types, focusing on the case where the underlying lattice is not assumed to be distributive. It therefore falls within the scope of the theory of Generalized Galois Logics, introduced by Dunn, and it contributes to its extension. We introduce order-dual relational semantics and present a semantic analysis and completeness theorems for non-distributive lattice logic with n -ary additive (...) or multiplicative operators, with negation operators modally interpreted as impossibility and unnecessity, as well as with implication connectives. Order-dual relational semantics shares with the generalized Kripke frames, or the bi-approximation semantics approach, the use of both a satisfaction and a co-satisfaction relation, but it also responds to the recently voiced concerns of Craig, Haviar and Conradie about the relative non-intuitiveness of the 2-sorted semantics of the aforementioned approaches. In this article, we provide a standard interpretation of modalities and natural interpretations of both negation and implication, despite the absence of distribution. Thereby, our results contribute in creating the necessary background for research in non-distributive logics with modalities variously interpreted as dynamic, temporal etc, by analogy to the classical case. (shrink)

Part I of this paper is developed in the tradition of Stone-type dualities, where we present a new topological representation for general lattices (influenced by and abstracting over both Goldblatt's [17] and Urquhart's [46]), identifying them as the lattices of stable compact-opens of their dual Stone spaces (stability refering to a closure operator on subsets). The representation is functorial and is extended to a full duality.In part II, we consider lattice-ordered algebras (lattices with additional operators), extending the Jónsson and Tarski (...) representation results [30] for Boolean algebras with Operators. Our work can be seen as developing, and indeed completing, Dunn's project of gaggle theory [13, 14]. We consider general lattices (rather than Boolean algebras), with a broad class of operators, which we dubb normal, and which includes the Jónsson-Tarski additive operators. Representation of l-algebras is extended to full duality. (shrink)

We identify the computational complexity of the satisfiability problem for FO 2, the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it has a finite model. (...) Moreover, Mortimer showed that every satisfiable FO 2 -sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO 2 -sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO 2 is NEXPTIME-complete. (shrink)