What does this set-theoretic notation mean in the proof of this theorem?

Question

From A friendly introduction to mathematical logic,

In the first red box below, what does this notation mean?

And in the second red box, how exactly is this process repeated?

---

Answer 1

what does [the highlighted] notation mean?

Note 1 : the set $B$ is the uncountable domain of the structure $\mathfrak B$ and $A_0$ is a nonempty countable subset of $B$.

The function $s: \text {Vars} \to A_0$ is the usual variable assignment function that maps variables of the language into objects of the domain of an interpretation: in this case $A_0$.

We have : "for each formula $\exists x \alpha$ and functions $s$ and $s'$ ... choose an element $a_{\alpha, s'}$ in $B$ [i.e. an object of the domain] such that..."

Now take the set $\{ a_{\alpha, s'} \}_{\text {all } \alpha, s': \text{Vars} \to A_0}$ of all such elements and set : $A_1 = A_0 \cup \{ a_{\alpha, s'} \}$.

Then consider "for each formula $\exists x \alpha$ and functions $s$ and $s'$ ... such that..." and build the new set $\{ a_{\alpha, s'} \}_{\text {all } \alpha, s': \text{Vars} \to A_1}$ and set $A_2 = A_1 \cup \{ a_{\alpha, s'} \}$.

And so on...

At the end of the process, the union of all $A_i$'s will be the domain of the countable substructure needed for the theorem.

---

how exactly is this process repeated?

Note 2 : in the initial stock of functions we have $s : \text {Vars} \to A_0$. We use them to enlarge the initial set $A_0$ to a new set $A_1$ with more elements.

Due to the fact that $A_1$ has new elements, in the succesive step the stock of functions $s : \text {Vars} \to A_1$ will be "larger", due to the fact we start with $A_0 ⊂ B$ but we "throw in" new elements of $B$ that not necessarily are in $A_0$.

The tricky point is the reason for "iteration"...

We have to recall the clauses defining the satisfaction relation $\vDash$ : $\mathfrak B \vDash \exists x \alpha [s]$ means that there is a variable assignment function $s'$ that agree with $s$ on every free variable of the formula such that $\mathfrak B \vDash \alpha [s'[x|a]]$, for some $a \in B$.

We start with $\exists x \alpha$ and $s : \text {Vars} \to A_0$ such that $\mathfrak B \vDash \exists x \alpha [s]$.

But it may happen that $\mathfrak B \vDash \exists x \alpha [s]$ does not hold because there is no suitable "$x$-variant" $s' : \text {Vars} \to A_0$.

In the following steps, when we have enlarged $A_0$, this may change and a new $s$ pops-up such that $\mathfrak B \vDash \exists x \alpha [s]$.

This is why at each step we have to review" every existential formulas.

Note 3 : Why consider only existential formulas ?

Because obviously every universal one that is true in the larger structure will holds also in every subset of the structure (if every ball in my box are black and I pick up at random five balls from it, for sure they will be black. It is not the same if in the box there is one white ball: I'm not certain that in the five chosen balls there is the white one.)

The issue is that with the existential formula like $\exists x \alpha$, we have no certainty that the "witness" (if any) is included into $A_0$.

The process described above amount "simply" to this : starting from the countable $A_0$, throw in countable new elements [because thera are countable many iterations] that are enough to satisfy all the existential formulas.