Homomorphism Preservation Theorems for Many-Valued Structures
James Carr
TL;DR
This work extends Rossman’s finite homomorphism preservation theorem to a broad class of many-valued predicate logics by developing a framework of interpreting lattices and morphisms (protomorphisms, homomorphisms, monomorphisms) and a many-valued back-and-forth theory. The authors prove two finite preservation theorems: a protomorphism-based finite h.p.t. and a fixed-algebra finite h.p.t., showing that consistency and preservation under protomorphisms (or homomorphisms in the fixed case) are equivalent to equivalence with existential-positive sentences. The analysis hinges on translating many-valued models to their classical two-element counterparts and applying Rossman’s finite extendability, supplemented by a careful treatment of integrality (residuated lattices) and the behavior of conjunctions. The results illuminate how classical model-theoretic methods can be adapted to nonclassical logics and have implications for valued constraint satisfaction problems, while also pointing to limitations and directions for non-integral algebras and semiring semantics. Overall, the paper advances finite model theory for many-valued logics and opens avenues for further exploration of preservation theorems in broader algebraic contexts.
Abstract
A canonical result in model theory is the homomorphism preservation theorem (h.p.t.) which states that a first-order formula is preserved under homomorphisms iff it is equivalent to an existential-positive formula, standardly proved via a compactness argument. Rossman (2008) established the h.p.t. remains valid when restricted to finite structures. This is a significant result, standing in contrast to the other preservation theorems proved via compactness where the failure of the latter carries forward. Almost all results from traditional model theory that do survive to the finite are those whose proofs work restricted to finite structures. Rossman's result is an example which remains true in the finite but whose proof uses different methods. It is of importance to the field of constraint satisfaction due to the equivalence of existential-positive formulas and unions of conjunctive queries. Adjacently, Dellunde and Vidal (2019) established a version of the h.p.t. holds for a collection of first-order many-valued logics, namely those whose structures (finite and infinite) are defined over a fixed finite MTL-chain. In this paper we unite these two strands. We show how one can extend Rossman's proof of a finite h.p.t. to a very wide collection of many-valued predicate logics. We establish a finite variant to Dellunde and Vidal's result, one which applies to structures defined over algebras more general than MTL-chains and where we allow for those algebra to vary between models. We identify the minimal critical features of classical logic that enable Rossman's proof from a model-theoretic point of view, and demonstrate how any non-classical logic satisfying them will inherit an appropriate finite h.p.t. Just as the classical finite h.p.t. has implications for constraint satisfaction, the many-valued finite h.p.t. has implications for valued constraint satisfaction problems.