Ytukyg

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?

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.