# Can you quantify over an ordered set in first order logic?

If you are working in first-order logic, can you define a sequence $f_{n}$ of $n$-ary functions (i.e. the $n$th function takes in $n$ inputs), and then later say

$(\exists n)(u = f_{n}(x_{1}, \cdots,x_{n}))$

I suspect that you can, but this also sounds suspiciously like second-order logic.

-

If you work in a signature that simply has a sequence of function symbols $(f_1, f_2, \ldots)$ then there is no way to quantify over these symbols. Any annotations on symbols in the signature are for our benefit only and are invisible to the theory itself. It makes no difference if the arities are the same or different.

One thing you can do to work around this is to make the functions binary, and use elements of the domain to index the functions. So you could make the signature have a single function symbol $F(x,y)$ and write $(\exists x)[u = F(x,y)]$. It would be suggestive to write $F_x(y)$ instead of $F(x,y)$.

If your signature includes some sort of sets, then you can often code functions by coding their graphs into the sets. For example, in ZFC it is perfectly possible to form a set of functions $\{f_n\}$ and then quantify over the $n$. Note that in this case the symbols $f_n$ are not part of the signature; they are merely how we are denoting some objects in the domain of a structure.

There is a final problem with $(\exists n)([u= f_n(x_1, \ldots, x_n)]$. As written, it seems that formula does not have a well-defined set of free variables, so it is not actually a formula. The usual way to work around this, as yaakov mentioned, is to move to a function that takes a single tuple as input, so that the arity is fixed at 1.

-

You can't do it in any straightforward way because you can't combine functions of arbitrary input length (n-ary) to any single formula - it won't be long enough.

In particular cases, (such as the system of the natural numbers), you can use an "encoding" for n-tuples of any length, and for the evaluation of specific functions (such as recursive functions) - and such a thing could be formulated.

-