Testing definitional equivalence of theories via automorphism groups
H. Andréka, J. Madarász, I. Németi, G. Székely
TL;DR
The paper provides a semantic, ultraproduct-based criterion for definitional equivalence of first-order theories: two theories are definitionally equivalent if and only if there is a bijection between their model classes that preserves universes, isomorphisms, and ultraproducts, formalized by $b(\prod_U\mathfrak{M}_i)=\prod_U b(\mathfrak{M}_i)$ for every ultrafilter $U$. It demonstrates that matching automorphism-group spectra is necessary but not sufficient for definitional equivalence, via explicit counterexamples, and then develops a complete framework using concrete ultracategories and ultraproduct-preserving functors to certify equivalence or inequivalence. The results connect to and settle conjectures by Barrett, Glymour, and Halvorson, and illuminate how ultraproducts, universes, and isomorphisms govern the recoverability of a theory from its model class. The work thereby clarifies the relationship between language-based and structural notions of theory equivalence and provides a robust method for distinguishing definitional equivalence in practice.
Abstract
Two first-order logic theories are definitionally equivalent if and only if there is a bijection between their model classes that preserves isomorphisms and ultraproducts (Theorem 2). This is a variant of a prior theorem of van Benthem and Pearce. In Example 2, uncountably many pairs of definitionally inequivalent theories are given such that their model categories are concretely isomorphic via bijections that preserve ultraproducts in the model categories up to isomorphism. Based on these results, we settle several conjectures of Barrett, Glymour and Halvorson.