I've heard about the following result:
The theory of infinite atomic Boolean algebra admits quantifier elimination in the language $\mathscr{L'}$, where $\mathscr{L'}$ is the language of Boolean algebra enriched with some other unary predicates.
For example, the unary predicates in $\mathscr{L'}$ can be $\{A_m(x) \, | \, m \in \omega \}$, where each $A_m(x)$ is the formula that says $x$ has at least $m$ atoms.
I've been trying to find a proof of this result. The only article that I found that contains such a proof is this: http://diposit.ub.edu/dspace/bitstream/2445/127682/2/memoria.pdf.
In this article, the proof makes use of $\omega$-saturated models. I've heard that the theorem is mentioned in (I cannot find this paper online)
Tarski, A., "Arithmetical classes and types of Boolean algebras," Bulletin of the American Mathematical Society, vol. 55 (1949).
Also, it seems that it is also mentioned in the famous paper
Tarski, A., "The concept of truth in formalized languages." Logic, semantics, metamathematics 2.152-278 (1956): 7.
If the theorem dates back to the 1940s, then, I think, the proof that Tarski has in mind cannot involve any modern model theoretic notion like $\omega$-saturated models. My question is: what is Tarski's original proof, or the idea behind Tarski's original proof of this result? Also, are there any other places where I can find a proof of this result?
In The Contributions of Alfred Tarski to Algebraic Logic, Monk writes
Here [49a] is the "paper" (really just an abstract) Arithmetical classes and types of Boolean algebras that you refer to in your question. See also the comments to my answer here.
Monk calls the quantifier elimination "somewhat involved" - but this is the general quantifier elimination result for all theories of Boolean algebras. The atomic case is much simpler, and the thesis you link to gives a nice presentation. And the $\omega$-saturated models are not actually necessary here!
The test for QE used in the linked thesis is Theorem 4.2.20 there: A theory $T$ is complete with QE if and only if for all $\omega$-saturated models $M$ and $N$, the set of all partial isomorphisms between finitely generated substructures of $M$ and $N$ forms a non-empty back-and-forth system (i.e., witnesses $M\cong_p N$).
Let me give you a very similar test: A theory $T$ has QE if and only if for any models $M$ and $N$, and any partial isomorphism $f\colon A\to B$, where $A\subseteq M$ and $B\subseteq N$ are finitely generated substructures, if $\varphi(x,\overline{a})$ is a quantifier-free formula with parameters $\overline{a}\in A$, then $\varphi(x,\overline{a})$ is satisfied in $M$ if and only if $\varphi(x,f(\overline{a}))$ is satisfied in $N$ (actually, by disjunctive normal form, it's enough to handle the case when $\varphi$ is a conjunction of atomic and negated atomic formulas).
The role of $\omega$-saturation of $M$ and $N$ in the statement of Theorem 4.2.20 is just to upgrade satisfying a bunch of quantifier-free formulas in $N$ to satisfying a complete quantifier-free type in $N$, in order to extend $f$ to a larger partial isomorphism (and vice versa in $M$). If you look at the proof of QE for atomic Boolean algebras given in the thesis (Theorem 5.3.4), you'll see that it can be easily modified to use the second test for QE I described above, eliminating any mention of $\omega$-saturated models.
It's an interesting historical question what exact method Tarski used for the quantifier elimination. But I don't have any insight on this. One could probably get some idea by looking at some of Tarski's other papers from around that time in which he proves quantifier elimination results for other structures...