# Is infinite-length formula allowed in ZFC?

I am curious whether infinite-length formulas are allowed in ZFC. If it is not, then how does it express the case where infinite number of terms (in ordinary mathematics) are being handled? (Like proving that limit of sum of numbers in a sequence is a particular number and so on) (Well, one may say that for limit, that can be done by specifying a formula for sequence, but there are cases where this might not be the case.)

Another way of viewing this problem: can a function or predicate be defined with infinite number of variables (both free and bound)?

For example, given a set of sequences of infinite cardinality (so the number of sequences in the set is infinite), a function takes out nth number from each sequence to form a set (so this function would take one set and map to set)- would this be a valid function in zfc?

-
First order formulas are of finite length, by definition. We can handle infinite objects, however, by coding them as appropriate sets. A sequence, for instance, is just a function with domain $\mathbb N$. And functions are sets. So there is no difficulty handling them in $\mathsf{ZFC}$. –  Andres Caicedo Mar 22 '14 at 23:27
But there are cases where this might not be the case. Example? –  Git Gud Mar 22 '14 at 23:27
Consider the definition of the natural numbers: by the axiom of infinity, there exists at least one set $X$ with $\emptyset \in X$ and for every $S \in X$, $S \cup \{S\} \in X$. Then $\mathbb N$ is the intersection of all such sets. –  Dustan Levenstein Mar 22 '14 at 23:28
For example, given a set of sequences of infinite cardinality (so the number of sequences in the set is infinite), a function takes out nth number from each sequence to form a set (so this function would take one set and map to set)- would this be a valid function in zfc? –  elem Mar 22 '14 at 23:31

I am going to assume that you mean "formula" in the logical meaning of the word. Formulas do not live "within $\sf ZFC$", but rather in the logic outside it, which is first-order logic and therefore does not permit infinitary formulas.

However, internally to $\sf ZFC$ we can define first-order logic, and we can define stronger logics, such as infinitary logics $\mathcal L_{\kappa,\lambda}$ which allow conjunction and disjunction of $<\kappa$ formulas, and $<\lambda$ quantifiers.

But we don't really need that for just simple things, that you might have had in mind, we can talk about functions whose domain is a function from an infinite set into the domain. For example, an $\omega$-tuple is just a function from $\omega$ into $X$. So a function taking $\omega$ variables is really a function taking as input a function from $\omega$ into $X$.

This can be extended in several different ways, but as with everything else in mathematics, once you allow infinite objects into your system, you add difficulties and some cases require more attentive and careful considerations.

-
Do you mean that we can use FOL to define first order ZFC and then in FOZFC define higher order logic? That feels like pulling yourself up by your own bootstraps. –  Trismegistos Mar 23 '14 at 21:21
@Trismegistos: That does feel like that. But there is a distinction, that the internal interpretation of FOL isn't necessary the same as the "outer" FOL. And that's the catch which prevents it from being circular like that. –  Asaf Karagila Mar 23 '14 at 21:58

In ZFC, sequences are represented by functions over $\mathbb{N}$. And functions, in turn, are represented by sets of pairs mapping an element of to domain to an element of the codomain. Thus, a sequence in ZFC corresponds to a set $\{(0,a_0),(1,a_1),\ldots\}$, where pairs $(a,b)$ stand for the set $\{a,\{a,b\}\}$. A set can thus represent a whole sequence, so infinit formulas aren't required to talk about infinite sets.

The ZFC axioms are usually formalized in first-order predicate logic, which does not permit infinit formulas. In principle, you could take the axioms of ZFC, and use some kind of infinitary logic. But for these logics, the compactness and completeness theorems fail, so you'd have to tread very carefully. These theorems guarantee that sentences are semantically true (i.e., true in all models) exactly if they are provable, and that theories are semantically consistent (i.e., have a model) exactly if they prove no contradiction. These aren't properties that one would give up lightly.

-