On the universal theory of the free pseudocomplemented distributive lattice

TL;DR

This paper proves the decidability of the universal theory of free pseudocomplemented distributive lattices and provides a recursive axiomatization, contrasting with the undecidability of the full elementary theory.

Contribution

It establishes the decidability and offers a recursive axiomatization for the universal theory of free pseudocomplemented distributive lattices, and describes embeddable finitely generated lattices.

Findings

Universal theory is decidable

Recursive axiomatization provided

Characterization of embeddable finitely generated lattices

Abstract

It is shown that the universal theory of the free pseudocomplemented distributive lattice is decidable and a recursive axiomatization is presented. This contrasts with the case of the full elementary theory of the finitely generated free algebras which is known to be undecidable. As a by-product, a description of the finitely generated pseudocomplemented distributive lattices that can be embedded into the free algebra is also obtained.