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.