Definition of function notation

[Manchot]

I've been going through Mendelson's mathematical logic book, and I'm having difficulty reconciling the definition of new function letters with the notion of function notation (as it applies to sets in ZFC). I realize what I just said is a mouthful, so let me try and elaborate. Mendelson defines the function letter f(y1...yn) in the following way:

Suppose that (\exists_{1}u)\beta(u,y_1,...,y_n). Then the function letter f(y_1,...,y_n) is defined by adding the axiom \beta(f(y_1,...,y_n),y_1,...y_n) to the theory. He then proves that the new theory produces the same theorems as the old one (essentially adding nothing to it).

This "definition of definition" seems fine for most circumstances, but it seems to me that it fails whenever the uniqueness is conditioned upon some condition. For example, in ZFC, one can say that "g is a function from A to B" iff x\in A \rightarrow (\exists_{1}y)(y\in B \wedge (x,y)\in g). In this case, uniqueness is contingent upon x \in A, so how would one define g(x)?

 

[CRGreathouse]

I don't really follow. Uniqueness shouldn't be a problem, since

\exists_1 x \mathcal{S}(x)
for some wff \mathcal{S} is surely just
\exists x\mathcal{S}(x) \wedge \forall y \mathcal{S}(y)\rightarrow x=y
right?

 

[Manchot]

Okay, I managed to find a way to get around the issue. Actually, the problem wasn't existence, it was uniqueness. For values of x outside of A, the statement x\in A \rightarrow (y \in B \wedge (x,y)\in g) is vacuously true, meaning that all choices of y satsify the condition. To fix the problem, I proved that if x\in A \rightarrow (\exists_{1}y)(y\in B \wedge (x,y)\in g), then (\exists_{1}y)((x\in A \rightarrow (y \in B \wedge (x,y)\in g)) \wedge (x\notin A \rightarrow y=\emptyset)). I was then able to define function notation with the latter statement. Of course, for values of x not in A, I had to arbitrarily set f(x) to be the null set, but this is acceptable to me.

 

[Hurkyl]

This is somewhat less awkward when you use typed languages, so that the domain of your functions symbols is part of the language.

 

[Manchot]

This is somewhat less awkward when you use typed languages, so that the domain of your functions symbols is part of the language.

I don't know, now that I've thought about it some more, it's kind of useful to have notation defined regardless of the context. I mean, with this notation I could even write down $\mathbb{N}$ (3) and have it be meaningful. Since $\mathbb{N}$ isn't a function, it would just evaluate to the empty set. On the other hand, I could conceive of some situations where the choice of the empty set as could cause some problems, if one is not careful about specifying what the domain of some variable is (e.g., asking whether there is a set whose successor is the empty set).