881: Some Logical Thresholds (Harvey Friedman)

[Juan P. Aguilera]

Concerning the question:

> On a vaguely related note, there used to be an open problem of whether
> any two Rosser sentences for PA (and other systems) are provably
> equivalent over PA, or even over EFA. Is still problem still open?

There is a theorem of Guaspari and Solovay (AML 1979) by which the answer depends on how one formalizes “provability in PA.” More precisely, there are extensionally correct Sigma_1 provability predicates P, Q (which can be assumed to satisfy Modus Ponens and provable Sigma_1 completeness) such that
i) all Rosser sentences for P are provably equivalent.
ii) not all Rosser sentences for Q are provably equivalent.

As far as I know, the problem for the “usual” proof predicate (i.e., the one used by Gödel) is still open.

Regards,
Juan