Randomized proofs in arithmetic

A randomized proof system for arithmetic is introduced. A proof of an arithmetical formula is defined as its derivation from the axioms of arithmetic by the standard rules of inference of arithmetic and also one more rule which we call the random substitution rule. Such proofs can be regarded as a special kind of interactive proof and, more exactly, as a special kind of the Arthur–Merlin proofs. The main result of the paper shows that a proof in arithmetic with the random substitution rule can be considerably shorter than an arithmetical proof of the same formula. Namely, there exists a set or formulas such that (i) these fo nulas are provable in arithmetic but, unless $\mathrm{PSPACE}=\mathrm{NP}$, do not have polynomially long proofs; (ii) these proofs have polynomially long proofs in arithmetic with random substitution (whatever random numbers appear) and the probability of error of these proofs is exponentially small. Bibliography: 10 titles.