A frontal operator in a Heyting algebra is an expansive operator preserving finite meets which also satisfies the equation (x) ≤ y ∨ (y → x). A frontal Heyting algebra is a pair (H, ), where H is a Heyting algebra and a frontal operator on H. Frontal operators are always compatible, but not necessarily new or implicit in the sense of Caicedo and Cignoli (An algebraic approach to intuitionistic connectives...

Contrary to the variety of Heyting algebras, finite Heyting algebras with successor only generate a proper subvariety of that of all Heyting algebras with successor. In particular, all finite chains generate a proper subvariety, SLH!, of the latter. There is a categorical duality between Heyting algebras with successor and certain Priestley spaces. Let X be the Heyting space associated by this duality...

The aims of the present paper are to introduction and investigate of notions of complementary pairs of quasi-antiorders and half-space quasi-antiorder on a given set. For a pair α and β of quasi-antiorders on a given set A we say that they are complementary pair if α ∪ β =6=A and α ∩ β = ∅. In that case, α (and β ) is called half-space on A. Assertion, if α is a half-space quasi-antiorder on A, then...

Given a LE-structure E, where LE is an infinitary language, we show that and can be chosen in such way that every orbit of the group G of automorphisms of E is LE -definable. It follows that two sequences of elements of the domain D of E satisfy the same set of L-formulas if and only if they are in the same orbit of G.

Anderson and Belnap’s implicational system RMO can be extended conservatively by the usual axioms for fusion and for the Ackermann truth constant t. The resulting system RMO is algebraized by the quasivariety IP of all idempotent commutative residuated po-monoids. Thus, the axiomatic extensions of RMO are in one-to-one correspondence with the relative subvarieties of IP. An algebra in IP is called...

In the first part of this paper (RML No. 42) a spectrum of constructive logics without the K axiom is defined. Negation is introduced with a propositional falsity constant. The aim of this second part is to build up logics definitionally equivalent to those displayed in the first part, negation being now introduced as a primitive unary connective. Relational ternary semantics is provided for all logics...

In the present paper, which is a sequel to [14] and [3], we investigate further the structure theory of quasi-MV algebras and √′quasi-MV algebras. In particular: we provide an improved version of the subdirect representation theorem for both varieties; we characterise the Ursini ideals of quasi-MV algebras; we establish a restricted version of J´onsson’s lemma, again for both varieties; we simplify...

This paper is devoted to investigation of the lattice properties of p-consequences. Our main goal is to compare the algebraic features of the lattices composed of all p-consequences and all consequence operations defined on the same propositional language.

For, not necessarily similar, single-sorted algebras Fujiwara defined, through the concept of family of basic mappingformulas between single-sorted signatures, a notion of morphism which generalizes the ordinary notion of homomorphism between algebras. Subsequently he also defined an equivalence relation, the relation of conjugation, on the families of basic mapping-formulas. In this article we extend...

Firstly, a contraction-free sequent system G4np for Nelson’s paraconsistent 4-valued logic N4 is introduced by modifying and extending a contraction-free system G4ip for intuitionistic propositional logic. The structural rule elimination theorem for G4np can be shown by combining Dyckhoff and Negri’s result for G4ip and an existing embedding result for N4. Secondly, a resolution system Rnp for N4...

In [4, Definition 8.1], some important subvarieties of the variety SH of semi-Heyting algebras are defined. The purpose of this paper is to introduce and investigate the subvariety ISSH of SH, characterized by the identity(0 - 1)* v (0 - 1)** = 11. We prove that ISSH contains all the subvarieties introduced by Sankappanavar and it is in fact the least subvariety of SH with this property. We also determine...

Interpretability logic is a modal description of the interpretability predicate. The modal system IL is an extension of the provability logic GL (Gödel–Löb). Bisimulation quotients and largest bisimulations have been well studied for Kripke models. We examine interpretability logic and consider how these results extend to Veltman models

This paper presents a complete classification of the complexity of the SAT and equivalence problems for two-element algebras. Cases of terms and polynomials are considered. We show that for any fixed two-element algebra the considered SAT problems are either in P or NP-complete and the equivalence problems are either in P or coNP-complete. We show that the complexity of the considered problems, parametrized...

It is known that classical logic CL is the single maximal consistent logic over intuitionistic logic Int, which is moreover the single one even over the substructural logic FLew. On the other hand, if we consider maximal consistent logics over a weaker logic, there may be uncountablymany of them. Since the subvariety lattice of a given variety V of residuated lattices is dually isomorphic to the lattice...

The notion of “sequences” is fundamental to practical reasoning in computer science, because it can appropriately represent “data (information) sequences”, “program (execution) sequences”, “action sequences”, “time sequences”, “trees”, “orders” etc. The aim of this paper is thus to provide a basic logic for reasoning with sequences. A propositional modal logic LS of sequences is introduced as a Gentzen-type...

Formulas for computing the number of Df2-algebra structures that can be defined over Bn, where Bn is the Boolean algebra with n atoms, as well as the fine spectrum of Df2 are obtained. Properties of the lattice of all subvarieties of Df2, (Df 2), are exhibited. In particular, the poset Sifin(Df2) is described.

We describe properties of simply axiomatized modal logics, which are called pseudo-Euclidean modal logics. We will then give a complete description of the inclusion relationship among these logics by showing inclusion relationships for pairs of their logics with fixed m and n.

This paper studies some properties of the so-called semilattice-based logics (which are defined in a standard way using only the order relation from a variety of algebras that have a semilattice reduct with maximum) under the assumption that its companion assertional logic (defined from the same variety of algebras using the top element as representing truth) is algebraizable. This describes a very...

The methods of categorical abstract algebraic logic are employed to show that the classical process of the coordinatization of abstract (affine plane) geometry can be viewed under the light of the algebraization of logical systems. This link offers, on the one hand, a new perspective to the coordinatization of geometry and, on the other, enriches abstract algebraic logic by bringing under its wings...

The paper deals with functional properties of three-valued logics. We consider the family of regular three-valued Kleene’s logics (strong, weak, intermediate) and it’s extensions by adding an implicative connectives (“natural” implications). The main result of our paper is the lattice that describes the relations between implicative extensions of regular logics.