Are All Formulas in ZF Set Theory Finitary?

[alexfloo]

I've never been exposed to this axiom schemata of replacement before, so here's my understanding of it: the axiom includes an arbitrary formula, and that formula may have arbitrarily many free variables. Therefore, a separate axiom is needed for formulas with one free variable, with two free variables, and so on.

So my first request is to criticize the above, but if it is correct, I have two questions:

First of all, the formalization of the schema I saw presented it as having a "last" free variable. Is the axiom schema only valid for fomulae with finitely many free variables? Are these the only formulas that exist, perhaps? Or is this just an artifact of the fact that the infinite multitude of axioms that fall under this schema just can't properly be recorded in the formal language?

Secondly, couldn't it be shown that every formula with k free variables is equivalent to another formula with only one? This would certainly be true if it were possible to guarantee the existence of k distinct objects in the universe, because then those k objects could be used to index a k-tuple: a single free variable which uniquely identifies all the old ones.

 

[Hurkyl]

the axiom includes an arbitrary formula

Actually, you can't even do that (in first-order logic) -- instead, the axiom schema actually includes one axiom for every formula.

Are these the only formulas that exist, perhaps?

Yes. Unless otherwise stated, "logic" refers to finitary logic (as opposed to infinitary logic), so that any particular formula consists of finitely many symbols.