Basic Logic, SMT solvers and finitely generated varieties of GBL-algebras

We show how to implement an effective decision procedure to check if a propositional Basic Logic formula is a tautology. For a formula with $n$ variables, the procedure consists of a translation, depending on $n$, from Basic Logic to the language of Satisfiability Modulo Theories SMT-LIB2 using the theory of quantifier free linear real arithmetic. Many efficient SMT-solvers exist to decide formulas in the SMT-LIB2 language. We also study finitely generated varieties of Basic Logic (BL-)algebras and give a description of the lattice of these varieties. Extensions to finitely generated varieties of Generalized BL-algebras are discussed, and a simple connection between finite GBL-algebras and finite closure algebras is noted.

Free algebras in the variety of three-valued closure algebras

In this paper, the variety of three-valued closure algebras, that is, closure algebras with the property that the open elements from a three-valued Heyting algebra, is investigated. Particularly, the structure of the finitely generated free objects in this variety is determined.

Complexity of interpolation and related problems in positive calculi

We consider the problem of recognizing important properties of logical calculi and find complexity bounds for some decidable properties. For a given logical system L, a property P of logical calculi is called decidable over L if there is an algorithm which for any finite set Ax of new axiom schemes decides whether the calculus L + Ax has the property P or not. In [11] the complexity of tabularity, pre-tabularity. and interpolation problems over the intuitionistic logic Int and over modal logic S4 was studied, also we found the complexity of amalgamation problems in varieties of Heyting algebras and closure algebras.In the present paper we deal with positive calculi. We prove NP-completeness of tabularity, DP-hardness of pretabularity and PSPACE-completeness of interpolation problem over Int+. In addition to above-mentioned properties, we consider Beth's definability properties. Also we improve some complexity bounds for properties of superintuitionistic calculi.

The contributions of Alfred Tarski to algebraic logic

One of the most extensive parts of Tarski's contributions to logic is his work on the algebraization of the subject. His work here involves Boolean algebras, relation algebras, cylindric algebras, Boolean algebras with operators, Brouwerian algebras, and closure algebras. The last two are less developed in his work, although his contributions are basic to other work in those subjects. At any rate, not being conversant with the latest developments in those fields, we shall concentrate on an exposition of Tarski's work in the first four areas, trying to put them in the perspective of present-day developments.For useful comments, criticisms, and suggestions, the author is indebted to Steven Givant, Leon Henkin, Wilfrid Hodges, Bjarni Jónsson, Roger Lyndon, and Robert Vaught.

Cocompactness in algebra and topology

This paper discusses two notions, developed independently and both termed “cocompactness”. The first arises in the area of topology, where J. de Groot and others have studied spaces which are, in a certain sense, complementary to a given space. If the given space is compact then the complementary spaces are said to be cocompact. The second concept arises in the area of logic and general algebra. Loosely speaking a logic is compact if every inconsistent set of formulas has a finite inconsistent subset. This notion of compactness may be generalized to any closure algebra and the use of the term “cocompactness” to describe the generalization was suggested to the author by Dr. R. A. Bull.It is shown here that topological and algebraic cocompactness are related in the following ways. Firstly, if a closure algebra is algebraically cocompact then its dual space is topologjcally cocompact, and conditions may be given for the implication to be reversible.3 Furthermore any cocompact topological space may be represented as the continuous 1-1 image of the dual space of a cocompact closure algebra. A final result relates another class of closure algebras with those topological spaces which are compact.