Suppose $L$ is a language of first order logic, $T$ is a theory of $L$. Suppose $L'$ is a language obtained by adding one new predicate symbol $R$ to $L$. Suppose $\varphi(x_1, \dots, x_n)$ is a well-formed formula in $L$. Consider the theory $T'$ obtained by adding to $T$ the statement $\forall x_1 \dots \forall x_n\ R(x_1, \dots, x_n) \leftrightarrow \varphi(x_1, \dots, x_n)$ . Then, according to https://en.wikipedia.org/wiki/Extension_by_definitions, $T'$ is a conservative extension of $T$, and for any statement $\psi$ in $L'$, $T'$ proves that $\psi$ is equivalent to the version of $\psi$ where all occurences of the symbol $R$ are expanded as $\varphi$. There is a similar theorem for functional symbols as well.
Notice that we've required that $\varphi$ doesn't contain the symbol $R$. This forbids recursive definitions. For example, consider the following three extensions of first order theories:
- This one is an extension of Peano axioms in the language of arithmetic with one new symbol. $\forall n\ \operatorname{Even}(n) \leftrightarrow n=0\ \lor \exists m\ \operatorname{Even}(m) \land n=m+2$
- This one is an extension of ZF in the language of set theory with one new symbol. $c(\emptyset) = 0\ \land \forall x \ c(\{x\})=c(x)+1$.
- This one is also an extension of ZF in the language of set theory with one new symbol. $\forall n \in \mathbb{N}\ \operatorname{Even}(n) \leftrightarrow n=0 \ \lor \exists m \in \mathbb{N}\ \operatorname{Even}(m) \land n=m+2$
I suspect that all three of these are conservative extensions even though they are not extensions by definition. But still, in some sense, they extend by definition. And I suspect that they can be rewritten to actually become extensions by definition.
So, my questions are:
- If we allow $\varphi$ to be a well-formed formula in $L'$ rather than only in $L$, under what reasonable additional assumptions will this be a conservative extension? When will there exist an equivalent extension by definition (i.e. an equivalent non-recursive axiom)?
- Can we somehow modify extension by definitions to allow recursive definitions?
- If questions 1 and 2 can't be nicely answered for arbitrary theories, please answer them for superlanguages of set theory with theories including the ZF axioms and superlanguages of the language of arithmetic with theories including the Peano axioms.