We prove, by using the concept of schematic interpretation, that the natural embedding from the category ISL, of intuitionistic sentential pretheories and i-congruence classes of morphisms, to the category CSL, of classical sentential pretheories and c-congruence classes of morphisms, has a left adjoint, which is related to the double negation interpretation of Gödel-Gentzen, and a right adjoint, which is related to the Law of Excluded Middle. Moreover, we prove that from the left to the right adjoint there is a pointwise (...) epimorphic natural transformation and that since the two endofunctors at CSL, obtained by adequately composing the aforementioned functors, are naturally isomorphic to the identity functor for CSL, the string of adjunctions constitutes an adjoint cylinder. On the other hand, we show that the operators of Lindenbaum-Tarski of formation of algebras from pretheories can be extended to equivalences of categories from the category CSL, respectively, ISL, to the category Bool, of Boolean algebras, respectively, Heyt, of Heyting algebras. Finally, we prove that the functor of regularization from Heyt to Bool has, in addition to its well-known right adjoint (that is, the canonical embedding of Bool into Heyt) a left adjoint, that from the left to the right adjoint there is a pointwise epimorphic natural transformation, and, finally, that such a string of adjunctions constitutes an adjoint cylinder. (shrink)

We consider the theory Thprin of Boolean algebras with a principal ideal, the theory Thmax of Boolean algebras with a maximal ideal, the theory Thac of atomic Boolean algebras with an ideal where the supremum of the ideal exists, and the theory Thsa of atomless Boolean algebras with an ideal where the supremum of the ideal exists. First, we find elementary invariants for Thprin and Thsa. If T is a theory in a first order language and (...) α is a linear order with least element, then we let Sentalg be the Lindenbaum-Tarski algebra with respect to T, and we let intalg be the interval algebra of α. Using rank diagrams, we show that Sentalg ⋍ intalg, Sentalg ⋍ intalg ⋍ Sentalg, and Sentalg ⋍ intalg. For Thmax and Thac we use Ershov's elementary invariants of these theories. We also show that the algebra of formulas of the theory Tx of Boolean algebras with finitely many ideals is atomic. (shrink)

This book is well known for its proof that many mathematical systems - including lattice theory and closure algebras - are undecidable. It consists of three treatises from one of the greatest logicians of all time: "A General Method in Proofs of Undecidability," "Undecidability and Essential Undecidability in Mathematics," and "Undecidability of the Elementary Theory of Groups.".

Shramko [. Truth, falsehood, information and beyond: The American plan generalized. In K. Bimbo, J. Michael Dunn on information based logics, outstanding contributions to logic...

In this paper we introduce a class of inquisitive Heyting algebras as algebraic structures that are isomorphic to algebras of finite antichains of bounded implicative meet semilattices. It is argued that these structures are suitable for algebraic semantics of inquisitive superintuitionistic logics, i.e. logics of questions based on intuitionistic logic and its extensions. We explain how questions are represented in these structures and provide several alternative characterizations of these algebras. For instance, it is shown that a Heyting (...) algebra is inquisitive if and only if its prime filters and filters generated by sets of prime elements coincide and prime elements are closed under relative pseudocomplement. We prove that the weakest inquisitive superintuitionistic logic is sound with respect to a Heyting algebra iff the algebra is what we call a homomorphic p-image of some inquisitive Heyting algebra. It is also shown that a logic is inquisitive iff its Lindenbaum–Tarski algebra is an inquisitive Heyting algebra. (shrink)

Lawvere hyperdoctrines give categorical algebraic semantics for intuitionistic predicate logic. Here we extend the hyperdoctrinal semantics to a broad variety of substructural predicate logics over the Typed Full Lambek Calculus, verifying their completeness with respect to the extended hyperdoctrinal semantics. This yields uniform hyperdoctrinal completeness results for numerous logics such as different types of relevant predicate logics and beyond, which are new results on their own; i.e., we give uniform categorical semantics for a broad variety of non-classical predicate logics. And (...) we introduce an analogue of Lawvere–Tierney topology and cotopology in the hyperdoctrinal setting, which gives a unifying perspective on different logical translations, in particular allowing for a uniform treatment of Girard’s exponential translation between linear and intuitionistic logics and of Kolmogorov’s double negation translation between intuitionistic and classical logics. In the hyerdoctrinal conception, type theories are categories, logics over type theories are functors, and logical translations between them, then, are natural transformations, in particular Lawvere–Tierney topologies and cotopologies on hyperdoctrines. The view of logical translations as hyperdoctrinal Lawvere–Tierney topologies and cotopologies has not been elucidated before, and may be seen as a novel contribution of the present work. From a broader perspective, this work may be regarded as taking first steps towards interplay between algebraic and categorical logics; it is, technically, a combination of substructural algebraic logic and hyperdoctrinal categorical logic, as the hyperdoctrinal completeness theorem is shown via the integration of the Lindenbaum–Tarski algebra construction with the syntactic category construction. As such this work lays a foundation for further interactions between algebraic and categorical logics. (shrink)

Post algebras of order + as a semantic foundation for +-valued predicate calculi were examined in [5]. In this paper Post spaces of order + being a modification of Post spaces of order n2 (cf. Traczyk [8], Dwinger [1], Rasiowa [6]) are introduced and Post fields of order + are defined. A representation theorem for Post algebras of order + as Post fields of sets is proved. Moreover necessary and sufficient conditions for the existence of representations preserving a (...) given set of infinite joins and infinite meets are established and applied to Lindenbaum-Tarski algebras of elementary theories based on +-valued predicate calculi in order to obtain a topological characterization of open theories. (shrink)

Orthologic is defined by weakening the axioms and rules of inference of the classical propositional calculus. The resulting Lindenbaum-Tarski quotient algebra is an orthoimplication algebra which generalizes the author's implication algebra. The associated order structure is a semi-orthomodular lattice. The theory of orthomodular lattices is obtained by adjoining a falsity symbol to the underlying orthologic or a least element to the orthoimplication algebra.

In Part I of this paper, we identified and compared various schemes for trivalent truth conditions for indicative conditionals, most notably the proposals by de Finetti and Reichenbach on the one hand, and by Cooper and Cantwell on the other. Here we provide the proof theory for the resulting logics DF/TT and CC/TT, using tableau calculi and sequent calculi, and proving soundness and completeness results. Then we turn to the algebraic semantics, where both logics have substantive limitations: DF/TT allows for (...) algebraic completeness, but not for the construction of a canonical model, while CC/TT fails the construction of a Lindenbaum-Tarski algebra. With these results in mind, we draw up the balance and sketch future research projects. (shrink)

In 1988, J. Ivlev proposed some (non-normal) modal systems which are semantically characterized by four-valued non-deterministic matrices in the sense of A. Avron and I. Lev. Swap structures are multialgebras (a.k.a. hyperalgebras) of a special kind, which were introduced in 2016 by W. Carnielli and M. Coniglio in order to give a non-deterministic semantical account for several paraconsistent logics known as logics of formal inconsistency, which are not algebraizable by means of the standard techniques. Each swap structure induces naturally a (...) non-deterministic matrix. The aim of this paper is to obtain a swap structures semantics for some Ivlev-like modal systems proposed in 2015 by M. Coniglio, L. Fariñas del Cerro and N. Peron. Completeness results will be stated by means of the notion of Lindenbaum–Tarski swap structures, which constitute a natural generalization to multialgebras of the concept of Lindenbaum–Tarski algebras. (shrink)

Two famous negative results about da Costa’s paraconsistent logic ${\mathscr {C}}_1$ (the failure of the Lindenbaum–Tarski process [44] and its non-algebraizability [39]) have placed ${\mathscr {C}}_1$ seemingly as an exception to the scope of Abstract Algebraic Logic (AAL). In this paper we undertake a thorough AAL study of da Costa’s logic ${\mathscr {C}}_1$. On the one hand, we strengthen the negative results about ${\mathscr {C}}_1$ by proving that it does not admit any algebraic semantics whatsoever in the sense (...) of Blok and Pigozzi (a weaker notion than algebraizability also introduced in the monograph [6]). On the other hand, ${\mathscr {C}}_1$ is a protoalgebraic logic satisfying a Deduction-Detachment Theorem (DDT). We then extend our AAL study to some paraconsistent axiomatic extensions of ${\mathscr {C}}_1$ covered in the literature. We prove that for extensions ${\mathcal {S}}$ such as ${\mathcal {C}ilo}$ [26], every algebra in ${\mathsf {Alg}}^*({\mathcal {S}})$ contains a Boolean subalgebra, and for extensions ${\mathcal {S}}$ such as,, or [16, 53], every subdirectly irreducible algebra in ${\mathsf {Alg}}^*({\mathcal {S}})$ has cardinality at most 3. We also characterize the quasivariety ${\mathsf {Alg}}^*({\mathcal {S}})$ and the intrinsic variety $\mathbb {V}({\mathcal {S}})$, with,, and. (shrink)

There is a well-established correspondence between interpolation and amalgamation for algebraizable logics that satisfy certain additional assumptions. In this paper, we introduce the Robinson property of a logic and show that a conditionally algebraizable logic without any additional assumptions has the Robinson property if and only if the corresponding class of Lindenbaum–Tarski algebras has the amalgamation property. Moreover, we give the logical characterization of the strong amalgamation property, solving an open problem of Andréka–Németi–Sain. It is also shown (...) that given the mentioned extra assumptions the Robinson property implies the interpolation property. As conditionally algebraizable logics cover algebraizable logics as well as various quantifier logics such as classical first order logic, our results yield a generalization of some of the results concerning interpolation and amalgamation. (shrink)

In this paper we give an axiom system of a logic which we call an approximation logic (AL), whose Lindenbaum-Tarski algebra is a strong Bunge algebra (or simply s-Bunge algebra), and show thatFor every s-Bunge algebra , a quotient algebra by a maximal filter is isomorphic to the simplest nontrivial s-Bunge algebra ;The Lindenbaum algebra of AL is an s-Bunge algebra;AL is complete;AL is decidable.

One of the most expected properties of a logical system is that it can be algebraizable, in the sense that an algebraic counterpart of the deductive machinery could be found. Since the inception of da Costa's paraconsistent calculi, an algebraic equivalent for such systems have been searched. It is known that these systems are non self-extensional (i.e., they do not satisfy the replacement property). More than this, they are not algebraizable in the sense of Blok-Pigozzi. The same negative results hold (...) for several systems of the hierarchy of paraconsistent logics known as Logics of Formal Inconsistency (LFIs). Because of this, these logics are uniquely characterized by semantics of non-deterministic kind. This paper offers a solution for two open problems in the domain of paraconsistency, in particular connected to algebraization of LFIs, by obtaining several LFIs weaker than C1, each of one is algebraizable in the standard Lindenbaum-Tarski's sense by a suitable variety of Boolean algebras extended with operators. This means that such LFIs satisfy the replacement property. The weakest LFI satisfying replacement presented here is called RmbC, which is obtained from the basic LFI called mbC. Some axiomatic extensions of RmbC are also studied, and in addition a neighborhood semantics is defined for such systems. It is shown that RmbC can be defined within the minimal bimodal non-normal logic E+E defined by the fusion of the non-normal modal logic E with itself. Finally, the framework is extended to first-order languages. RQmbC, the quantified extension of RmbC, is shown to be sound and complete w.r.t. BALFI semantics. (shrink)

The starting point for the investigation in this paper is the following McKinsey-Tarski's Theorem: if f and g are algebraic functions (of the same number of variables) in a topological Boolean algebra (TBA) and if C(f)C(g) vanishes identically, then either f or g vanishes identically. The present paper generalizes this theorem to B-algebras and shows that validity of that theorem in a variety of B-algebras (B-variety) generated by SCI B -equations implies that its free Lindenbaum-Tarski's (...) algebra is normal. This is important in the semantical analysis of SCI B (the Boolean strengthening of the sentential calculus with identity, SCI) since normal B-algebras are just models of this logic. The rest part of the paper is concerned with relationships between some closure systems of filters, SCI B -theories, B-varieties and closed sets of SCI B -equations that have been derived both from the semantics of SCI B and from the semantics of the usual equational logic. (shrink)

In this work we will study Tarski algebras endowed with a subordination, called subordination Tarski algebras. We will define the notion of round filters, and we will study the class of irreducible round filters and the maximal round filters, called ends. We will prove that the poset of all round filters is a lattice isomorphic to the lattice of the congruences that are compatible with the subordination. We will prove that every end is an irreducible round (...) filter, and that in a topological subordination Tarski algebra A, every irreducible round filter is an end iff A is a monadic subordination Tarski algebra. As corollary of this result we have that the variety of monadic Tarski algebra can be characterised as the topological Tarski algebras where every irreducible open filter is a maximal open filter. (shrink)

Tarski algebras, also known as implication algebras or semi-boolean algebras, are the \-subreducts of Boolean algebras. In this paper we shall introduce and study the complete and atomic Tarski algebras. We shall prove a duality between the complete and atomic Tarski algebras and the class of covering Tarski sets, i.e., structures \, where X is a non-empty set and \ is non-empty family of subsets of X such that \. This (...) duality is a generalization of the known duality between sets and complete and atomic Boolean algebras. We shall also analize the case of complete and atomic Tarski algebras endowed with a complete modal operator, and we will prove a duality for these algebras. (shrink)

In this work, we study the relational representation of the class of Tarski algebras endowed with a subordination, called subordination Tarski algebras. These structures were introduced in a previous paper as a generalisation of subordination Boolean algebras. We define the subordination Tarski spaces as topological spaces with a fixed basis endowed with a closed relation. We prove that there exist categorical dualities between categories whose objects are subordination Tarski algebras and categories whose (...) objects are subordination Tarski spaces. These results extend the known dualities for modal algebras. Finally, we are going to characterise some algebraic conditions written in the quasi-modal language by means of first-order conditions. (shrink)

We deal with monotone structural deductive systems in an unspecified propositional language \ . These systems fall into several overlapping classes, forming a hierarchy. Along with well-known classes of deductive systems such as those of implicative, Fregean and equivalential systems, we consider new classes of unital and weakly implicative systems. The latter class is auxiliary, while the former is central in our discussion. Our analysis of unital systems leads to the concept of Lindenbaum–Tarski algebra which, under some natural (...) conditions, is a free algebra in a variety closely related to the deductive system in focus. (shrink)

Logical matrices for orthomodular logic are introduced. The underlying algebraic structures are orthomodular lattices, where the conditional connective is the Sasaki arrow. An axiomatic calculusOMC is proposed for the orthomodular-valid formulas.OMC is based on two primitive connectives — the conditional, and the falsity constant. Of the five axiom schemata and two rules, only one pertains to the falsity constant. Soundness is routine. Completeness is demonstrated using standard algebraic techniques. The Lindenbaum-Tarski algebra ofOMC is constructed, and it is shown (...) to be an orthomodular lattice whose unit element is the equivalence class of theses ofOMC. (shrink)

First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and DFOL fit in this semantical framework. A soundness and completeness theorem is proved (...) for DFOL. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle. (shrink)

Two connectives are of special interest in metalogical investigations — the connective of implication which is important due to its connections to the notion of inference, and the connective of equivalence. The latter connective expresses, in the material sense, the fact that two sentences have the same logical value while in the strict sense it expresses the fact that two sentences are interderivable on the basis of a given logic. The process of identification of equivalent sentences relative to theories of (...) a logic C defines a class of abstract algebras. The members of the class are called Lindenbaum-Tarski algebras of the logic C. One may abstract from the origin of these algebras and examine them by means of purely algebraic methods. (shrink)

In the study of modal and nonclassical logics, translations have frequently been employed as a way of measuring the inferential capabilities of a logic. It is sometimes claimed that two logics are “notational variants” if they are translationally equivalent. However, we will show that this cannot be quite right, since first-order logic and propositional logic are translationally equivalent. Others have claimed that for two logics to be notational variants, they must at least be compositionally intertranslatable. The definition of compositionality these (...) accounts use, however, is too strong, as the standard translation from modal logic to first-order logic is not compositional in this sense. In light of this, we will explore a weaker version of this notion that we will call schematicity and show that there is no schematic translation either from first-order logic to propositional logic or from intuitionistic logic to classical logic. (shrink)

It is well known that there is a categorical equivalence between lattice-ordered Abelian groups (or l-groups) and conical BCK-algebras (see [COR 80]). The aim of this paper is to study this equivalence from the perspective of logic, in particular, to study the relationship between two deductive systems: conical logic Co and a logic of l-groups, Balo. In [GAL 04] the authors introduce a system Bal which models the logic of balance of opposing forces with a single distinguished truth value, (...) that represents equilibrium. Its equivalent algebraic semantics BAL (via Blok-Pigozzi's construction) is definitionally equivalent to the variety of l-groups. In this paper we define the system Balo which is equivalent to Bal and whose Lindenbaum-Tarski algebra is an l-group. On the other hand, we define the conic logic Co and we prove that it can be naturally merged in the system Balo. Also, we prove that every formula of Balo has a normal form that depends on translations of formulas of Co. (shrink)

The paper is devoted to applications of algebraic logic to databases. In databases a query is represented by a formula of first order logic. The same query can be associated with different formulas. Thus, a query is a class of equivalent formulae: equivalence here being similar to that in the transition to the Lindenbaum-Tarski algebra. An algebra of queries is identified with the corresponding algebra of logic. An algebra of replies to the queries is also associated with algebraic (...) logic. These relations lie at the core of the applications.In this paper it is shown how the theory of Halmos (polyadic) algebras (a notion introduced by Halmos as a tool in the algebraization of the first order predicate calculus) is used to create the algebraic model of a relational data base. The model allows us, in particular, to solve the problem of databases equivalence as well as develop a formal algebraic definition of a database's state description. In this paper we use the term "state description" for the logical description of the model. This description is based on the notion of filters in Halmos algebras. When speaking of a state description, we mean the description of a function which realizes the symbols of relations as real relations in the given system of data. (shrink)