Finite axiomatizability of logics of distributive lattices with negation

TL;DR

This paper investigates the finite axiomatizability of logics derived from distributive lattices with negation, providing both negative and positive results, and introduces constructive methods for translating between algebraic and logical presentations.

Contribution

It establishes syntactic conditions for non-finite axiomatizability and shows that certain subvarieties have finitely axiomatizable logics, with constructive translation methods.

Findings

Logic of all distributive lattices with negation is not finitely axiomatizable.

Subvarieties of semi-De Morgan algebras are finitely axiomatizable if their algebraic varieties are.

Constructive methods enable effective translation between algebraic presentations and Hilbert calculi.

Abstract

This paper focuses on order-preserving logics defined from varieties of distributive lattices with negation, and in particular on the problem of whether these can be axiomatized by means of finite Hilbert calculi. On the side of negative results, we provide a syntactic condition on the equational presentation of a variety that entails failure of finite axiomatizability for the corresponding logic. An application of this result is that the logic of all distributive lattices with negation is not finitely axiomatizable; likewise, we establish that the order-preserving logic of the variety of all Ockham algebras is also not finitely axiomatizable. On the positive side, we show that an arbitrary subvariety of semi-De Morgan algebras is axiomatized by a finite number of equations if and only if the corresponding order-preserving logic is axiomatized by a finite Hilbert calculus. This equivalence also holds for every subvariety of a Berman variety of Ockham algebras. We obtain, as a corollary, a new proof that the implication-free fragment of intuitionistic logic is finitely axiomatizable, as well as a new Hilbert calculus for it. Our proofs are constructive in that they allow us to effectively convert an equational presentation of a variety of algebras into a Hilbert calculus for the corresponding order-preserving logic, and vice versa. We also consider the assertional logics associated to the above-mentioned varieties, showing in particular that the assertional logics of finitely axiomatizable subvarieties of semi-De Morgan algebras are finitely axiomatizable as well.