# 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 ?

• Why not: $\forall x \ (Ex \leftrightarrow (x \in \mathbb N \land x/2 \in \mathbb N))$ ? – Mauro ALLEGRANZA Oct 10 '17 at 6:53
• Well that would imply that $\pi$ is non-even, and the idea is to say that it should make no sense to talk about evenness or non-evenness for $\pi$. – Sephi Oct 10 '17 at 6:58
• On definitions, you can see P.Suppes, Introduction to Logic (1957), Ch 8: Thoery of Definition and page 165 for conditional definitions. – Mauro ALLEGRANZA Oct 10 '17 at 7:01
• For the continuity of a function at a point, the same problem appears. Let's try to define a binary relation $C$, with "$Cfa$" meaning "$f$ is continuous at $a$". We could suggest two axioms : $$\forall f\forall a(a\in\text{dom f}\Rightarrow(Cfa\Leftrightarrow Pfa))$$ $$\forall f\forall a(Cfa\Leftrightarrow (a\in\text{dom}\,f\wedge Pfa))$$ where "$Pfa$" is the standard $\epsilon$-$\delta$ formula defining the continuity. The second definition would imply that $\sqrt x$ is discontinuous at $-10$, which is odd. Thank you for the reference, I'm going to read it. – Sephi Oct 10 '17 at 7:05
• With conditional defs, the issue is about the "eliminability" of the defined symbol. See the "division by zero" case in the def od division; the conditional version will be like: $y \ne 0 \to (x|y=z \leftrightarrow x=yz)$. – Mauro ALLEGRANZA Oct 10 '17 at 7:10

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$.