Model-theoretic Conservative Extension of Definitional Theories

Many logical frameworks allow extensions, i.e. the introduction of new symbols, by definitions. Different from asserting arbitrary non-logical axioms, extensions by definitions are expected to be conservative: they should entail no new theorems in the original language. The popular theorem prover Isabelle implements a variant of higher-order logic that allows ad hoc overloading of constants. In 2015, Kunčar and Popescu introduced definitional theories, which impose a non-circularity condition on constant and type definitions in this logic, and showed that this condition is sufficient for definitional extensions to preserve consistency. We strengthen and generalize this result by showing that extensions of definitional theories are model-theoretic conservative, i.e. every model of the original theory can be expanded to a model of the extended theory