FOM: Re: formalizing probabilistic tests

[Harvey Friedman]

Replay to Shipman 2:10AM 9/18/98:

>Harvey, can you please clarify this?  For delta_0 sentences like "n is prime"
>or "multivariate polynomial matrix A is singular" this is obviously true
>because you can just calculate exhaustively, but if your "without resorting to
>this" is supposed to imply that there is a proof over ZFC that is not much
>more complex, you are making a statement with strong complexity-theoretic
>implications (P=BPP if the proof is not only short but also easily found, BPP
>/in NP  if it is just short).  Does your "almost certain" thus mean that
>BPP is "almost certainly" contained in NP, or were you only talking about
>statements of
>higher type than delta_0, or is the ZFC proof allowed to be exponentially
>longer than the
>probabilistic test-proof?

I was talking about arbitrary P. Yes, ZFC proof allowed to be exponentially
longer than probabilistic test-proof.