# (When) are recursive "definitions" definitions?

This is a "soft" question, but I'm greatly interested in canvassing opinions on it. I don't know whether there is anything like a consensus on the answer. Under what conditions (if any) are recursive definitions of arithmetical functions truly definitions worthy of the name?

By "recursive definition" I mean a pair of axioms taking the following form:

1. $$\forall y_1 \cdots\forall y_n f(0, y_1, ..., y_n) = \varphi(y_1, ..., y_n)$$
2. $$\forall x \forall y_1 \cdots\forall y_n f(s(x), y_1, ..., y_n) = \psi(y_1, ..., y_n, f(x, y_1, ..., y_n), x)$$

where $$f$$ is the $$(n+1)$$-place function symbol being "defined", and $$\varphi$$ and $$\psi$$ are $$n$$-place and $$(n+2)$$-place function symbols (respectively) already expressible in the original language. Let $$L$$ be the original language (I'm assuming some arithmetical language, certainly containing '0' and 's'), and let $$L^+ = L\cup\{f\}$$ be the new language. Let $$T$$ be the theory in the language $$L$$ for which $$f$$ is being introduced. Finally, let $$R$$ be the set of these two axioms.

I think there is a spectrum of possible views here, so let me lay out what I think is a sensible taxonomy. I may well be wrong about this being a sensible taxonomy, in which case I'd be interested to know about that too.

Presumably, the strictest view is that $$R$$ never constitutes a definition of $$f$$, since any definition worth the name must always take the form

$$(\delta) \quad \forall z \forall x \forall y_1 \cdots\forall y_n(f(x, y_1, \ldots, y_n) = z \leftrightarrow \chi(x, y_1, \ldots, y_n, z))$$

for some $$(n+2)$$-place $$L$$-formula $$\chi$$. Presumably we also need some guarantee that for every $$x, y_1, \ldots, y_n$$, $$z$$ is unique in satisfying $$\chi$$, call this sentence (when suitably formalised in $$L$$) $$\gamma$$. Then according to the strictest view, any definition of $$f$$ must take the form of $$\delta$$, and we must have $$T\vdash\gamma$$.

But I'm interested in the possibility that the strictest view is too strict. One might ask: What is it about $$\delta$$ that makes it worthy of being a definition? It strikes me that there are four desiderata one might demand. In the following, let $$\Delta$$ be the set of sentences that "do the defining":

1. Proof-theoretic conservativeness: For any $$L$$-sentence $$\sigma$$, $$T\cup\Delta\vdash \sigma$$ only if $$T\vdash\sigma$$.
2. Model-theoretic conservativeness: Every $$L$$-model of $$T$$ has some expansion that is an $$L^+$$-model of $$T\cup\Delta$$.
3. Proof-theoretic eliminability: There is some $$(n+2)$$-place $$L$$-formula $$\chi$$ such that $$T\cup\Delta\vdash \delta$$ (and presumably we also demand $$T\vdash\gamma$$?).
4. Model-theoretic eliminability: Any two distinct $$L^+$$-models of $$T\cup\Delta$$ have distinct $$L$$-reducts (and again, presumably we also demand $$T\vdash\gamma$$?).

Correct me if I'm wrong, but if the logic here is first-order, then Beth's definability theorem entails that 3 and 4 are equivalent conditions. So there are really only 3 conditions in total here. Also 2 implies 1 (but not vice versa).

Now, setting $$\Delta = \{\delta\}$$ obviously satisfies 2 and 3. But if $$\Delta = R$$, would satisfying 2 and 3 be sufficient for $$\Delta$$ to count as a definition, rather than "just" extra axioms?

What about dropping 3 (and 4) altogether? Perhaps it is acceptable for $$f$$ to be only "partially" defined. Or perhaps a middle position is better: we demand model-theoretic eliminability only for the standard model of the natural numbers (so that the standard $$L$$-model has a unique $$L^+$$-expansion)? Any recursive definition would surely(?) satisfy this. (Incidentially, it strikes me as strange that 3 is often called "explicit definability" and 4 is often called "implicit definability", when it is rather 1 or 2 that capture the idea of a definition being harmless/saying nothing new.)

What about weakening 2 to 1? I believe (though I haven't proved it to myself) that $$R$$ will always satisfy 1. Is that right?

It can be proved (I think) that 2 may fail for recursive definitions. (Rough idea: let $$L$$ be $$(0, s, +)$$, let $$T$$ be Presburger arithmetic for this language, PrA, and let $$R$$ be the usual recursive definition of multiplication, so that $$f = \times$$ and $$T\cup R$$ is Peano arithmetic PA. There are recursive non-standard models of PrA, but by Tennenbaum's theorem no non-standard models of PA in which + is recursive. Thus there are models of PrA with no expansion into a model of PA.) It therefore strikes me that 2 is a good desideratum, because it is non-trivial, and accords with (what I take to be) consensus that the recursive "definition" of multiplication in PA is not really a definition. Besides, it just smells right.

I'm very interested to know people's thoughts. Many thanks in advance.

• I would never accept 1 or 2 as being sufficient to call something a definition. For example, adding a new function symbol and saying nothing about it satisfies 1 and 2. The new function symbol has in no way been defined! Commented Jul 19 at 17:23
• Also, I don't understand your linguistic point about "being harmless / saying nothing new". What is the connection supposed to be between harmlessness and implicit or explicit definability? To me, "$f$ is definable" means "we can specify exactly what function $f$ is". This is a far cry from "assuming there is function $f$ satisfying such and such conditions does not have any new provable consequences for our theory". Commented Jul 19 at 17:27
• @AlexKruckman the connection is simply that definitions ought to be something like true in virtue of meaning alone, and so uninformative. If I define vixens as female foxes, I thereby make no commitment about foxes, female or otherwise (at least that’s the idea). Commented Jul 19 at 18:24
• From what you say it seems like conservativeness of either kind is, for you, not a necessary condition. Is that right? Commented Jul 19 at 18:25
• Conservativity is necessary but not sufficient. The reason recursive definitions are valid over base theories $T$ like PA or ZF is that $T$ proves the recursion theorem, which tells us how to transform a recursive definition into an explicit one. It seems like you're interested in weak base theories like PrA which don't prove the recursion theorem. I would call the recursive axiomatization of $\times$ relative to PrA just an axiomatization, not a definition. Of course, it is a definition (in that it uniquely defines a function!) if we restrict our attention to the standard model. Commented Jul 19 at 20:00

This answer elaborates on my comments above. My impression from your question is that you are interested in definitions in the technical sense of mathematical logic (rather than the informal notion of definition used in mathematical writing), so my answer will be about this perspective. You probably know most if not all of the things I write here, but I erred on the side of giving more detail, to make sure everything is clear.

Let $$\newcommand{\K}{\mathcal{K}}\K$$ be a class of $$L$$-structures. Usually, we are interested in the case when $$\K = \{M\}$$, a single structure, or when $$\K= \DeclareMathOperator{\Mod}{Mod}\Mod(T)$$, the class of all models of a first-order $$L$$-theory $$T$$. But my remarks will apply just as well to arbitrary $$\K$$. The notation $$\K\models \varphi$$ means that every structure in $$\K$$ satisfies $$\varphi$$. Note that in the case $$\K = \Mod(T)$$, $$\K\models \varphi \iff T\vdash \varphi$$ by the completeness theorem.

For logicians, there is an unambiguous meaning of "definable function" relative to $$\K$$, which is what you call the "strictest view".

A definable ($$n$$-ary) function is an $$L$$-formula $$\varphi(\overline{x},y)$$ (where $$\overline{x}$$ is an $$n$$-tuple of variables) such that: $$\K\models \forall \overline{x}\exists y\,(\varphi(\overline{x},y)\land \forall z\,(\varphi(\overline{x},z)\rightarrow y = z)).$$ Let's call that previous sentence $$\DeclareMathOperator{\Fun}{Fun}\Fun(\varphi)$$, since it asserts that $$\varphi$$ defines a function.

Let $$L' = L\cup \{f\}$$, where $$f$$ is a new $$n$$-ary function symbol. Following your notation, let $$\delta_{f,\varphi}$$ be the sentence $$\forall \overline{x}\forall y\, (f(\overline{x}) = y \leftrightarrow \varphi(\overline{x},y))$$. If $$\K\models \Fun(\varphi)$$, then every structure $$M\in \K$$ admits a unique expansion to an $$L'$$-structure $$M'$$ satisfying $$\delta_{f,\varphi}$$ (by defining $$f^{M'}(\overline{a})$$ to be the unique $$b$$ such that $$M'\models \varphi(\overline{a},b)$$).

Now there's a natural way to generalize the above: Suppose $$\Delta$$ is an $$L'$$-theory such that every structure $$M\in \K$$ admits a unique expansion to an $$L'$$-structure $$M'$$ satisfying $$\Delta$$. Then we say that the new function symbol $$f$$ is implicitly defined by $$\Delta$$. In the case that $$\Delta = \{\delta_\varphi\}$$ as in the previous paragraph, we say that $$f$$ is explicitly defined by $$\varphi$$.

Implicit and explicit definitions are the only things I would be willing to call "definitions". In fact, because "definition" is a technical term in logic with a precise meaning, I would only ever use it for the "strict" sense of explicit definition. But I do agree that an implicit definition provides a satisfactory definition of $$f$$, exactly because every structure in $$\K$$ can be expanded to a model of $$\Delta$$ in a unique way: $$\Delta$$ completely specifies the behavior of $$f$$. I would just be careful to always call such a definition an implicit definition.

If $$\K = \Mod(T)$$, then it follows from Beth's definability theorem that any implicitly definable $$f$$ is in fact explicitly definable. That is, if $$f$$ is implicitly defined by $$\Delta$$, then $$T\cup \Delta\vdash \delta_{f,\varphi}$$ for some $$L$$-formula $$\varphi$$.

It also follows from the completeness theorem that $$T\cup \Delta$$ is a conservative extension of $$T$$. So in the case of a first-order theory, there is no difference between implicit and explicit definitions, and these notions satisfy all four of your desiderata.

To my mind, conservativity is an attractive byproduct of definability, but it has nothing to do with the core concept of definability. For example, as I pointed out in the comments, if we take $$\Delta = \varnothing$$, then the $$L'$$-theory $$T\cup \Delta$$ is conservative over $$T$$. But I don't think anyone would claim that $$\Delta$$ therefore serves as a definition of the new function symbol $$f$$!

Now what about recursive definitions? Taking again $$L' = L\cup \{f\}$$, a "recursive definition" of $$f$$ an $$L'$$-theory $$\Delta$$ of a certain form. Let's call such a $$\Delta$$ a "recursive specification", since it may not actually serve as a definition of $$f$$. That is, it may not be the case that every structure in $$\K$$ admits a unique expansion to a model of $$\Delta$$.

For example, let $$L = \{0,S,+\}$$, and let $$\Delta$$ contain: \begin{align*} &\forall x\, (x\times 0 = 0)\\ &\forall x\forall y\, (x\times S(y) = (x\times y)+x) \end{align*} If $$\K = \{(\mathbb{N};0,S,+)\}$$, then $$\Delta$$ is an implicit definition of $$\times$$ relative to $$\mathbb{N}$$. In fact, by the set-theoretic version of the recursion theorem, any recursive specification over $$\mathbb{N}$$ (in any language, as long as it has standard $$0$$ and $$S$$) is an implicit definition.

But if $$\K = \Mod(\mathrm{PrA})$$, then $$\Delta$$ fails to be an implicit definition of $$\times$$, because $$\mathrm{PrA}$$ has nonstandard models for which the existence/uniqueness of $$\times$$ fails.

In many arithmetic theories (like $$\mathsf{PA}$$, but not $$\mathsf{PrA}$$), the recursion theorem (which is really a theorem schema, with one instance for each recursive definition) implies that recursive specifications actually are implicit definitions. Even better, the proof constructively transforms a recursive specification into an explicit definition.

So: When are recursive "definitions" definitions?

• They are as good as explicit definitions when we have the recursion theorem.
• They are satisfactory definitions exactly when they are implicit definitions, i.e., when they are satisfied by a unique function over every structure of interest. For example, whenever $$\K=\{\mathbb{N}\}$$.
• +1. To the OP, re: the limited scope of Beth definability see here. Commented Jul 20 at 23:25
• Comprehensively answered. Thank you! Commented Jul 21 at 0:11