Constructive reflectivity principles for regular theories

TL;DR

This paper explores constructive methods for completing structures to models of regular theories, revealing that certain reflectivity principles depend on choice axioms, yet still enabling completeness results.

Contribution

It demonstrates that classical reflectivity principles are equivalent to choice in constructive set theory and introduces a new approach to model completion without assuming decidable equality.

Findings

Constructive chase construction is unproblematic but not weakly reflective.

Reflectivity principles are equivalent to choice principles in set theory.

Embedding into chase-completion remains conservative, supporting completeness of regular logic.

Abstract

Classically, any structure for a signature $\Sigma$ may be completed to a model of a desired regular theory $T$ by means of the chase construction or small object argument. Moreover, this exhibits $\mathrm{Mod}(T)$ as weakly reflective in $\mathrm{Str}(\Sigma)$. We investigate this in the constructive setting. The basic construction is unproblematic; however, it is no longer a weak reflection. Indeed, we show that various reflectivity principles for models of regular theories are equivalent to choice principles in the ambient set theory. However, the embedding of a structure into its chase-completion still satisfies a conservativity property, which suffices for applications such as the completeness of regular logic with respect to Tarski (i.e. set) models. Unlike most constructive developments of predicate logic, we do not assume that equality between symbols in the signature is decidable. While in this setting, we also give a version of one classical lemma which is trivial over discrete signatures but more interesting here: the abstraction of constants in a proof to variables