On Rosser sentences and proof predicates

Abstract

It is a well known fact that the G ̈del sentences γ of a theory T are o all provably equivalent to the consistency statement of T , Con T . This result is independent from choice of proof predicate. It has been proved by Guaspari and Solovay [4] that this is not the case for Rosser sentences of T . There are proof predicates whose Rosser sentences are all provably equivalent and also proof predicates whose Rosser sentences are not all provably equivalent. This paper is an attempt to investigate the matter and explicitly define proof predicates of both kinds.