You are correct. I confused myself by confounding the complexity of the proof with the complexity of finding the proof _given the size of the original problem_. Even for decidable theories like real closed fields, the proofs could be quite long. I seem to recall that if you have a series of alternating quantifiers in the original problem statement, the shortest proof might be exponential (?) in the number of alternations. Of course, once a theory is complex enough so that it can talk about Turing machines with a certain amount of tape, you can diagonalize over all such machines with shorter amounts of tape, and you can in this way force proofs to be as long as you wish. At 12:04 PM 3/19/2012, Gareth McCaughan wrote:
On Monday 19 March 2012 01:58:59 Henry Baker wrote:
Proof _checking_ is a purely mechanical, almost linear complexity (in the length of the proof) problem (depending upon the representation). _Finding_ a proof is the hard part, and can be multiply- (?) exponential in the length of the proof.
Clearly not multiply-exponential, given that proof checking is of approximately linear complexity. All you have to do is enumerate all possible proofs (there are singly-exponentially many) and check them one by one.
-- g