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 ?
How can one quantify on a function in ZFC?
764 Views Asked by Bumbble Comm https://math.techqa.club/user/bumbble-comm/detail AtThere are 3 best solutions below
On
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.
On
$$(\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}$$
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:
Putting this into first-order terms:
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.)
Response to comments below
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:
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).