Reference proof for Second-Order Logic captures Polynomial-Time Hierarchy I'm looking for a complete proof of $\mathrm{PH=SO}$. The (admittedly few) textbooks and papers i've looked at all either state that it's a corollary from Fagin's Theorem, or leave it as an exercise to the reader. Even Stockmeyer's original paper on the hierarchy (this one, right?) proves the result in a "Remark." section, so it's not exactly the most detailed proof. 

Just so we're clear, i did write my own version of the proof; it's exactly because of all the work i had to do in order to prove said result, contrasted with the one-paragraph proofs commonly found in the literature, that makes me curious about what kind of insight i might be missing. 

As for how my proof proceeds, i can give an high-level overview of the harder direction. Using the certificate version of the hierarchy, and second-order logic with alternating quantifier blocks, the proof goes by induction. Base case is Fagin's Theorem. For the inductive step, you have a second-order formula deciding the input+certificate relation, so all you need to do is to introduce some existential quantifiers over the given formula quantifying all of its relational symbols, plus a formula that states that the interpretation given by the quantifiers does contain the input.

Of course, like any high-level overview, this is easier said than done. At least in my proof, there's a fair amount of translating in order to make things work. Plus there's the fact that the usual certificate definition is over languages, and we're dealing with arbitrary finite structures, so there's some conversion there too. Then you have to prove that all the stuff you did is in fact correct. All in all, it's not pretty.

So i have to ask: Is there any proof of this result that isn't afraid of working out some of the details, but has the same intuitive clarity as the usual short proof?
It's one of those proofs that's essentially obvious once you can prove Fagin's theorem that the existential fragment of SO is exactly NP. Alternating quantifiers in the SO formula takes you up the polynomial hierarchy more or less by definition.

Proposition 7.35 of Libkin's Elements of Finite Model Theory proves that MSO expresses complete problems at every level of PH. Corollary&nbsp;9.9 of the same book is that SO=PH; but the proof consists of a sketch with an exercise to fill in one of the steps.  The proof that SO=PH is also essentially Exercise&nbsp;7.5.18 of Ebbinghaus and Flum's Finite Model Theory (2nd ed.). Immerman's Descriptive Complexity states the equivalence as Theorem&nbsp;7.21 and Corollary&nbsp;7.22 but leaves the proof as an exercise and credits the result to Stockmeyer's paper.

Given all of that, I doubt you'll find a proof in print. The details probably are fiddly but your outline sounds correct.