Codomain as part of the definition of a function

TL;DR I don't think you need one to describe a function, but I think you need a codomain to define a function.

(The original iteration)

However, in set theory, the definition of function as a binary relation (i.e. a subset 𝑅 of $𝐴×𝐵$) does not include its codomain

Sure it does, you just did it: it's $B$. You can't specify ordered pairs without mentioning $B$. What does $(a,b)$ even mean if you don't know what set $b$ is from? (Edit: Of course you can build an ordered pair with two arbitrary sets. What I wanted to express, but failed to make clear, is that to use comprehension to select ordered pairs it would be necessary to mention $B$. The discussion is in the commentary to Arthur's comment below.)

It's not entirely unnatural to discern based on codomains

Also, $(𝑎,𝑏)$ does mean something if, for example, we change $𝐵$ to a larger set, and this does not affect $𝑅$.

This is part of the "is the codomain a part of the function?" question. I would say it is not so clear that it "does not affect $R$."

In Mac Lane's formulation of category theory, for example, each arrow has two associated objects of categories: the domain, and the codomain. This definition allows two technically different arrows which otherwise might be "the same function" to have different codomains, one properly containing the other.

Now look what happens when we define extensions of functions: say that we have a function $R\subseteq A\times B$ and a function $S\subseteq C\times D$ where $A\subseteq C$ and $B\subseteq D$. We say that $S$ extends $R$ if $R(a)=S(a)$ for every $a\in A$.

Of course, if $A=C$ the "bigger codomain" is just a special case of extension. From this viewpoint one can avoid confusing $R$ with its extension $S$, although for all intents and purposes we usually think of them as being the same thing "with different codomain."

While Mac Lane's formulation of category theory is largely independent of set theory, I think the mindset above is a thing in set theory too.

Regarding Arthur's comment:

A set $𝑅$ of ordered pairs where each element of 𝐴 appears exactly once as the first element of a pair" avoids the mention of anything like a codomain.

I will concede that this is a description of a function, but I would argue it does not allow one to define a function. (I'm operating under ZF only.)

Think about what it would take to try to define a function using this description. You have in hand, we suppose, the sets that will be elements of the domain and the sets that will be their images. For each assignment $a\mapsto b$, you can form $\{\{a\},\{a,b\}\}$ using the axiom of pairing, no problem.

But now you need something to pull all of these into a single set that is your set of ordered pairs. But how does one do that? I do not believe the axiom of comprehension can handle this$^\ast$. As the wiki notes, "the axiom schema of specification can only construct subsets". I think attempting to pull all the pairs into a single set would amount to using unrestricted comprehension, which is of course not safe.

A thought experiment

What I'm trying to get at is that to realize functions as sets, picking a codomain seems as necessary as specifying a domain.

How about we double-down on the logic that the codomain can be done away with completely with this thought experiment: if one believes that a function doesn't need a codomain, should we also believe that a partial function don't need a domain specified either? It's just "a set of ordered pairs, period." Is the domain not meaningful because we can extend it at will?

$^\ast$ (With a finite domain, you might be able to combine pairing, powerset and union to assemble them into a set, but of course I want to discuss infinite domains too.)

My point of view is the following.

A function is defined to be a functional relation. A relation is by definition a triple $(A,B,R)$ where $R\subseteq A\times B$, where $A$, $B$, and $R$ are (possibly empty) sets.

Under this definition when you formally give a function $(A,B,\Gamma)$, you specify its domain, its codomain, and its graph (the latter, in the case of a function, must satisfy the usual functional condition: $\forall a\in A \exists!\;b\in B: (a,b)\in \Gamma$).

This way the notion of surjectivity makes sense.

Another reason why we should prefer a definition of relation (and hence of function) to explicitly include the whole triple $(A,B,R)$ is that, this way, the collection of sets $\mathrm{Rel}(A,B)$ forms the collection of hom-sets of a category $\mathrm{Rel}$ (one axiom a general category $\mathcal C$ has to satisfy is that, for $(A,B)\neq(A',B')$, the hom-sets $\mathcal{C}(A,B):=\mathrm{Hom}_\mathcal{C}(A,B)$ and $\mathcal{C}(A',B')$ must have empty intersection).

Of course, for fixed $(A,B)$, there's a bijection between $\mathrm{Rel}(A,B)$ as I've defined it and the set of subsets of $A\times B$.

BTW, I find it quite strange that set theorists prefer the definition of relation that doesn't specify the codomain. Somehow, I think set theorists who don't use the "relations as triples" definition are just "wrong". Set theorists sometimes have to take the union of functions (which means increasing unions of graphs of extensions of a function), which for them is just literally a union of sets. I think the mild abuse of language necessary to define the "union" of functions in the "relations as triples" framework is well worth accepting.

This question is about the definition of a function. So let's define a lot of things.

Preliminary

Suppose $X$ and $Y$ are sets and $R\subset X\times Y$. Then we say $R$ is a relation between $X$ and $Y$. We also say that $X$ is a source for $R$ and $Y$ is a target for $R$. Note that any set $X'$ with $X\subset X'$ is also a source for $R$ and any set $Y'$ with $Y\subset Y'$ is also a target for $R$. So the source and target spaces are not unique when looking at $R$ on its own.

We define \begin{align*} \text{Dom}(R) =& \{x\in X:\exists y(y\in Y\land (x, y)\in R)\}\\ \text{Img}(R) =& \{y\in Y:\exists x(x\in X\land (x, y)\in R)\}. \end{align*} Clearly $\text{Dom}(R)\subset X'$ if $X'$ is any source for $R$ and $\text{Img}(R)\subset Y'$ if $Y'$ is any target for $R$.

The relation $R\subset X\times Y$ is functional if for each $x\in X$ and $y, y'\in Y$ if $(x, y), (x, y')\in R$ implies $y=y'$. If $R$ is functional and $(x, y)\in R$ then we can introduce the notation $R(x)=y$.

We are now in a position to define a function in one of two ways.

One Definition of a Function

One definition of a function is that any functional relation is a function. If $f$ is a functional relation then we denote this by \begin{align*} f: \text{Dom}(f) \to Y \end{align*} where $\text{Img}(f)\subset Y$.

Another Definition of a Function

Suppose $X$ and $Y$ are sets and $R\subset X\times Y$ is a relation between $X$ and $Y$. We can define the triple \begin{align*} R_T = (X, Y, R). \end{align*} For lack of a better name, we call $R_T$ the relation tuple, by contrast with $R$ which is the relation. In the context of the relation tuple we say $X$ is the source, $Y$ is the target, and $R$ is the relation graph. If $R$ is a functional relation then we say $R_T$ is a partial function.

Suppose $R_T = (X, Y, R)$ is a relation tuple. If $X = \text{Dom}(R)$ then we say $R_T$ is a total relation tuple.

if $f_T = (X, Y, f)$ is a total partial function then we say $f_T$ is a function and denote this by \begin{align*} f:X\to Y \end{align*}

Discussion

The most important thing I want to point out is that we sometimes hear that a function is a relation that is functional and total. But in the discussion above it is clear that we cannot even define what it means for a relation to be total by looking at the relation. We must explicitly specify a set $X$ with respect to which a relation $R$ either is or is not total.

I think this introduces the possibility for a lot of ambiguity. For example, someone might say $R\subset X\times Y$ is a total relation if $\text{Dom}(R) = X$. But it is also the case that $R\subset X'\times Y$. Is $R$ a total relation now? A rebuttal would be that this English text is implicitly assuming the definition of a 3-tuple $R_T = (X, Y, R)$ and stating that the relation tuple is total. But this is a lot of implicit action going on under-the-hood. Not to mention that to be rigorous with use of the relation/function-tuple is pretty painful in text and authors often abuse notation by treating $R$ and $R_T$ as the same thing, when they aren't.

Using the relation tuple notation it is possible for two functions with the same graph to be unequal. For example, if $X\subset X'$ then it is possible for $(X, Y, f)$ to be total but $(X', Y, f)$ is not total.

Surjectivity is the same as total. We can't tell if a bare relation $R\subset X\times Y$ is surjective. Rather, we need to explicitly indicate the set with respect to which $R$ is surjective or not. If $R_T = (X, Y, R)$ is a relation tuple then $R_T$ is surjective if $Y = \text{Img}(R)$. But all of the same ambiguities crop up again.

I like the first definition because it doesn't open the door to these ambiguities and the temptation of abusing notation by equating a function or relation with its function/relation tuple.

If you want to say a relation is total then you can say $R$ is total on $X$ to mean $X = \text{Dom}(R)$. If you want to say a relation is surjective then you can $R$ is surjective onto $Y$ to mean $Y=\text{Dom}(R)$. If you want to say a function is a bijection then you can say $f$ is a bijection between $X$ and $Y$ to mean $X=\text{Dom}(f)$ and $Y=\text{Img}(f)$.

If you rigorously use the first definition you will probably have to spend more time in English text spelling out which source and target domains matter to you. If you rigorously use the second definition you have have to spend a bit of time juggling between the function/relation tuple and the function/relation graph. I think many texts sort of ambiguously sit between the two definitions letting the relevant source and target sets be implicitly identified.