Are "formulas" in Axioms of ZFC indefinite?

Question

There is the Separation Schema in Axioms of ZFC.

Where do "formulas" in this axiom comes from?Are they indefinite and is ZFC actually something like "ZFC(X)" where X is a variable which denotes a collection of formulas?

Added:

Does "the first order language of set theory" defined recursively by logical symbols $\neg,\wedge,\forall$, etc... and a nonlogical symbol $\in$. Are there constant symbols which we can use for denoting "red", "apple", etc... in it?

When someone says "Let $S$ be a set of propositions"(which includes something like "A red apple is red."), for there are no formulas like "x is red" or "x is a proposition" in ZFC, this assertion is invalid or should be interpreted in set theoretic language, assigning words like "red" with a combination of the signatures $\{,\},\emptyset$?

Answer 1

Set theory has a language, and this language has terms, formulas and sentences. Just like any other language in logic.

The schemata in set theory simply give you a template, and they state that for every formula in the language we add an axiom which has a certain form.

Remember that set theory does not happen in vacuum. It is formalized in first order logic.

---

To your edit, the language of set theory includes $\in$ as a binary relation symbol and the usual connectives and quantifiers. You can even omit equality if you want, but it's also useful to have that in the language.

The only terms, if so, are atomic. Namely free variables. How does it work out with "the set of all propositions bla bla"? After we have developed set theory we can develop inside a copy of first order logic. And then we essentially work inside the theory with that copy. So now "red" as a constant is reinterpreted as some set. Much like how you compile code into binary instructions to the processor.

Answer 2

No, they're definitely definite. The axioms of ZF(C) are sentences. (Anyway, the result of binding any free variables in an axiom schema with universal quantifiers is a sentence; think of that as the axiom.)

The comprehension axiom schema states that for every formula $\varphi(x)$ in the first order language of set theory, (the universal closure of) the following is an axiom: $$ \forall y \exists z\,(z=\{x\in y\mid \varphi(x)\}).\tag{*} $$ (If $\varphi$ has additional free variables $v_0, \dotsc v_n$ then assume that the axiom is $\forall v_0, \dotsc v_n \forall y \exists z\,(z=\{x\in y\mid \varphi(x)\})$. For simplicity, however, assume there are no other free variables than those shown.)

Here, $z=\{x\in y\mid \varphi(x)\}$ is a shorthand using "set builder" notation, also known as a "set comprehension". Eliminating it gives the pure first order formula $$ \forall y \exists z\,\forall u\,(u\in z \leftrightarrow (x\in y\land\varphi(x))). $$ Similarly, every instance of the separation schema is, or is equivalent to, a sentence in the first order language with a single 2-place predicate $\in$. The other axioms can be written to use defined terms such as $\{x,y\}$ and $\emptyset$, but these definitions can likewise all be eliminated.

Answer 3

A good way to think of this is that although the axioms of ZFC are infinite in number, there is a computer program that prints them all out, one axiom per row. The "Separation Schema" is the primary subroutine which produces infinitely many axioms. What that subroutine does is to internally go through the infinitely many sentences having one free variable, by following the rules for sentence formation, and for each such sentence the subroutine produces one axiom.