One of the points that Tim Gowers makes in this blog post, is that the set theoretic definition of functions achieves nothing, that it is possible to treat functions as fundamentally different objects from sets. However, I think this might raise an issue on the existence of functions.
Consider an example in group theory. Suppose we want to prove that for each set $T$, $\text{Sym}(T)$, the set of all bijections on $T$ forms a group under function composition. We know that the composition of two bijections is a bijection, function composition is associative, we can take the identity element to be the identity function on $T$, and the inverse function of a function is bijective. Let's examine the identity axiom more closely:
The identity axiom requires the existence of an identity element. We need to somehow prove that for every set $T$, there exists a function $f: T \to T$, such that for each $t \in T$, $f(t) = t$. If we treat functions as sets, we can do this. If $T$ is a set, it can be shown that $T \times T$ exists, and is the unique set which consists of all ordered pairs of elements of $T$. Then, by the axiom of specification, the set $$ f = \{ (a,b) \in T \times T \ | \ a = b \}$$ also exists. Once the existence of the identity function is established, it can be shown that it satisfies the remaining requirements of the identity axiom.
However, if we treat functions as fundamentally different from sets, it seems that we need to be careful when specifying axioms surrounding them. Statements such as:
- A function is a rule which associates each element of one set with exactly one element of another
- If $f: A \to B$, then for each $a \in A$, $f(a) \in B$
do not seem sufficient to show that any function exists in the first place, so we would be left unable to prove that symmetric groups are actually groups!
At the end of his post, Gowers proposes the following way of defining functions:
Here in detail is what I would say. Let $G$ (to stand for “graph”) be a subset of $A \times B$ such that for every $x \in A$, there is exactly one $y \in B$ with $(x,y) \in G$. Then we can define a function $f: A \to B$ in terms of $G$ by letting $f(x)$ be the unique $y$ such that $(x,y) \in G$. Moreover, every function from $A$ to $B$ can be obtained this way, since $f$ is a function we can define $G$ to be the set of all $(x,y)$ such that $y = f(x)$.
Is this sufficient to solve the problem of asserting the existence of an identity function on each set? What if $A$ is empty? Then there is no unique $y$ such that $(x,y) \in G$. Going backward seems fine, since if there is no $(x,y)$ such that $y = f(x)$, then the resulting $G$ would be empty. Am I missing something here?
In summary, my questions are:
- Is the argument that for each set $T$, an identity function on $T$ exists, valid? That is, under the framework of defining functions as sets.
- Is the method of defining functions that Tim Gowers proposes sufficient to deal with the problem of the existence of identity functions?
From the tone of the question, it sounds like you want a proof that will work even in mathematical foundations which treat functions as being fundamentally distinct objects from sets. This is a typical feature of the family of mathematical foundations known as type theory.
What a type theory usually provides is a way to construct compound types and functions from basic principles. A common set of such constructions can be described as simply typed lambda calculus, in which functions are defined using a vaguely Lisp-like syntax but with type annotations -- for example, $\lambda (f : X \multimap Y) . \lambda (g : Y \multimap Z) . \lambda (x : X) . g(f(x))$. Here, $X \multimap Y$ denotes the type of functions from $X$ to $Y$, and for example $\lambda (x:X) . g(f(x))$ represents the function with domain $X$ which takes $x \mapsto g(f(x))$. Then, we have a set of "type checking" rules which are similar to formal proof rules, in which you want to prove so-called typing inferences of a form like $$X \mathrm{~type}, Y \mathrm{~type}, Z \mathrm{~type}, f : X \multimap Y, g : Y \multimap Z \vdash [\lambda(x : X) . g(f(x))] : X \multimap Z.$$
Typical rules for verifying typing inferences include things like assumption:
\begin{align*} \phi & \in \Gamma \\ \hline \Gamma & \vdash \phi \end{align*}
map types:
\begin{align*} \Gamma & \vdash \tau \mathrm{~type} \\ \Gamma & \vdash \upsilon \mathrm{~type} \\ \hline \Gamma & \vdash (\tau \multimap \upsilon) \mathrm{~type} \end{align*} function application:
\begin{align*} \Gamma & \vdash \tau \mathrm{~type} \\ \Gamma & \vdash \upsilon \mathrm{~type} \\ \Gamma & \vdash \phi : \tau \multimap \upsilon \\ \Gamma & \vdash \psi : \tau \\ \hline \Gamma & \vdash \phi(\psi) : \upsilon \end{align*}
and abstraction:
\begin{align*} \Gamma & \vdash \tau \mathrm{~type} \\ \Gamma & \vdash \upsilon \mathrm{~type} \\ \Gamma, x : \tau & \vdash \phi : \upsilon \\ \hline \Gamma & \vdash (\lambda (x : \tau) . \phi) : \tau \multimap \upsilon. \end{align*}
(Here in the last one, we require that $x$ does not appear in any formula in the context $\Gamma$.) Here, $\tau$ and $\upsilon$ represent formulas representing a type; $\phi, \psi$ represent formulas representing a (possibly complex) value expression; and $x$ represents an atomic variable symbol. The statements above the line in each rule represent the hypotheses of the typing inference rule, and the statement below represents the conclusion.
In this context, it is easy to prove $X \mathrm{~type} \vdash (\lambda (x : X) . x) : X \multimap X$. First, by assumption, we have $X \mathrm{~type}, x : X \vdash x : X$; therefore, by the abstraction rule (and a couple more assumptions repeating that $X \mathrm{~type}$, we get $X \mathrm{~type} \vdash (\lambda (x : X) . x) : X \multimap X$. This has the interpretation that whenever $X$ is a type, then $\lambda (x : X) . x$ is a function from $X$ to $X$.
In fact, many type theories will also provide a fundamental way to construct an element $\operatorname{except}_X : \emptyset \multimap X$ whenever $X$ is any type. If you interpret simply typed lambda calculus as a bare-bones programming language, then a possible interpretation of $\operatorname{except}_X$ is as a function which can never be called; so the internal implementation could be some formalization of "if this function is ever called, something must have gone seriously wrong with the runtime since there should be no possible way to provide me with an element of the empty type $\emptyset$ as the input argument; therefore, I will signal an exception and exit, so the function will never return to its caller and therefore the return type of this function doesn't matter".
As it happens, simply typed lambda calculus also has a straightforward interpretation in ZFC: you ignore hypotheses of the form $X \mathrm{~type}$ (since all the objects you work with are sets anyway); you interpret $X \multimap Y$ as usual as $\{ f \in P(X \times Y) \mid \forall x\in X, \exists! y\in Y, (x, y) \in f \}$; you interpret $\phi : \tau$ as the proposition $\phi \in \tau$; you can interpret $\operatorname{except}_X$ as $\emptyset \in (\emptyset \multimap X)$; and so on. Then all the typing inference rules listed above lead to valid implications in ZFC. In particular, the validity of the typing inference $X \mathrm{~type} \vdash (\lambda (x : X) . x) : X \multimap X$ implies that $\forall X, \{ (x, x) \mid x \in X \} \in (X \multimap X)$ is a theorem of ZFC.