Are there non-surjective functions in ZFC theory? If I understand correctly, in ZFC set theory, a function is just a set of ordered pairs with certain properties. The codomain set is just the set of all its 2nd co-ordinates (ordinates). There is no distinction made between the codomain and what is commonly called the range of a function. So, every function in ZFC set theory would be surjective. Is that correct?
 A: Surjectivity is a relationship between a function and a set. It is an extrinsic property of a function, when the function is defined as a set of ordered pairs. Not an intrinsic one like injectivity is.
So talking about whether or not "a function" (in the context of $\sf ZFC$) is surjective is kind of meaningless, in the sense that the information is missing. Normally, however, we have an implicit context for a function where we also assign it a domain and codomain, and then we can ask whether or not the range is equal to the its codomain, in which case it is indeed surjective.
For this reason, when we talk about functions we normally say things like:

*

*let $f$ be a function from $A$ onto $B$.

*The function $f\colon A\to B$ is surjective.

We are including the necessary context in this text.
A: Your question has nothing to do with ZFC set theory specifically and is just about the definition of "function" that you choose to use.  ZFC set theory does not define "function" any more than it defines "group" or "Hilbert space"; it just provides a foundational theory in which all of these notions can be defined (in various different interchangeable but not exactly identical ways) and worked with.
So, if you define a function as just a set of ordered pairs in which no two distinct elements have the same first coordinate, then yes, there is no point in talking about whether such a function is "surjective".  If you define a function to have a codomain as part of its definition itself (as in Angel's answer), then it is meaningful to ask whether a function is surjective. Or, as in Asaf's answer, you can not include a codomain in your definition of a function and instead talk about whether a function is surjective with respect to some chosen codomain.
All of these are reasonable choices and can be done within ZFC set theory or pretty much any other foundation for mathematics that you might want to use instead.  Which definition you choose has nothing to do with the specific foundational axioms you are using.  The only connection this has with ZFC is that set theorists tend to use the codomain-less definition more often than other mathematicians do, since it has some technical conveniences in the context of axiomatic set theory that it doesn't have in most other parts of math.
A: While some authors do define functions as just sets of ordered pairs, this is largely an oversimplification aimed at a beginner-level audience in mathematics. An author with more educated and sophisticated audience, though, will make the distinction between a relation and a graph, and thus a function, and a graph. Whether an author uses one definition or the other also depends on how old the text is. Older authors tend to use the simpler definition you gave, but more modern authors tend to be more careful in distinguishing functions and graphs.
Consider two sets $X$ and $Y.$ The Cartesian product is denoted $X\times{Y}.$ A subset $G$ of $X\times{Y}$ is called a graph, though in graph theory, graphs are almost always defined for when $X=Y.$ The graph $G$ is called a functional graph if and only if

*

*For every $y\in{Y},$ there exists exactly one $x\in{X}$ such that $(x,y)\in{G}.$
In older texts, $G$ is just called a function, rather than a functional graph. Under this definition of a function, it actually is meaningless to talk about surjectivity, because the domain and graph uniquely determine the codomain.
In newer texts, a function would instead be defined by $F=((X,Y),G).$ In other words, to have a well-defined function, you must have a well-defined domain, well-defined codomain, and a well-defined graph. Changing the codomain changes the function, even if the graph and codomain are the same. In this context, $Y$ is the codomain, and $F[X]\subseteq{Y},$ where $F[X]$ is the range of $F.$ Surjectivity is then defined as $F$ having the property that $F[X]=Y.$ This can be done in the language of ZFC. This can be done in any language forming a Heyting algebra. If $Y\subset{F[X]},$ then $G$ violates the functional graph axiom, so $F$ is not a function.
