# 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?

• I'm not familiar with the theorem in question, but it is not unheard of in TCS/maths, that nobody ever wrote down all the details of a proof, if the high level argument is sufficient to convince all the experts and the details are tedious. Your description sounds as if this could be such a case. – FrankW Sep 12 '14 at 18:37
• @FrankW Yes, I think that's exactly right. – David Richerby Sep 12 '14 at 19:27