I am reading Patrick Suppes' "Axiomatic Set Theory".
It defines "Conditional definitions of operations" as follows:
An implication P is introducing a new operation symbol O is a conditional definition if and only if P is of the form
Q $\Rightarrow$ [O($v_1$,....,$v_n$) = w $\Leftrightarrow$ R]
and the following restrictions are satisfied
(i) the variable w is not free Q,
(ii) the variables $v_1$,....,$v_n$ ,w are distinct variables
(iii)R has no free variables other than $v_1$,....,$v_n$ ,w
(iv) the only non-logical constants are primitive or previously defined symbols of set thoery, and
(v) the formula Q $\Rightarrow$ (E!w)R is derivable from the axioms and preceding definitions.$^1$
Can you please explain this more intuitively. I'm having trouble grasping concepts like: does this definition follow from the Identity and Equivalence rules of definitions of operations? Does this rule comply to the criteria of non-creativity and eliminability? Can this definition also applying to definitions of objects other than operations?
Here is a link to google books, the definition is on page 18.
$^1 $Suppes, P. (1972). Axiomatic Set Theory. Dover Publications
The concept of "conditional" definition of an operation symbol is a generalization of the concept of definition of operation symbol. (In Suppes terminology, "operation" symbol is what people more usually call a function symbol.)
As Suppes says, there are two ways of defining function symbols. Definition by identity is the more mathematically familiar approach: a function symbol is defined from other function symbols. For example, $x^2 = x\times x$.
However, in formal mathematical theories, it's sometimes convenient to take only relation symbols as primitives. (A case in point is axiomatic set theory, taking as primitive only the symbol $\in$.) Nonetheless, developing mathematics within the formal theory practically requires the use of function symbols. So it would be nice to be able to define function symbols in terms of relations symbols.
Hence the second kind of definition of operation symbol, definition by equivalence. Very informally, to define a function $f$ by equivalence is to say "the $f$ of $x$ is the $y$ such that blah($x,y$)". Clearly, this presupposes a substantial condition on the relation specified by "blah": it must hold that for each $x$, there is a unique $y$ such that blah($x,y$), i.e., that the relation is "functional".
However, that presupposition isn't always fulfilled. For example, consider the square root function on the natural numbers. Here you would like to say "the square root of $x$ is the $y$ such that $y\times y=x$". But such $y$ doesn't always exist. This leads to a logical problem: since $\sqrt{x}=\sqrt{x}$ is logically provable, it could be derived from the "definition" that for all $x$ there is a $y$ such that $y\times y=x$, and so provable, e.g., that the square root of two is a whole number.
One response is simply to revise the definition, putting instead "it's either the $y$ such that $y\times y=x$ or failing that, the $y$ such that $y=0$". But that's a pain. So we're led to the idea of conditional definition of operation.
A conditional definition directly extends the method of definition by equivalence to situations when the defining relation isn't functional. That is, we say instead "if there's a unique $y$ such that $y\times y=x$, then $\sqrt{x}$ is that $y$." This takes care of the logical problem mentioned above.
According to Suppes, a definition of a symbol needs to satisfy some formal criteria of "conservativeness and eliminability". Do conditional definitions satisfy these criteria?
On the one hand, it's clear that a conditional definition of a function symbol yields a conservative extension of a theory. To see this, note that everything provable from
"if there's a unique $y$ such that blah($x,y$), then $f(x)$ is that $y$"
is provable from
"$f(x)$ is the unique $y$ such that either there's a unique $z$ such that blah($x,z$) and $y=z$, or there isn't and $y=0$".
Since adding the latter always yields a conservative extension, so does the former.
However, it's not true that conditional definitions satisfy eliminability. To see this, note that a conditional definition leaves open the meaning of the formula for those arguments which don't satisfy its condition. For example, to the conditional definition of the square root function symbol in formal number theory, we could consistently add an axiom "the square root of two is zero" or an axiom "the square root of two is one", or etc.; but the square root function symbol is eliminable only if there is at most one such consistent extension.
So, conditional definitions don't satisfy eliminability. Still, it's clear that each can be trivially extended to one that does. So it's not so bad even by Suppes' standards to call them definitions.
As you suggest, one can consider conditional definitions of relation symbols as well. One motivation would be for relations whose application is naturally restricted to some subset of the domain. For example, (so far as I know) "$x$ is congruent to $y$ mod $z$" is only reasonable for $z$ a positive integer. As before, such "definitions" will yield conservative extensions, and be trivially extensible to satisfy eliminability.