Lists of sets as objects of ZF axiomatics

Question

I have a naive question about foundations of mathematics. A common opinion of most mathematicians is that the essential part of mathematics can be reduced to ZF(C) axioms. I do not quite understand one of basic steps of this reduction. How to define rigorously an intuitive concept of "a finite sequence of arbitrary length consisting of arbitrary sets", in other words a concept of a sequence $X_1,X_2,\dots X_n$ where all $X_k$ are arbitrary sets. A difficulty here is that usually a finite sequence $y_1,\dots y_n$ (i.e. a list) is defined as a function from the segment $\{1,\dots n\}$ to some set $Y$ (i.e. as a sequence of elements of some set) but if we want to deal with arbitrary sets $X_k$ we do not have a priory such a set $Y$.

More specifically, is it possible to formulate the following intuitive theorem as a single formula of ZF: "for any finite sequence of countable sets $X_1,\dots X_n$, their union is countable" or such a theorem can be realized in ZF only as a kind of theorem scheme?

---

Edited after receiving first answers: Thanks everyone for explanations! As far as I understand now, everything depends on the definition of a function which is used. The problem described in my question appears if one uses the traditional definition of a function as a binary relation having functional property (as presented, e.g. in Wikipedia) because the domain and codomain must already exist as sets before we obtain a function according to this definition. But if we use another definition of a function as an arbitrary set of ordered pairs which satisfies functional property (see the comment of Max), we have no problems!

Answer 1

That's not an issue. It is true that there is no set of "all finite sequences of countable sets". But this is a theorem.

If $f$ is a finite sequence of countable sets, this means that $f$ is a function, whose domain is some $n<\omega$, and for each $i<n$ we have that $f(i)$ is a countable set.

Using the axiom of replacement, $\{f(i)\mid i<n\}$ is a set as well, so $\bigcup\{f(i)\mid i<n\}$ is again a set. And we claim that it is countable.

This is no more a schema, than "Every even number can be realized as the sum of two primes" is a schema in the language of first-order arithmetic. And of course it's not a schema.

Answer 2

Sure, totally possible, though it won't necessarily be pretty if you want it to be entirely in the language of $\mathsf{ZF}$ (you have make a formula saying something is a function, specifying the domain and codomain of a function, of saying that something is a union of a given set, of $\omega$, and of saying that something is countable). None of it is particularly hard, just long.

Let $\mathrm{natural}(x)$ mean that $x$ is a natural number, $\mathrm{func}(f)$ mean that $f$ is a function (from some domain into some codomain), $\mathrm{dom}(f,x)$ mean that $f$ is a function and its domain is $x$, $\mathrm{im}(f,y)$ mean that $f$ is a function and its image (i.e. range) is $y$, $\mathrm{union}(X,x)$ mean that $x$ is the union of the family of sets $X$, and $\mathrm{countable}(x)$ to mean that $x$ is countable. All of these things are perfectly definable (once you decide how you want to define a function, say as an ordered-triplet).

Then there are a few different ways you could express what you want. One approach is to say, "For every natural number $n$, every finite sequence of length $n$ whose elements are countable has the union of its image countable". I'll assume you mean "countably-infinite" by "countable", but if you just mean "finite or countably-infinite", the sentence is still the same:

$$\forall n (\mathrm{natural}(n) \rightarrow \forall f \forall X \Bigl( \bigl( \mathrm{dom}(f,n) \wedge \mathrm{im}(f,X) \wedge \forall x (x\in X\rightarrow \mathrm{countable}(x))\bigr) \rightarrow \forall y (\mathrm{union}(X,y) \rightarrow \mathrm{countable}(y) )\Bigr) )$$

Now, I claimed that each of the formula $\mathrm{natural}$, $\mathrm{func}$, $\mathrm{dom}$, $\mathrm{im}$, $\mathrm{countable}$, and $\mathrm{union}$ can be expressed entirely in the language of $\mathsf{ZF}$. Really all of this amounts to just writing down the definitions of these things in symbols, and is not difficult (though can be a bit time consuming). As an example, consider $\mathrm{natural}$. Here we're using the Von Neumann definition for the natural numbers, so the set of all natural numbers $\omega$ is the intersection of all inductive sets. Define $\mathrm{inductive}(I)$ to stand for $$\exists x (\forall y (\neg y\in x) \wedge x\in I) \wedge \forall y (y\in I\rightarrow \exists z (z\in I \wedge \forall w (w\in z\rightarrow (w\in y) \vee (w=y))))$$ (i.e. it says that $I$ is an inductive set). Then we may define $\mathrm{omega}(X)$ to mean that "$X$ is the set of natural numbers" by $$\forall x (x\in X\leftrightarrow \forall I (\mathrm{inductive}(I) \rightarrow (x\in I))$$ and finally $\mathrm{natural}(n)$ can be expressed by $$\forall X( \mathrm{omega}(X) \wedge n\in X)$$

Answer 3

A traditional way to formalize the notion of "function" in set theory goes like this:

a function is a set $f$ of ordered pairs such that, if $(x,y)\in f$ and $(x,z)\in f$ then $y=z$.

Given this definition, the expression ``$f(x)$'' can be explained to denote the $y$ such that $(x,y)\in f$.

Assuming that the function $F$ which $f$ formalizes is ``total'', then you can extract from $f$ the domain of $F$, namely as the class of $x$ such that $(x,y)\in f$ for some $y$.

However, there's no way to recover the range of $F$ from $f$. For example, the object

$\{(x,y):x\in\mathbb \omega\land y=0\}$

might formalize a function $F:\mathbb N\to\mathbb N$ or a function $F:\mathbb N\to \{0,1\}$ or...

This approach to formalizing functions ducks the problem you mention. That is, a mapping of $F$ from integers $i< k$ to arbitrary sets $F(i)$ becomes the "set-sized" collection of pairs $(i,F(i))$ for $i<k$.

There is another way to think of functions as formalized, namely as proper classes, but I don't know that it's useful in formalizing ordinary mathematics.