What exactly is a function? [duplicate]

I think an answer to this question would have to go into philosophical questions on mathematical foundations. Currently, as far as I know, most mathematics education would present foundations based on ZFC. The basic idea here is that every object of consideration is considered to be a set, and then for any two objects $x$ and $y$ it is valid to ask whether $x \in y$, and to ask whether $x = y$. This has the advantage of reducing things to a very small number of primitives, while still being powerful enough to eventually be able to represent almost all the useful mathematical concepts such as real or complex numbers, and yes, functions. (Though category theory does start to run into some theoretical issues when trying to express that in terms of ZFC...)

The disadvantage, though, is that this representation is "artificial" and doesn't really reflect the way that most mathematicians actually think about things on a daily basis. For instance, the most common "representation" of natural numbers in ZFC is: $0 = \{ \}$, $1 = \{ 0 \} = \{ \{ \} \}$, $2 = \{ 0, 1 \} = \{ \{ \}, \{ \{ \} \} \}$, and so on. This is hardly a natural representation: we tend to think of natural numbers not as sets that you can compare by $\in$ but rather as "atomic" objects that we can compare for example using $<$. Likewise, suppose for example that in an abstract algebra course you start off by saying "let $G$ and $H$ be two groups". Then you do think of $G$ and $H$ as being sets of elements; however, you usually don't think of elements $g \in G$ or $h \in H$ as sets themselves, nor do you usually think it would make sense to ask whether $g = h$ for $g \in G$ and $h \in H$ (or even if it is theoretically valid, it would almost always be considered an irrelevant thing to ask).

Going on to the subject of functions: at a primitive level, we tend to think of functions $f : X \to Y$ not as an abstract set of pairs, but as some notion of a way of taking an element $x \in X$ as input and producing some corresponding element $y \in Y$ as output. Then, from that, we can indeed consider the graph of $f$ as a subset of $X \times Y$; but we tend to think of this as being both more complex than the base "algorithm to transform input into output", and as being less useful in most cases.

So, some work has been done under the heading of "type theory" to try to come up with foundations for mathematics that are more natural and more closely reflect the mode of thinking of day-to-day mathematics, as compared to ZFC. The general idea of this philosophy for coming up with a foundational system is: we work with types that are considered to be incomparable; e.g. if $X$ and $Y$ are two different types, then in general it doesn't make sense to try to ask about $X \cap Y$ or about $X \cup Y$ (though many type theories do allow forming a disjoint union $X \sqcup Y$). Moreover, the elements of a general type are considered to be "atomic" objects which are not considered to have any further internal structure. Also, functions are generally required to just be one of the irreducible notions which cannot be defined (just as the notion of "set" and the relation $\in$ cannot be defined in ZFC). All we can do is to provide ways to take existing functions and build up more complex functions from them.

As an illustrative example of what such a type theory might look like, "simply typed lambda calculus" might be a good place to start. Here, the fundamental notion is of a "typing judgment" and of relations between them. For example, one valid "typing derivation" might be:

$$ X ~ type, Y ~ type, Z ~ type, f : X \to Y, g : Y \to Z \vdash (\lambda (x : X) . g(f(x))) : X \to Z. $$

This says that if $X,Y,Z$ are variables representing types, and $f$ is a function from $X$ to $Y$ and $g$ is a function from $Y$ to $Z$, then the term $\lambda (x : X) . g(f(x))$ forms a function from $X$ to $Z$, representing the composition $g \circ f$. This would be proved formally from rules such as:

\begin{align*} \Gamma & \vdash \phi : X \to Y \\ \Gamma & \vdash \psi : X \\ \hline \Gamma & \vdash \phi(\psi) : Y. \end{align*}

This says that if you have a context $\Gamma$ (a list of things like $X~type$ or $term : X$), along with two terms $\phi$ and $\psi$, and in the context $\Gamma$ you can prove that $\phi$ is of type $X \to Y$ and $\psi$ is of type $Y$, then you can form a function application term and in the context $\Gamma$ you have that $\phi(\psi)$ is of type $Y$.

Then, there are also type theories that extend this with assertions such as $\tau~proposition$, $\tau~true$, and add a formal proof system to work with these. Note that in keeping with the philosophy, it is much more common to use a natural deduction style of formal proof system in such an extended type theory as opposed to a Hilbert-style system. (Though a common alternative is to invoke the Curry-Howard correspondence which essentially says that type derivations, along with constructions such as product types and disjoint union types, are already enough to express the relevant first-order logic. If this is used, then in these formal systems, a proposition just becomes a special case of a type.)

So, these type theories do tend to map mathematical arguments more naturally into formal language. However, they do have some disadvantages as compared to ZFC. For one thing, they have significantly more primitive notions that have to be described in the metatheory, making a metamathematical study of the properties of a type theory possibly more difficult. Also, we do tend to think of relations such as $\mathbb{N} \subseteq \mathbb{Z} \subseteq \mathbb{Q} \subseteq \mathbb{R} \subseteq \mathbb{C}$, whereas type theory tends to have difficulties in expressing such "canonical inclusion" relations.

To return to the original question, I'm not that familiar with Tao's Analysis text. But from the quote, it does appear that the author is subscribing more to the point of view of type theory that functions should be considered a primitive notion, and graphs of functions should be considered something you derive from the primitive - as opposed to the view of ZFC that a function is precisely a set satisfying certain properties.

I like and suggest the following definition:

A function $f:A\to B$ is a triple

1. a first set $A$ (domain)

2. a second set $B$ (codomain)

3. a law (i.e. a rule, a relationship, etc.) such that at each element of $A$ is associated one and only one element of $B$ that is

$$\forall x\in A \quad \exists ! y\in B:\,y=f(x)$$

Tao defines a function from $X$ to $Y$ to be a property $P(x,y)$ of elements $x \in X$ and $y \in Y$ such that for each $x$ there is exactly one $y$ making the property true.

Of course, this definition of a function as being a "property" without further clarification does not meet the standards of precision and rigour one would find in a construction of mathematics on the basis of set theory. Tao presumably feels that such a construction is inappropriate at the level of his book. Obviously, since a "property" is not a set, Tao is correct in saying that, according to his definition of a function, it is not a set.

With respect to the question of whether the domain of definition is all of $X$ or not, I will make the following observations.

The distinction between a function (fonction) and a mapping (application) that you refer to does indeed exist in France (or once existed), but only at school level, not in higher mathematics in general. The reason is that one wants to be able to refer to a function such as $f(x) = 1/(x-1)$ as being a function from $\mathbf{R}$ to $\mathbf{R}$, even though it is a mapping from $\mathbf{R} - \{1\}$ to $\mathbf{R}$. This distinction does not exist in English-speaking countries, as far as I am aware, and I don't know about other languages.

Even in France, other than in specific contexts, this distinction is not usually made by mathematicians. If one speaks of a function from $X$ to $Y$, one is saying that the domain of definition is all of $X$. One exception, to which Suzet alludes in a comment, is the theory of recursive functions, where one wants to be able to speak of a "partial function" from $\mathbf{N}$ to $\mathbf{N}$.

When the concept of a function is formalized set-theoretically, the most common approach is to define a mapping $f$ from $X$ to $Y$ as being synonymous with its graph, which is the set you define in (2).

This definition has much to be said for it, but it also has what some consider a serious deficiency. A graph $\Gamma$ could represent a function $f$ from a set $X$ to a set $Y$, but the same graph could also represent a function from $X$ to any other set $Y'$ containing $f(X)$. There are areas of mathematics, particularly those where category theory is often used, where this is inconvenient, and one would like to consider two mappings $f \colon X \to Y$ and $f' \colon X \to Y'$ with the same graph $\Gamma$ to be distinct objects. Consequently, Bourbaki defines the mappings $f$ and $f'$ to be the distinct triples $(\Gamma, X, Y)$ and $(\Gamma, X, Y')$, respectively. In this convention it has been followed by many authors, particularly in France where its influence has been greatest.