Rosser orderings and free variables (Q1176097)

Guaspari and Solovay have proposed the arithmetically complete modal system \(R\) of provability in the case where Rosser sentences are taken into account. In this paper the authors prove that if free variables are included, the arithmetically complete system is not \(R\) but \(R^ -\) of Guaspari and Solovay, which has been introduced for the sake of \(R\) first. From this completeness result, there follow the non-validity of some rules and that some principles concerning Rosser orderings cannot be decided even by the usual proof predicates in the case where free variables are included.