How can one quantify on a function in ZFC?

I have read that $ZFC$ and first-order logic could formalize all the mathematics, but I do not manage to conceive that. First, let me show what my understanding of $ZFC$ is.
I have read that $ZFC$ was a L-theory where L is the language formed with no functions, no constants and two relations $=$ and $\in$.
One can add functions symbols to make $ZFC$ richer, for example, if $ZFC \vdash \forall x \forall y \exists ! z,F(x,y,z)$, one can create the $ZFC+$, a L+-theory, where L+ is L to which we add a function symbol f with arity 2, and where $ZFC+$ is $ZFC$ to which we add the formulas $\forall x \forall y F(x,y,f(x,y))$. It is easy to prove that for all F L-formula which are closed, we have $$ZFC\vdash F$$ if and only if we have $$ZFC+ \vdash F$$ And I think that for all L+-formula F, there is a L-formula F' such that $ZFC+ \bigcup \left\{F\right\}$ and $ZFC+ \bigcup \left\{F'\right\}$ are equivalent; or something like that, so we can work in everyday mathematics as if it were in ZFC, although we use symbols such as $\cos$, $\sin$, $\emptyset$, $\left\{a,b\right\}$ and so on.
We can thus introduce our language $ZFC+$, but how can we consider such an easy sentence as $$(\star) \forall f \in \mathbb{C}^{\mathbb{N}}, \forall n \in \mathbb{N}, f(n) \in \mathbb{C}$$ Because, although we have introduced our function symbols for each $f$ (for example, taking the formulas $\forall x \exists ! y,(x\in \mathbb{N} \wedge (x,y) \in f) \vee (x\notin \mathbb{N} \wedge y=\emptyset )$ ), we do not have a first-order sentence, or so I think.
$\textbf{EDIT}$ : It is because f here is a symbol of a function. For example, a first-order sentence, as I understand them, would be : $\forall f \in \mathbb{C}^{\mathbb{N}}, (f=f) \wedge (f \in f)$, because here f is the symbol of a variable. Is it possible to formalize sentence $(\star)$ using a first-order sentence ? Am I missing something ?

-
It seems to me that you are very unclear on where first-order ends, and where higher-order logic begins. It also seems that you are unclear on how set theory plays a role in "reducing" high-order sentence to a first-order sentence (in a different language, though). – Asaf Karagila Oct 1 '13 at 23:07
I do not know what higher-order sentences are. I just know what first-order sentences are. And I cannot see how $(\star)$ is a first-order sentence. $(\star\star) \forall f \in \mathbb{C}^{\mathbb{N}}, \forall n \in \mathbb{N}, F[f,n]$ is a first-order sentence (or formula) if F[f,n] is a first-order formula with free variables in {f,n}, but, precisely, $f(n) \in \mathbb{C}$ is a first order formula, but n is the only free variable. f is a function symbol, and we cannot quantify over a function symbol (at least in the first-order logic I was taught). – Florian Oct 1 '13 at 23:35
The point is that saying buzzwords like first order logic without understanding what it means is a wasted effort. What is the language? What do the symbols $\Bbb{C,N}$ mean? Why do you think that cannot be written in first order logic? Do you even understand all the terms and definitions in your question? It seems to me that the answer is no. – Asaf Karagila Oct 1 '13 at 23:40
I say first order logic because it is what is written in the book I read. The language is the language of ZFC to which I added symbols to the point that I have $\mathbb{R}$ as a constant symbol and $(.)^2$ as a 1-ary function symbol (I also add axioms to ZFC as shown in the question). Furthermore $\exists ! y, y={R}^{2}$. I expand the language with $\mathbb{C}$ and add the axiom $\mathbb{C}=\mathbb{R}^2$. Of course, I can't construct $\mathbb{N}$ and $\mathbb{C}$ from ZFC in 400 characters. But yes, I can do it. – Florian Oct 2 '13 at 1:12
Thank you for having answered me. I just regret that I didn't get a direct answer like the one I will give me in a few minutes, in place of a criticism of my understanding of logic. – Florian Oct 2 '13 at 1:15

When building up mathematics from set theory ($\mathsf{ZFC}$, if you like), we have to make decisions about how things in the mathematical universe are encoded. This is a very time consuming task. Let us consider the simple case of function from one set to another.

We generally make the decision that a function $f$ is defined to be its graph; the set of all ordered pairs $\langle x , y \rangle$ such that $f(x) = y$. Of course, we also have to determine what an ordered pair is. The common current convention is to define the ordered pair $\langle x , y \rangle$ to be the set $\{ \{ x \} , \{ x , y \} \}$. We can show that this identification obeys the basic properties we would hope to be true about ordered pairs (namely that $\langle x , y \rangle = \langle u , v \rangle$ iff $x=u$ and $y=v$).

So given two sets $X , Y$, how do we determine that some set $f$ is a function from $X$ to $Y$? Well here are some steps:

• every element of $f$ must be an ordered pair of the form $\langle x,y \rangle$ where $x \in X$ and $y \in Y$; and
• every element of $X$ must be the first-coordinate of exactly one element of $f$.

Putting this into first-order terms:

• $( \forall u ) ( u \in f \rightarrow ( \exists x ) ( \exists y ) ( x \in X \wedge y \in Y \wedge u = \langle x , y \rangle ) )$ (where this last part is actually an abbreviation for $( \forall a ) ( a \in u \leftrightarrow ( ( \forall v ) ( v \in a \leftrightarrow v = x ) \vee ( \forall v ) ( v \in a \leftrightarrow ( v = x \vee v = y ) ) ) )$); and
• $( \forall x ) ( x \in X \rightarrow ( \exists y ) ( \forall z ) ( ( \exists u ) ( u \in f \wedge u = \langle x , z \rangle ) \leftrightarrow z = y ) )$.

So we have a description within the language of set-theory of what a function between two given sets is. $\mathsf{ZFC}$ has certain axioms that allow us to proclaim that given $X , Y$ there is a set $Y^X$ of all functions $X \to Y$, and then we can quantify over this set: using $( \forall f \in Y^X ) \phi$ as an abbreviation for $( \forall f ) ( f \in Y^X \rightarrow \phi )$. (To be perfectly honest, saying $f \in Y^X$ can itself be seen as an abbreviation for the conjunction of the two formulas given above.)

Although very important, this was an fairly simple step in the long process of formalising "real mathematics" inside set theory. (For example, we still have to construct the sets $\mathbb{R} , \mathbb{C}$ of real and complex numbers.)

You won't be able to find a single formula that will be the un-abbreviation of $u = \{ x_1 , \ldots , x_n \}$ for all possible sets on the right-hand-side. Instead we create a scheme that allows us to construct the requisite formulas recursively.

At its base level $u = \{ x_1 , \ldots , x_n \}$ is an abbreviation for $$( \forall v ) ( v \in u \leftrightarrow ( v = x_1 \vee \cdots \vee x_n ))$$ (where it is clear what the formula will look like for each $n$). Depending on that set on the right-hand-side (if it is given to us explicitly) we may also un-abbreviate each $v = x_i$. For the abbreviation you have given $u = \{ \varnothing, \{ \varnothing , \{ \varnothing \} \} \}$ we work thusly:

• at the base step, this is an abbreviation for $$( \forall v ) ( v \in u \leftrightarrow ( v = \varnothing \vee v = \{ \varnothing , \{ \varnothing \} \} ) ); \tag{1}$$
• noting that $v = \{ \varnothing , \{ \varnothing \} \}$ is an abbreviation for $( \forall w ) ( w \in v \leftrightarrow ( w = \varnothing \vee w = \{ \varnothing \} ) )$, we plug this into (1), yielding $$( \forall v ) ( v \in u \leftrightarrow ( v = \varnothing \vee ( \forall w ) ( w \in v \leftrightarrow ( w = \varnothing \vee w = \{ \varnothing \} ) ) ) ); \tag{2}$$
• noting once again that $w = \{ \varnothing \}$ is an abbreviation for $( \forall y ) ( y \in w \leftrightarrow y = \varnothing )$ we plug this into (2), giving $$( \forall v ) ( v \in u \leftrightarrow ( v = \varnothing \vee ( \forall w ) ( w \in v \leftrightarrow ( w = \varnothing \vee ( \forall y ) ( y \in w \leftrightarrow y = \varnothing ) ) ) ) ); \tag{3}$$
• finally noting, as you have, that $x = \varnothing$ is an abbreviation for $( \forall z ) ( z \notin x )$, we plug all essential instances of this into (3) resulting in $$\begin{multline}( \forall v ) ( v \in u \leftrightarrow ( ( \forall z ) ( z \notin v ) \vee ( \forall w ) ( w \in v \leftrightarrow \\ \leftrightarrow ( ( \forall z ) ( z \notin w ) \vee ( \forall y ) ( y \in w \leftrightarrow ( \forall z ) ( z \notin y ) ) ) ) ) )\end{multline} \tag{4}$$

As you can see, (4) somewhat unwieldy to work with directly or even to comprehend if just given directly, which is the entire point of coming up with abbreviations.

You could expand the language of set theory to include all of these abbreviations, and also extend $\mathsf{ZFC}$ to include all of the defining formulas. This will be a conservative extension, meaning that the same sentences in the un-expanded language will be theorems in each of $\mathsf{ZFC}$ and $\mathsf{ZFC}+\text{(all definitions)}$. But the point of all of this is that one does not have to expand the language. You asked about formalising mathematics within $\mathsf{ZFC}$, and this can be done, albeit not in a pleasant way.

More to the point, if there were no definitions of these new symbols within $\mathsf{ZFC}$ then there would be no guarantee that such an extension was conservative (or perhaps even meaningful).

-
I believe, if I am correct, that you meant : * [...] an abbreviation for $\forall a , ( a \in u \leftrightarrow (\exists v \in a) \wedge ( ( \forall v , v \in a \leftrightarrow v = x ) \vee (\forall v , v \in a \leftrightarrow ( v = x \vee v = y )))$ – Florian Oct 1 '13 at 23:00
$$\begin{multline}( \forall x ) ( ( x \in X \rightarrow \exists y \exists z,z \in f \wedge z=\langle x,y \rangle) \wedge \\ \wedge ( (\exists u \exists v \exists w \exists y, (y \in f \wedge y= \langle x,w \rangle) \wedge (v \in f \wedge v= \langle x,u \rangle)) \rightarrow (u=w))\end{multline}$$ – Florian Oct 1 '13 at 23:11
I tried very hard to formalize such notions as the empty set, the union of sets as abbreviations, but I found it impossible. For example, it is easy to tell that $u=\emptyset$ is an abbreviation for $\forall x, x\notin u$ and that $u=\left\{x,y\right\}$ is an abbreviation for $(\forall z \in u , u=x \vee u=y) \wedge (\exists z \in u)$. But then what does $u=\left\{\emptyset,\left\{\emptyset,\left\{\emptyset\right\}\right\}\right\}$ stand for, etc. ? – Florian Oct 1 '13 at 23:41
It is impossible to give a general definition of this abbreviation, except for considering an expanded language where $\emptyset$ is a constant symbol and "$\left\{.,.\right\}$" is a 2-ary function symbol. – Florian Oct 1 '13 at 23:42
@Florian: The "$(\exists v \in a )$" from your first comment is completely superfluous, since the rest of the formula implies (together with a very small fragment of $\mathsf{ZFC}$) that $\{ x \}$ is an element of $u$. Similarly for your second comment. I'll add quite a bit to my answer to respond to your other comments. – arjafi Oct 2 '13 at 4:12

When we formalize mathematics in $\sf ZFC$ we don't add new symbols to the language of set theory.

The meaning is that we can use sets from the universe of $\sf ZFC$ to encode the operations and symbols from the language we want to work with, and we can formalize the statement "$M$ is an $\cal L$-structure".

Now in $\sf ZFC$ itself we can quantify over functions, over sets of $M$, and so on. Because those are all elements of the universe of set theory. And the statement "Every bounded set of real numbers has a $\sup$" is now a first-order statement in $\sf ZFC$, because it really says something like this:

Every set which is a subset of an underlying set of a structure encoding the field of real numbers and is bounded above, has a least upper bound.

To reiterate the point I am trying to make all along here.

When one uses $\sf ZFC$ as a foundational theory for mathematics, one does not extend the language of set theory. And if one decides to do so, then one adds constant symbols for $\Bbb{N,R,C}$ and so on. Constants which are interpreted as sets in the universe of set theory.

Therefore the statement $\forall f\in\Bbb{C^N}\ldots$ is in fact a first-order statement in the language of set theory which include constant symbols $\Bbb{C,N}$ and an operator for exponentiation.

It should be noted that any addition to the language of set theory is a conservative extension of the language. We rarely add things which are undefinable. For example $\subseteq,\mathcal P,\times,\cup$ and so on are all definable relations and operations on sets. Therefore adding them is just a matter of convenience and we can easily translate any statement to a statement without using these symbols, it will just be very long and unreadable.

-
Every set which is a subset of a structure encoding the field of real numbers has a least upper bound? Does this include the entire underlying set of the structure encoding the field of real numbers? – arjafi Oct 1 '13 at 18:14
Right... That. :-) – Asaf Karagila Oct 1 '13 at 18:24
Sorry for stepping on your toes, but you seem to have missed the point of my above comment. – arjafi Oct 1 '13 at 18:47
It's because of the Quantum Leap... I have a swiss cheese memory! :-P – Asaf Karagila Oct 1 '13 at 18:48
I can't wait until you're nominated for MO mod-ship! – arjafi Oct 1 '13 at 18:50

$$(\star) \forall f \in \mathbb{C}^{\mathbb{N}}, \forall n \in \mathbb{N}, f(n) \in \mathbb{C}$$ is not a well-formed formula in first-order logic, but what it meant was what is meant by the following well-formed formula in first-order logic in the language of a theory $ZFC ++...+$ : $$\forall f \in \mathbb{C}^{\mathbb{N}},\forall n \in \mathbb{N}, \exists c,\exists p\in f, p=\langle n,c\rangle \rightarrow c \in \mathbb{C}$$

-