# How to write the definition of a function axiomatically?

In the theory of "objects" developed in Terence Tao's Analysis I, he defines objects of type "function" on page 49 as follows:

Definition 3.3.1 (Functions). Let $X$, $Y$ be sets, and let $P(x, y)$ be a property pertaining to an object $x \in X$ and an object $y \in Y$, such that for every $x \in X$, there is exactly one $y \in Y$ for which $P(x, y)$ is true (this is sometimes known as the vertical line test). Then we define the function $f \colon X \to Y$ defined by $P$ on the domain $X$ and range $Y$ to be the object which, given any input $x \in X$, assigns an output $f(x) \in Y$, defined to be the unique object $f(x)$ for which $P(x, f(x))$ is true. Thus, for any $x \in X$ and $y \in Y$, $$y = f(x) \iff P(x, y) \text{ is true.}$$

He goes on to clarify what he means by calling a function a "unique object" when he defines equality of functions on page 51 as follows:

Definition 3.3.7 (Equality of functions). Two functions $f \colon X \to Y$, $g\colon X \to Y$ with the same domain and range are said to be equal, $f = g$, if and only if $f(x) = g(x)$ for all $x \in X$.

I think that these definitions encompass some implicit axiom schemata, the first an assertion that given certain premises about sets $X$, $Y$ and a property $P$, then a function $f$ exists, and the second that this function is unique.

The part of the above definition that says "there is exactly one $y \in Y$ for which $P(x, y)$ is true" relies on there being a definition of equality for objects of the type of $y$, in order to refer to the uniqueness of $y$ (as discussed in my previous question, he requires that the equality predicate be defined separately for each "class $T$ of objects under consideration").

I'm kind of concerned, that if functions are a type of object, and the definition of a function relies on there being a defined equality predicate for each type of object $y$, then is it a problem if $y$ is of type function (which we are just now defining the equality predicate for)? Or is it okay to simply assume that in case $y$ is of type function, we will just use the function equality predicate that is subsequently defined?

Assuming that we can do this, my attempt to write the definitions above as axiom schemata is as follows:

Let $X$, $Y$ be sets, and let $\phi$ be a formula with free variables $x$ and $y$ such that for all $x\in X$, there exists $y\in Y$ such that $\phi(x,y)$ is true, and also for any $y'\in Y$ such that $\phi(x,y')$ is true, then $y$ and $y'$ are of the same type $T$, and $y=y'$. Then there exists an object $f$, of type function, determined by $X$, $Y$, and $\phi$.

Moreover, for each function $f'$ determined by sets $X'$, $Y'$ and a formula $\phi'$ in free variables $x$ and $y$, then $f = f'$ if and only if $X = X'$, $Y = Y'$, and for all $x\in X$ and $y\in Y$, $\phi(x,y)$ is true if and only if $\phi'(x,y)$ is true.

Is the above correct? As an axiom schema, I think the second paragraph above would need to be included for every pair of formulas $\phi$ and $\phi'$ in free variables $x$ and $y$?

I don't have the text to know the details of how he's setting things up, but I imagine the idea you want isn't that "function" is a type of object: it's a family of types. That is, it's the "function from $X$ to $Y$" that are the actual types.

• Hmm, I don't know the text either, but to me the quote seems to fit into a program where there are finitely many "types" of object of which function is one. Then we can ask each function for its domain and codomain, of course -- but the main goal would probably be to deny that a function is identical to the set-of-pairs representation we're usually taught. – Henning Makholm Apr 8 '17 at 20:04
• @HenningMakholm: I agree it could go either way... but given the author is Tao I very much expect that he has type theory in the back of his mind and is taking care to say things consistent with that approach to foundations. – Hurkyl Apr 8 '17 at 20:09

I'm kind of concerned, that if functions are a type of object, and the definition of a function relies on there being a defined equality predicate for each type of object $y$, then is it a problem if $y$ is of type function (which we are just now defining the equality predicate for)? Or is it okay to simply assume that in case $y$ is of type function, we will just use the function equality predicate that is subsequently defined?

You're right -- as written the definition 3.3.7 doesn't really work as a definition, at least not in the sense the $f=g$ can be viewed as an abbreviation for the definition: we couldn't ever finish unfolding the definition because there's no limit to how many functions returning functions returning functions, etc. we may need to deal with.

The usual way out of that dilemma is to reinterpret things such that 3.3.7 is an axiom instead of a definition.

In this view, the symbol $=$ denotes a primitive concept that has no definition. The world simply comes from the beginning with a relation that we write $=$, and we then have some axioms that tells us some of how that relation behaves. In many cases the axioms will be strong enough that we can know for sure whether $a=b$ or $\neg(a=b)$ for any two given $a$ and $b$, but they don't promise to fix it completely in all corner cases.

For example, if the world is not well-founded (I don't know if Tao's system has axioms to prevent this or not) there might be some objects $\alpha$ and $\beta$ such that $\alpha$ happens to be the unique function object with domain $\{0\}$ and range $\{\beta\}$ (we can easily show that then $\alpha(0)=\beta$), and $\beta$ happens to the unique function with domain $\{0\}$ and range $\{\alpha\}$. Then it would satisfy 3.3.7 equally well to claim either that $\alpha=\beta$ or that $\alpha\ne\beta$.

The first paragraph of your attempt looks reasonable, assuming that "determined by $X$, $Y$, and $\phi$" actually means something like, "such that forall $x$ and $y$ it holds that $f(x)=y \leftrightarrow x\in X\land y\in Y\land \phi(X,Y)$".

The second paragraph is not really needed, if instead you elevate 3.3.7 to be an axiom in itself. It says that equality between any pair of function works in such-and-such way, this automatically tells us that in particular equality between functions determined by formulas work in that way too.

Note that there may be functions that are not defined by any property that we can write down. Your axiom tells us that there exist at least all the functions we can write down definitions for, but there may be more functions than that.

(In particular, if Tao gets to the Axiom of Choice at some point, it is usually phrased such that it asserts that function with certain properties exist, without specifying completely what each of their values have to be).

• Could you clarify what you mean by "$\phi(x)=y \leftrightarrow x\in X\land y\in Y\land \phi(X,Y)$"? I think you meant to write "$f(x)=y \leftrightarrow x\in X\land y\in Y\land \phi(x,y)$", but I'm still concerned about this because I'm not sure if the meaning of the expression $f(x)=y$ has really been defined--is the parentheses syntax now being defined in some way, or is it being used as an abbreviation for some other expression in the language? – justin Apr 9 '17 at 14:27
• @justin: Yes, it should have been $f(x)=y$, fixed. I'm not completely sure how Tao is setting up his system, but I think the parenthesis syntax is formally another undefined notion whose behavior is partially specified by this axiom. It would feel quite strange in this context if it were an abbreviation. – Henning Makholm Apr 9 '17 at 14:35

Definition 3.3.1 (Functions). Let $X$, $Y$ be sets, and let $P(x, y)$ be a property pertaining to an object $x \in X$ and an object $y \in Y$, such that for every $x \in X$, there is exactly one $y \in Y$ for which $P(x, y)$ is true (this is sometimes known as the vertical line test). Then we define the function $f \colon X \to Y$ defined by $P$ on the domain $X$ and range $Y$ to be the object which, given any input $x \in X$, assigns an output $f(x) \in Y$, defined to be the unique object $f(x)$ for which $P(x, f(x))$ is true. Thus, for any $x \in X$ and $y \in Y$, $$y = f(x) \iff P(x, y) \text{ is true.}$$

I'm not sure that Tao put much thought into this definition. Strictly speaking, there is no need to define a function in terms of a predicate $P$ like this. A more straightforward way to define a function would be:

Let $X$ and $Y$ be sets, and let $f\subset X\times Y.$ Then $f$ is said to be a function mapping elements of set $X$ to elements of set $Y$ if and only if

1. For all $a\in X$, there exists $b\in Y$ such that $(a,b)\in f$.
2. For all $a\in X$ and $b, c\in Y$, if $(a,b)\in f$ and $(a,c) \in f$, then $b=c$.

If $f$ is a function mapping elements of set $X$ to elements of set $Y$, then we can write $f: X \to Y$, or for all $a\in X$ we have $f(a)\in Y$ where $X$ is said to be the domain of $f$, and $Y$ the co-domain of $f$.

• Note that there is a small subtlety here: if we view $f$ as a subset of $X\times Y$, then the codomain is not unique, since we may always replace $Y$ with any larger set $Y'$! In fact the only thing we know about the codomain from looking at $f$ is that it must contain $ran(f)$. For this reason functions are often defined as triples $(f, X, Y)$ where $f\subseteq X\times Y$ is appropriate; however, in set theory we generally just drop the idea of a uniquely-defined codomain altogether. – Noah Schweber Apr 10 '17 at 20:01
• Also I think it's unfair to suggest that Tao didn't put thought into his definition. First, he may reasonably have thought that defining functions in terms of predicates is pedagogically useful (I would happen to disagree, but I don't think that's a thoughtless position). Second, that definition is very similar to and helps motivate the axiom(s) of replacement, which is famously a very difficult axiom for students to understand when first encountering set theory. – Noah Schweber Apr 10 '17 at 20:03
• @NoahSchweber Not everyone obsesses over definitions like we do. Though I haven't seen his book, I imagine Tao must have been impatient to get on to meat of the subject -- analysis, not the axioms of set theory. Reminds me a bit of golf tournament I saw some years ago on TV when a commentator was second-guessing Tigers Woods' use a of 5-iron for a very difficult shot at the Canadian Open. The commentator paused thoughtfully and said, "Then again, I'm not Tiger Woods." Woods then went on to make the most amazing shot I have ever seen! The crowd went wild as they say. – Dan Christensen Apr 10 '17 at 20:26
• Sure, but given that the question is explicitly about axioms I think this is a salient point. – Noah Schweber Apr 10 '17 at 20:55
• @NoahSchweber My point was that an axiom schema for functions is not necessary. I'm not sure why Tao thought it was necessary in the context of an introductory chapter of a textbook on analysis. It needlessly complicates a simple concept IMHO. Either way, I would be surprised if it made any difference in subsequent chapters. – Dan Christensen Apr 10 '17 at 21:54