How to formalize a "conditional" definition? In Kenneth Kunen's book The Foundations of Mathematics, there is a definition of a mathematical definition : it is an conservative extension $\mathcal L'$ of a language $\mathcal L$ of a theory $T$. More precisely, to define a new $n$-ary relation $\phi$ in $T$ is to add "$\phi$" to $\mathcal L$ and add an axiom of the form :
$$\forall x_1,\ldots,\forall x_n (\phi(x_1,\ldots,x_n)\Leftrightarrow R(x_1,\ldots,x_n))$$
where $R$ is a $n$-ary relation already included in the base language $\mathcal L$. So far so good.
But what about what I could call a "conditional" definition ? By that expression I mean a property that is only defined over a subset of the universe. For example, in a theory of real numbers, I could define the predicate "$n$ is even" only when $n$ is a natural number. I would proceed in this manner :

(Let's recall that we work with the real numbers.)
Definition. Let $n$ be a natural number. We say that $n$ in even if and only if $n/2$ is a natural number.

A consequence is that the number $\pi$ is not even nor non-even, it makes no sense to talk about the evenness of non-natural numbers. Mathematics are full of that kind of definitions (I think of "$f$ is continuous at $a$" where $a$ is not any number but member of the domain of $f$).

My question is :
How to formalize that kind of "conditional" definition ?

I would try this. Add a predicate symbol $E$ to the base language ("$Ex"$ would mean "$x$ is even") and the following axiom :
$$\forall x(x\in\mathbb N\Rightarrow (Ex\Leftrightarrow x/2\in\mathbb N))$$
But this doesn't correspond to Kunen's definition of a mathematical definition.
So is it a good way to formalize a "conditional" definition ? In particular, is that process a conservative extension of the base theory ?
 A: Yes, your idea is a good principle of conservative extension and you don't need to introduce any notion of "undefined" or "nonsense" terms to justify it: let $T$ be a theory and let $\chi$ and $\rho$ be sentences over the language of $T$ extended with one or more new symbols. If $T \cup \{\chi\}$ is conservative over $T$ and if $T \cup \{\chi\} \vdash \rho$, then $T \cup \{\rho\}$ is conservative over $T$. (Because $T \cup \{\rho\}$ cannot prove anything that $T \cup \{\chi\}$ cannot.)
In your example, if $T$ is the theory of real arithmetic extended with a predicate "$(\cdot) \in \Bbb{N}$" for membership of the natural numbers and if $\chi \equiv \forall x(E(x)\Leftrightarrow x/2\in\mathbb N)\,$ (a sentence in the language of $T$ extended with a new one-place predicate symbol $E(\cdot)$), then $T \cup \{\chi\}$ is conservative over $T$ (using the principle from Kunen's book). But then, if $\rho \equiv \forall x(x\in\mathbb N\Rightarrow (E(x)\Leftrightarrow x/2\in\mathbb {N}),\;$ we have $T \cup \{\chi\} \vdash \rho$, so $T \cup \{\rho\}$ is also conservative over $T$.
