S is a Rosser proof of the formula A iff S is a proof of A and all proofs S' with smaller Godel code than S don't prove not(A). The great thing about Rosser provability is that it is consistent: you can prove in 1st order Peano arithmetic that for all x, x isn't the Godel code of a Rosser proof of 0=1. The not so great thing about Rosser provability is that it can be a bit, well, slow to check if S is a Rosser proof of A. This leads me to my first question: (1) Given a length n proof of A, what's the computational complexity of checking that it is a Rosser proof? Naively, it's something like O( n 2^n ), but surely you can do a bit better? My second question is probably conclusive evidence that the whole field of logic is just too darn subtle for me: (2) Is there a normal provabile but not Rosser provabile formula A? If so, why doesn't this imply the existence of a proof of not(A) [aka the inconsistency of PA] ? If not, why doesn't this prove the consistency of normal provability? -Thomas C