Do good PCPs for NP give us good PCPs for the entire polynomial hierarchy?

Question

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.

It seems to me that a PCP for a problem almost by definition puts the problem in BPP, which would mean that it is in $\Sigma_2 \cap \Pi_2$ by Sipser–Gács–Lautemann. But maybe also see this related question. — Peter Shor, Dec 12 '11 at 20:37
This sounds reasonable, but I'm confused. If this were right, wouldn't it put NP in BPP? — Ross Snider, Dec 12 '11 at 21:26
Oops. I should have said MA, which is also contained in $\Sigma_2 \cap \Pi_2$. — Peter Shor, Dec 12 '11 at 21:30
this will not work. the PH is resistant to the lemmas involved. consider something like EXP^2. It can handle RP, RNP, etc. as a joke. You're not traveling up that hierarchy easily. — Steve Uurtamo, Nov 28 '17 at 22:43

Kaveh · Answer 1 · 2011-12-13T00:30:57.280

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".

Dana Moshkovitz · Answer 2 · 2011-12-17T14:07:53.920

Let me try to clarify.

Consider the following computational problem: given a mathematical statement (in your favorite axiom system) and a number n given in unary representation, decide whether the statement has a proof of size n.

This is an NP problem: given a proof, one can efficiently verify that it is of size n and that it is a valid proof of the theorem. Note: even if the statement involves quantifiers like FOR ALL, it does not mean that the verifier needs to check all possibilities, it just means that the verifier uses inference rules that involve the FOR ALL quantifier.

The PCP Theorem therefore applies to this problem, and so there is a (different) proof format that allows probabilistic verification.

Another note (regarding Peter's remark): The PCP verifier uses only logarithmic randomness. This means that it could be replaced by a standard, deterministic, verifier that looks at the entire proof. That is having a PCP verifier for a language puts it in NP.

Do good PCPs for NP give us good PCPs for the entire polynomial hierarchy?

2 Answers2