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).

(2) Is there a normal provabile but not Rosser provabile formula A?

No if the Peano axioms are consistent; yes if they are inconsistent. That is, the statement 'Every provable formula is Rosser provable" is equivalent to the statement "The Peano axioms are consistent". Both are true (or at least provable in ZF, if you believe ZF is consistent), but neither is provable from the Peano axioms. Andy Latto andy.latto@pobox.com