Solovay's Arithmetical Completeness theorem states that if $A$ is sentence of modal logic, then if every realization $A^*$ of $A$ is proved by $\mathsf{PA}$, then $\mathsf{GL}\vdash A$.
The way this is proven is through "embedding" Kripke models into $\mathsf{PA}$, and constructing a sequence of Solovay sentences such that $\mathsf{PA}\vdash\bigwedge_{1\le i\le n}[\mathsf{Bew}(\neg S_i)\rightarrow\neg S_i]\rightarrow S_0$ and $\mathsf{PA}\vdash S_0\rightarrow\neg \mathsf{Bew}(A^*)$. Each of the Solovay sentences $S_j$ affirms that the limit of a function $h$ is $j$. Meanwhile function $h$ is defined as follows:
The proof then proceeds by proving like $10$ lemmas till we finally get completeness from all of this. But is there any intuitive, informal way of saying what's happening here? For example, in Godel's incompleteness theorem, we know that we are aiming to construct a sentence that "says of itself" that it's unprovable. And even if that's not entirely accurate, that intuition greatly helps in understanding where each step of the proof is headed. Is there any such simple, informal statement of what Solovay's theorem is aiming to construct?