- #1
Manchot
- 473
- 4
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 [itex](\exists_{1}u)\beta(u,y_1,...,y_n)[/itex]. Then the function letter [itex]f(y_1,...,y_n)[/itex] is defined by adding the axiom [itex]\beta(f(y_1,...,y_n),y_1,...y_n)[/itex] 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 [itex]x\in A \rightarrow (\exists_{1}y)(y\in B \wedge (x,y)\in g).[/itex] In this case, uniqueness is contingent upon [itex]x \in A[/itex], so how would one define g(x)?
Suppose that [itex](\exists_{1}u)\beta(u,y_1,...,y_n)[/itex]. Then the function letter [itex]f(y_1,...,y_n)[/itex] is defined by adding the axiom [itex]\beta(f(y_1,...,y_n),y_1,...y_n)[/itex] 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 [itex]x\in A \rightarrow (\exists_{1}y)(y\in B \wedge (x,y)\in g).[/itex] In this case, uniqueness is contingent upon [itex]x \in A[/itex], so how would one define g(x)?