Do good PCPs for NP give us good PCPs for the entire polynomial hierarchy? The PCP Theorem states that every decision problem in NP has probabilistically checkable proofs (or equivalently, that there exists a complete and quasi-sound proof system for theorems in NP using constant query complexity and logarithmically many random bits).

The “folk wisdom” surrounding the PCP Theorem (ignoring for a moment PCP’s importance to the theory of approximation) is that this means proofs written up in strict mathematical language can be checked efficiently to any desired degree of accuracy without the requirement of reading the entire proof (or much of the proof at all).

I am not able to quite see this. Consider the second-order extension to propositional logic with unrestricted use of quantifiers (which I am told is already weaker than ZFC, but I am no logician). We can already start to express theorems which are not accessible to NP by alternating quantifiers.

My question is whether there is a simple, known way of ‘unrolling’ quantifiers in higher order propositional statements so that PCPs for theorems in NP apply equally well to any level of PH. It could be that this cannot be done – that unrolling a quantifier costs, in the worst case, some a constant part of the soundness or correctness of our proof system.
The truth of a statement is different from it having a (short) proof in a proof system. The language is expressive but it doesn't mean that all valid statements in the language have short proofs in the system.

The theorem doesn't say that you can check the truth of a statement or even the correctness of an arbitrary long proof or of arbitrary theorems. It is for proofs of membership in an $\mathsf{NP}$ set, which by definition have polynomial size proofs (certificates) of membership. The theorem only says that you don't need to read the full (polynomial size) proof of membership in an $\mathsf{NP}$ set to decide its correctness.

One implication of the theorem is applying it to the set of theorems in an arbitrary language which have short (i.e. an arbitrary polynomial) proofs in an efficient proof system (i.e. it is decidable in polynomial time if a given string is a proof of a given statement). For example, theorems of ZFC which have proofs of size $n^{100}$ where $n$ is the size of the formula. If the proof system is sound then you can probabilistically verify the correctness of the theorems which have short proofs with reading a small part of their proofs. I think this is the intend meaning of the informal statement "proofs written up in strict mathematical language can be checked efficiently to any desired degree of accuracy without the requirement of reading the entire proof".