Generalization of terms via universal algebra

TL;DR

This paper introduces a universal-algebraic framework for understanding term generalization in equational theories, linking algebraic structures with logical systems and analyzing their properties.

Contribution

It develops a new algebraic approach to study generalization problems, reducing complexity in certain varieties and applying results to various algebraic and logical systems.

Findings

Generalization poset can be studied via congruence lattices of free algebras.

Identifies varieties where the generality poset reduces to congruence lattice analysis.

Shows MV-algebras have nullary type, impacting the understanding of Lukasiewicz logic.

Abstract

We provide a new foundational approach to the generalization of terms up to equational theories. We interpret generalization problems in a universal-algebraic setting making a key use of projective and exact algebras in the variety associated to the considered equational theory. We prove that the generality poset of a problem and its type (i.e., the cardinality of a complete set of least general solutions) can be studied in this algebraic setting. Moreover, we identify a class of varieties where the study of the generality poset can be fully reduced to the study of the congruence lattice of the 1-generated free algebra. We apply our results to varieties of algebras and to (algebraizable) logics. In particular we obtain several examples of unitary type: abelian groups; commutative monoids and commutative semigroups; all varieties whose 1-generated free algebra is trivial, e.g., lattices, semilattices, varieties without constants whose operations are idempotent; Boolean algebras, Kleene algebras, and G\"odel algebras, which are the equivalent algebraic semantics of, respectively, classical, 3-valued Kleene, and G\"odel-Dummett logic. Finally, we prove that the variety of MV-algebras, the equivalent algebraic semantics of Lukasiewicz logic, has nullary type.