On page $8$ of Holz' Introduction to Cardinal Arithmetic classes are introduced. I have a couple of questions regarding them.
We use capitel letters $A$, $B$, $\ldots$ to denote classes, also with indices, and define the extended formulas as those expressions which may contain the symbols $\{$, $\}$ and $:$ besides the symbols of $\mathcal{L}_{ZF}$ and which are defined in the same way as the formulas with the additional rule that $(A = B)$ and $(A \in B)$, for classes $A$ and $B$, are also atomic formulas.
To be clear, would the following be an equivalent definition of an extended formula?
Extended formulas are any combination of symbols in $\mathcal{L}_{FC}$ along with $\{$,$\}$ and $:$ formed inductively by the following rules:
- If $A$ and $B$ are classes, then
- $(A=B)$ is an extended formula.
- $(A\in B)$ is an extended formula.
- Every formula in $\mathcal{L}_{ZF}$ an extended formula.
- If $F$ and $G$ are formulas, then so are $$\sim F, (F\wedge G), (F\lor G), \exists xF, \forall xF.$$
The authors continue:
If $A = \{x : ϕ(x)\}$ and $B = \{x : ψ(x)\}$, then $y ∈ A$ is the formula $ϕ(y)$, $A = B$ is the formula $∀x(ϕ \iff ψ)$, $A = y$ is the formula $∀x(ϕ \iff x ∈ y)$, $A ∈ B$ is the formula $∃z(ψ(z) ∧ ∀u(u ∈ z \iff ϕ(u)))$, and $A ∈ y$ is the formula $∃z(∀x(ϕ \iff x ∈ z)∧z ∈ y)$, where the variable $z$ can be chosen uniquely (and suitably). Thus any extended formula can be replaced by a formula of $\mathcal{L}_{ZF}$.
What is the meaning of "is" in phrases such as "$y ∈ A$ is the formula $ϕ(y)$"? At first I thought it means the former is an abbreviation of the latter, which would make sense as "$y\in A$" is (formally) not an extended formula. Such notion seems contradictory to the sentence "$A=B$ is the formula $∀x(ϕ \iff ψ)$" as here both are extended formulas, and the author even went through the trouble of stating "$A=B$" is an atomic formula, so it would seem bizarre now claim the expression is an abbreviation for something else. What do the authors mean in this last passage then?
This is a bit different than I'm accustomed to, but it seems to check out.
Usually I think of a "class" in ZFC as an informal way of talking about its defining formula, but here they are thinking of "class" in a more technical way as a term (term in the extended language, not $\mathcal L_{ZF}$). For instance, they stipulate that "variables are classes" (you omitted this part) . With this in mind, $y\in A$ is an extended formula (once you substitute a class for $A$).
I don't understand your comment that $A=B$ and $\forall x(\phi \iff \psi)$ are both extended formulas... the second is an $\mathcal L_{ZF}$ formula (but I don't see what the problem would be if it were an extended formula... as they mention in the last sentence of page 8, they could have allowed nested classes, in which case you'd just need to reduce it again).
The meaning of "is" is that we reduce the extended language to $\mathcal L_{ZF}$ (i.e. eliminate all the $\{x:\phi\}$ terms) by replacing $y\in \{x:\phi(x)\}$ by $\phi(y)$ and so on. I don't know that there's any huge difference between saying it this way and saying that $y\in\{x:\phi(x)\}$ is an abbreviation for $\phi(y).$
On a side note, maybe it's just curiosity on your part, but there's not really any great reason to follow this part of the book closely. Nothing after the first couple of sections depends on the formal details spelled out here. (And this book isn't probably going to be useful unless you already have some comfortability with set theory.)