Model-Theoretic Conservative Extension for 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 hi her-orderlogic that allows ad hoc overloading of constants. In 2015, Kun6ar and Popescu introduced de nitional theories, which impose a non-circularity condition on constant and type definitions in this logic, an 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.