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 is introduced by modifying an intuitionistic resolution system Rip, which is originally introduced by Mints and modified by Troelstra and Schwichtenberg. The equivalence between Rnp and G4np can be shown. Thirdly, a typed λ-calculus for N4 is introduced based on Prawitz’s natural deduction system for N4 via the Curry-Howard correspondence. The strong normalization theorem of this calculus can be proved by using Joachimski and Matthes’ proof method for intuitionistic typed λ-calculi with premutative conversions.

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 the theory of Fujiwara to the, not necessarily similar, many-sorted algebras, by defining the concept of polyderivor between many-sorted signatures under which are subsumed the standard signature morphisms, the derivors of Goguen-Thatcher-Wagner, and the basic mapping-formulas of Fujiwara.

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 defined in the paper.

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 the induced anti-order θ on A/(α ∪ α−1) is a half-space too, is the main result of this paper.

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 idem-potent 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 semiconic if it decomposes subdirectly (in IP) into algebras where the iden- tity element t is order-comparable with all other elements. The semiconic algebras in IP are locally finite. It is proved here that a relative subvariety of IP consists of semiconic algebras if and only if it satisfies x ≈ (x → t) → x. It follows that if an axiomatic ∗ extension of RMO has ((p → t) → p) → p among its theorems then it is locally tabular. In particular, such an extension is strongly decidable, provided that it is finitely axiomatized.

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 the proof of standard completeness for the variety of √′ quasi-MV algebras; we show that this same variety has the finite embeddability property; finally, we investigate the structure of the lattice of subvarieties of √′quasi-MV algebras.

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. Journal of Symbolic Logic, 66, No4 (2001), 1620-1636). Classical examples of new implicit frontal operators are the functions, (op. cit., Example 3.1), the successor (op. cit., Example 5.2), and Gabbay’s operation (op. cit., Example 5.3).
We study a Priestley duality for the category of frontal Heyting algebras and in particular for the varieties of Heyting algebras with each one of the implicit operations given as examples. The topological approach of the compatibility of operators seems to be important in the research of affin completeness of Heyting algebras with additional compatible operations. This problem have also a logical point of view. In fact, we look for some complete propositional intuitionistic calculus enriched with implicit 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 suc- cessor and certain Priestley spaces. Let X be the Heyting space associated by this duality to the Heyting algebra with successor H.

If there is an ordinal κ and a filtration on X such that X =LJλ≤κ X_λ, the height of X is the minimun ordinal ξ ≤ κ such that   filtration allows us to write the space X as a disjoint union of antichains. We may think that these antichains define levels on this space.

We study the way of characterize subalgebras and homomorphic images in finite Heyting algebras with successor by means of their Priestley spaces. We also depict the spaces associated to the free algebras in various subcategories of SLH_ω.