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 ?

  • $\begingroup$ Why not: $\forall x \ (Ex \leftrightarrow (x \in \mathbb N \land x/2 \in \mathbb N))$ ? $\endgroup$ – Mauro ALLEGRANZA Oct 10 '17 at 6:53
  • $\begingroup$ 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$. $\endgroup$ – Sephi Oct 10 '17 at 6:58
  • $\begingroup$ On definitions, you can see P.Suppes, Introduction to Logic (1957), Ch 8: Thoery of Definition and page 165 for conditional definitions. $\endgroup$ – Mauro ALLEGRANZA Oct 10 '17 at 7:01
  • $\begingroup$ 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. $\endgroup$ – Sephi Oct 10 '17 at 7:05
  • $\begingroup$ 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)$. $\endgroup$ – 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$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.