Is there a theory of extensible definitions?

Question

We can define $+$ as a function $\mathbb{N}^2 \rightarrow \mathbb{N}$, and then prove:

Theorem 1. The range of $+$ is $\mathbb{N}$.

If we later wish to extend $+$ to a function $\mathbb{Z}^2 \rightarrow \mathbb{Z}$, then we have a problem; according to our new definition, the theorem we proved isn't true any more. To be rigorous, we must therefore define a new operation $ +' : \mathbb{Z}^2 \rightarrow \mathbb{Z}$. But this is clumsy. In practice, what we usually do is refrain from talking about $+$ in certain ways, and this allows us to extend the definition. So for instance, the following sentence is fine:

Theorem 2. For all $a,b \in \mathbb{N}$ it holds that $a \leq a+b$.

By writing sentences like Theorem 2 only, and refraining from sentences like Theorem 1, we're able to extend $+$ without invalidating our previous theorems, as opposed without having to introduce a new operation $+'$.

So what I'm looking for is a rigorous approach to the idea that, by pairing a definition with some additional information about how that definition is allowed to be used, it becomes extensible. And the more stringent we are about how a definition can be used, the more extensible it becomes.

Is there a theory of extensible definitions?

P.S. I don't know which tags are appropriate for this question. Please feel free to retag it.

Answer 1

I don't think there's any formal distinction between your (i) and (ii) that would have told you, knowing only about addition in $\mathbb N$, that one is going to keep holding for the extendion and the other isn't.

It would have been simple enough instead to define an extension of $+_{\mathbb N}$ to $\mathbb Z$ which instead preserves the validity of (ii) but doesn't preserve (i). For example, we could have defined $a+_{\mathbb Z}b=|a|+_{\mathbb N}|b|$ and the resulting $+_{\mathbb Z}$ would still have been a strict extension of $+_{\mathbb N}$, satisfying (ii) but not (i).

So it's not really that some statements are inherently extensible, but merely that in choosing which extensions to consider we implicitly choose which properties are going to continue holding. Conversely, our desire to keep some properties valid will inform our choice of which extensions we allow to keep the same name and symbol.

Of course, when we originally defined + we could have paired it with an explicit list of properties that we intend all our extensions of it to keep satisfying. But that's not a very satisfactory solution in a larger setting, because in general we'll want to be able to consider many different kinds of extensions, some that will preserve many properties and others that will leave most of them behind.

For example, most extensions of $+$ preserve the property $a+b=b+a$, and in most cases one would certainly want to consider that "extensible" if the word is to have any useful meaning. However, $a+b=b+a$ is not true about the usual extension of $+$ to addition of transfinite ordinals.

Answer 2

Perhaps what you're looking for is model theory. Model theory is a branch of logic which deals with structures defined in particular languages (which just consist of some symbols and rules of syntax). As an example, let's suppose your language $\cal{L}$ consists of the constant symbol "$0$", a two-place function symbol "+", and a binary predicate "$\leq$". Then on the structure $\mathcal{N} = \langle \mathbb{N},0^\mathbb{N},+^\mathbb{N},\leq^\mathbb{N} \rangle$, where "$s^\mathbb{N}$" denotes the standard interpretation of these symbols on $\mathbb{N}$, your (i) and (ii) hold in this structure, i.e. $\mathcal{N} \vDash \forall x\forall y(x \leq x + y)$ and $\text{ran}(+^\mathbb{N}) = \mathbb{N}$. Now define another structure $\mathcal{Z} = \langle \mathbb{Z},0^\mathbb{Z},+^\mathbb{Z},\leq^\mathbb{Z} \rangle$ in a similar way. In this case, it's not longer the case that $\mathcal{Z} \vDash \forall x\forall y(x \leq x + y)$, but what we have is $\mathcal{Z} \vDash \forall x,y \geq 0(x \leq x + y)$ (where "$\geq$" is an appropriate abbreviation), so (i) is still good. As for (ii), we then just note that, on these structures, $+^\mathbb{Z} \mid \mathcal{N} = +^\mathbb{N}$, where "$\mid$" is now denotes restriction to a substructure. So the range of $+^\mathbb{Z} \mid \mathcal{N}$ is $\mathbb{N}$, as before, even though the range of full $+^\mathbb{Z}$ is not $\mathbb{N}$.

In addition to being a good tool for talking about all these sorts of things, model theory does have a number of results regarding "definability" in a model, i.e. when a model can define certain objects/properties and when it can't, and also what things follow from such definable objects/properties. There are also a number of "preservation" results, stating when certain sentences (usually of a certain syntactic form) remain true in extensions/substructures of the original structure you're looking at. So for instance, $\mathcal{Z}$ doesn't satisfy the sentence $\forall x \forall y (x \leq x + y)$ (since $y$ could be negative); model theory let's you prove something more general, viz. $\forall_1$ sentences (which have the syntactic form of a string of $\forall$s followed by an atomic formula) aren't necessarily preserved in extensions of structures, though they're preserved in substructures. For a nice introduction to the material, see Hodges's A Shorter Model Theory or Marker's Model Theory: An Introduction (note, though, these assume you're already familiar with the basics of mathematical logic).