Elementary embedding between infinite atomic Boolean algebras Let $S$ be an infinite set of atoms and let $At(S)$ be the infinite atomic Boolean algebra generated by $S$.
Now suppose we expand $S$ to $S'$ by adding some other atoms, and let $At(S')$ be the infinite atomic Boolean algebra generated by $S'$.
Let $\mathscr{L}$ be the language of Boolean algebra and $T$ be the theory of infinite atomic Boolean algebra in $\mathscr{L}$. $At(S)$ and $At(S')$, as models of $\mathscr{L}$, are both models of $T$ (and hence they are elementarily equivalent). Now my question is: is $At(S)$ an elementary submodel of $At(S')$, in the sense that for any $\phi(x_1, ..., x_n)$ of $\mathscr{L}$, and $a_1, ..., a_n \in At(S)$,
$$At(S) \models \phi(x_1, ..., x_n)[a_1, ..., a_n] \, \, \text{iff}\, \, At(S') \models \phi(x_1, ..., x_n)[a_1, ..., a_n]$$
I can see that $At(S) $ is definitely a submodel of $At(S')$, but I struggle about the quantified forlumas.
 A: (Below, given a set $X$ let $\mathsf{At}(X)$ be the atomic Boolean algebra generated by $X$.)
Yes, as long as $S$ is infinite we have $\mathsf{At}(S)\preccurlyeq\mathsf{At}(S')$ whenever $S\subseteq S'$. The easiest way to see this in my opinion is via the following two facts:

*

*Fact $1$ (Tarski-Vaught): To show $\mathcal{X}\preccurlyeq\mathcal{Y}$ it's enough to show that whenever $\overline{a}\in\mathcal{X}$ and $\varphi$ is a formula such that $\mathcal{Y}\models\exists\overline{x}\varphi(\overline{x},\overline{a})$, there is some $\overline{b}\in\mathcal{X}$ such that $\mathcal{Y}\models\varphi(\overline{b},\overline{a})$.


*Fact $2$: Suppose $A,B,C,D$ are sets with $A\subseteq B\cap C$, $\vert B\vert=\vert C\vert$, $B,C\subseteq D$, and $\vert D\setminus B\vert=\vert D\setminus C\vert$. Then there is an automorphism $\alpha$ of $\mathsf{At}(D)$ which is the identity on $\mathsf{At}(A)$ and restricts to an isomorphism $\mathsf{At}(B)\cong\mathsf{At}(C)$.
The proof of Fact $1$ can be found on the wiki page linked above, and I'm going to leave the proof of fact $2$ as an exercise since it's a bit tedious. The point is that as long as $S$ is infinite we can combine these to show $\mathsf{At}(S)\preccurlyeq\mathsf{At}(S')$ as follows:
Fix a finite tuple of elements $\overline{a}\in \mathsf{At}(S)$ and a formula $\varphi(\overline{x},\overline{y})$ such that $\mathsf{At}(S')\models\exists\overline{x}\varphi(\overline{x},\overline{a})$. We want to find some $\overline{c}\in\mathsf{At}(S)$ such that $\mathsf{At}(S')\models\varphi(\overline{c},\overline{a})$ (if we can do this we'll be done by Fact $1$ above). Let $\overline{b}\in\mathsf{At}(S')$ be such that $\mathsf{At}(S')\models\varphi(\overline{b},\overline{a})$; since $S$ is infinite and $\overline{a}$ is finite we can apply Fact $2$ to get an automorphism of $\mathsf{At}(S')$ which fixes $\overline{a}$ and sends $\overline{b}$ to some $\overline{c}\in\mathsf{At}(S)$. Since automorphisms preserve first-order truth, we're done.

EDIT: actually, the third fact comes up in the above and is probably worth mentioning explicitly:

*

*Fact $3$: The "$\mathsf{At}(\cdot)$-construction" is locally finite, in the sense that for all $X$ we have $$\mathsf{At}(X)=\bigcup_{F\subseteq X\mbox{ finite }}\mathsf{At}(F),$$ and so in particular for every finite tuple $\overline{a}\in\mathsf{At}(S)$ there is some finite $F\subseteq S$ with $\overline{a}\in\mathsf{At}(F)$ (since the finite union of finite sets is finite).

This gets to the precise definition of $\mathsf{At}(\cdot)$. The key is that elements of $\mathsf{At}(X)$ are recursively built up via taking finite joins and meets (and complements); if we take arbitrary joins and meets we wind up building the complete atomic Boolean algebra generated by $X$, $\mathsf{At_{comp}}(X)$, which is a different object. Now as it happens we still have $\mathsf{At_{comp}}(S)\preccurlyeq\mathsf{At_{comp}}(S')$ when $S\subseteq S'$ and $S$ is infinite, since in fact $\mathsf{At}(X)\preccurlyeq\mathsf{At_{comp}}(X)$ holds for all $X$, but this takes a different argument than the above (which crucially uses local finiteness).
In fact, at this point it's probably worth being explicit. There are a few different concrete constructions which can be used here; I think the following are the simplest:

*

*$\mathsf{At_{comp}}(X)$ is the powerset Boolean algebra on $X$; elements of $\mathsf{At_{comp}}(X)$ are subsets of $X$, and the join/meet/complement operations are just union/intersection/complement.


*$\mathsf{At}(X)$ is the subalgebra of $\mathsf{At_{comp}}(X)$ consisting of all sets which are either finite or cofinite. For each $a\in\mathsf{At}(X)$ we can pick out a finite piece of $X$ as being "important" for $a$, namely $a$ itself if $a$ is finite and $X\setminus a$ if $a$ is infinite.
