In my recent efforts to delve into the core of mathematics, I've uncovered an anomaly. Codomains are weird and there is something missing.
The classic definition of a function
Let $A$ and $B$ be sets and $f$ a set of tuples of elements respectively in $A$ and $B$. $f:\ A \rightarrow B$ is a function if $f$ is single-valued ...
$$ (x,y_{1}) \in f \wedge (x,y_{2}) \in f \Rightarrow y_{1} = y_{2} $$
... and $f$ is total:
$$ \forall x \in A, \exists y \in B: (x, y) \in f $$
The domain of a function $f:\ A \rightarrow B$ is defined as the set ${ x \mid \exists y \in B: (x, y) \in f }$ and the range (or image) is defined as ${ y \mid \exists x \in a: (x, y) \in f }$.
$B$ is called the codomain of $f$.
Preliminary notes
Note firstly that $A$ and $B$ are included in the definition of a function $f:\ A \rightarrow B$. This also means that the equality of two functions is defined as conjunction of equalities between the respective $A$'s, $B$'s and $f$'s.
Note also that the domain of a function $f:\ A \rightarrow B$ is equal to $A$ while the range of that function is not equal to $B$.
Lastly, because $B$ is not equal to the range of the function, $B$ can be an arbitrary superset of the range. There is no connection whatsoever between $B$ and the set of tuples $f$.
This codomain $B$ is only used to define things like surjectivity or in theorems like, for example, the isomorphism theorems.
Problems with this definition
That was a lot of theory that any mathematician should have known by heart for years.
Ugly
The first problem with this definition is that it's ugly. The sets $A$ and $B$ are baked into the definition of a function while $f$ could just be a single-valued set of tuples! The domain and range definitions would stay the same because they are inherent to $f$ and can be defined irrespective of $A$ and $B$.
No partial functions
The second problem is that it doesn't allow for non-total functions.
Most mathematicians often have the luxury to only have to think about total functions. Ironically, people like information theorists and computer scientists often use the more abstract notion of partial functions.
To remind you, partial functions are functions where there isn't necessarily an output defined for every input. I would say $A$ is not equal to $dom(f)$ if the above definition hadn't disallowed that!
In the above definition of functions, there is no way to define non-total functions and that limits our thinking. Powerful mathematical concepts like Turing-machines can't be defined unless we allow for the more abstract notion of partial functions.
Asymmetric
Now, suppose you really want to define a codomain each time, then there is a third problem. The definition is now asymmetric:
$$ f:\ dom(f) \rightarrow img(f) \subseteq B $$
I hope it's obvious that there is something missing here. Much nicer would be the following:
$$ f:\ dom(f) \subseteq A \rightarrow img(f) \subseteq B $$
We can't do this, however, because the above definition of a function dictates that $A$ must equal $dom(f)$.
A new definition
Now clear your mind and have a look at this new and improved definition:
Let $A$ and $B$ be sets and $f$ a set of tuples of elements respectively in $A$ and $B$. $f:\ A \rightarrow B$ is a function if $f$ is single-valued:
$$ (x,y_{1}) \in f \wedge (x,y_{2}) \in f \Rightarrow y_{1} = y_{2} $$
The domain of a function $f:\ A \rightarrow B$ is defined as the set ${ x \mid \exists y \in B: (x, y) \in f }$ and the range (or image) is defined as ${ y \mid \exists x \in A: (x, y) \in f }$.
$A$ is called the corange of $f$ and $B$ is called the codomain of $f$.
Note that we can't call $A$ the coimage because that name is taken.
Advantages
This new definition solves all the problems of the last definition:
$f$ could (possibly) be defined independent of a corange and codomain, though that would still require another definition of equality. This definition is not as ugly as the last one.
Because the corange $A$ is now different from the domain of $f$: $dom(f) \subseteq A$, $f$ is no longer necessarily total. This means that a function can now be partial and still be a function. This is precisely the case when $dom(f)$ is a strict subset of $A$.
The definition of a function is now symmetric:
$$ f:\ dom(f) \subseteq A \rightarrow img(f) \subseteq B $$
... and as an added bonus, this new way of defining functions requires you to acknowledge the existence of partial functions.
Feedback
While suggesting this idea to mathematicians, I have often been figuratively pelted by vegetables. However, they've never been able to tell me why it was that they couldn't be open to other definitions. After all, there is no such thing as a true definition.
I hope that, if there are any other mathematicians that feel deeply and personally offended by this, they will be able to explain to me what is mathematically (!) wrong with this new definition. As of yet, I have not been able to find any flaws.