PCP characterization of NP The PCP theorem (NP= PCP(log n, O(1)) )is a major result in complexity theory with many applications such as proving hardness of approximate results. However, it seems to me that it does not offer any insight that leads to separating P from NP or NP from coNP. My intuition is that P=NP would imply that coNP = PCP( log n, O(1)). That means Tautology instance has a proof that can be verified by an efficient probabilistic verifier using logarithmic random bits and reading only constant number of bits from a proposed proof. It seems that PCP theorem can not shed a light on why Tautology can not have such proof system.


  Why is the PCP characterization of NP not helpful in separating NP from coNP ( or from P)? Is there any known barrier?


** EDIT**: Provided context and motivation.
The PCP Theorem is a theorem about checking proofs, i.e. that there exist locally checkable proof systems, ones that don't "turn from non-accepting to accepting by changes that would be insignificant by any reasonable metric" (quote, top of page 2 here).

Simply stated, it's not directly related to "efficient computation" at all -- more of "efficient checking," for an appropriate definition of efficient.

I suppose it might be possible to use the machinery and terminology of PCPs to attack P vs NP, but it seems likely that such an argument would have a simpler statement under a different model and mode of thought to me. If nothing else -- I haven't seen any attempts in that direction.