Creative Commons Attribution 4.0 International license
The Homomorphism Preservation Theorem (HPT) of classical model theory states that a first-order sentence is preserved under homomorphisms if, and only if, it is equivalent to an existential-positive sentence. This theorem remains valid when restricted to finite structures, as demonstrated by the author in [Rossman, 2008; Rossman, 2017] via distinct model-theoretic and circuit-complexity based proofs. In this paper, we present a third (and significantly simpler) proof of the finitary HPT based on a generalized Cai-Fürer-Immerman construction. This method establishes a tight correspondence between syntactic parameters of a homomorphism-preserved sentence (quantifier rank, variable width, alternation height) and structural parameters of its minimal models (tree-width, tree-depth, decomposition height). Consequently, we prove a conjectured "equi-rank" version of the finitary HPT. In contrast, previous versions of the finitary HPT possess additional properties, but incur blow-ups in the quantifier rank of the equivalent existential-positive sentence.
@InProceedings{rossman:LIPIcs.CSL.2025.6,
author = {Rossman, Benjamin},
title = {{Equi-Rank Homomorphism Preservation Theorem on Finite Structures}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {6:1--6:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-362-1},
ISSN = {1868-8969},
year = {2025},
volume = {326},
editor = {Endrullis, J\"{o}rg and Schmitz, Sylvain},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.6},
URN = {urn:nbn:de:0030-drops-227634},
doi = {10.4230/LIPIcs.CSL.2025.6},
annote = {Keywords: finite model theory, preservation theorems, quantifier rank}
}