Probabilistic verification of proofs in calculuses

The paper defines a special kind of probabilistically checkable proof system, namely, probabilistically checkable proof calculuses (PCP calculuses). A proof in such a calculus can be verified with enough confidence by examining only one random path in the proof tree, without reading the whole proof. The verification procedure just checks all applications of inference rules along the path; its running time is supposed to be polynomial in the theorem length. It is shown that the deductive power of PCP calculuses is characterized as follows: (i) the decision problem for theorems is in PSPACE for all PCP calculuses, and (ii) this problem is PSPACE-hard for some of them.