[FOM] Machine-checkable proofs: NP, or worse?

[Mitch Harris]

On 6/20/07, someone wrote:
> On Monday 18 June 2007 00:21, Mitch Harris wrote:
> > Since 'winnability in nxn checkers' is in PSPACE', the
> > proof/calculation for 8x8 might be bad. And even if some one claims to
> > have one, it may take a long time, as far as we can guess now, even
> > exponential in the size of the proof to check it.
>
> since you're saying that checking may take time exponential in the size of the
> proof, maybe you could elaborate on your notions of "proof" and "checking".
>
> Don't most proof systems allow checking in polynomial (or even linear) time in
> the size of the proof?

Yes, I terribly misspoke in that last sentence of mine, using the
terms ambiguously, not only conflating proof verification with proof
finding, but also informal vs. formal proof.

In that paragraph above, I was writing about -checking- an -informal-
proof, where so-called 'trivial' steps in checking a human oriented
proof may request the reader to use a well known decision procedure
(solving a linear system of equations, deciding satisfiability of a
boolean formula, deciding equality of two regular expressions, etc up
the complexity hierarchy). Such a 'trivial' step, having arbitrarily
bad complexity, is essentially proof -finding- (even if a proof or
proof witness is not produced).

As to the original question of proof finding (for checkers), for a
-formal- proof, I don't see how checking it could be anything other
than poly time in the size of the proof (linear time with appropriate
data structures?) in the size of the proof (almost by definition of a
formal proof) since all that is being checked is correctness of each
step. But of course, the size of the proof could be exponential in the
size of the theorem statement (e.g. any problem complete for EXPSPACE)

-- 
Mitch Harris