Unification and projectivity in Fregean varieties

TL;DR

This paper explores the conditions under which Fregean varieties, related to logic algebraizations, guarantee the existence of projective unifiers, and characterizes those varieties with this property.

Contribution

It provides a detailed analysis of Fregean varieties, identifying identities that characterize those with projective unifiers and establishing the existence of a largest subvariety with this property.

Findings

Identifies identities characterizing congruence permutable Fregean varieties with projective unifiers.

Shows the existence of a largest subvariety with projective unifiers.

Analyzes properties ensuring the existence of projective unifiers in Fregean varieties.

Abstract

In some varieties of algebras one can reduce the question of finding most general unifiers (mgus) to the problem of the existence of unifiers that fulfill the additional condition called projectivity. In this paper we study this problem for Fregean (1-regular and orderable) varieties that arise from the algebraization of fragments of intuitionistic or intermediate logics. We investigate properties of Fregean varieties, guaranteeing either for a given unifiable term or for all unifiable terms, that projective unifiers exist. We indicate the identities which fully characterize congruence permutable Fregean varieties having projective unifiers. In particular, we show that for such a variety there exists the largest subvariety that have projective unifiers.