The fork and its role in unification of closure algebras

TL;DR

This paper investigates the structure of a specific algebraic variety generated by a dual closure algebra, providing insights into its finite projective algebras and demonstrating that unification within this variety is finitary but not unitary.

Contribution

It offers a detailed description of finite projective algebras in the variety and provides a semantic proof regarding the nature of unification in this context.

Findings

Finite projective algebras characterized

Unification in the variety is finitary

Unification is not unitary

Abstract

We consider the two-pronged fork frame $F$ and the variety $\mathbf{Eq}(B_F)$ generated by its dual closure algebra $B_F$. We describe the finite projective algebras in $\mathbf{Eq}(B_F)$ and give a purely semantic proof that unification in $\mathbf{Eq}(B_F)$ is finitary and not unitary.