[FOM] Re: dichotomies/constructivity
Robert M. Solovay
solovay at math.berkeley.edu
Wed Sep 11 02:33:32 EDT 2002
On Wed, 11 Sep 2002, Adam Epstein wrote:
> 1) Are there ANY known sentences phi in L(PA) such that
> Con(PA + phi) <-> Con(PA) <-> Con(PA + not phi)
> is provable in PA?
The standard example is the Rosser sentence; It says
[approximately] "If there is a proof of me than their is a proof of my
negation with an earlier Godel number."
> 2) In this situation, how would it be relevant if phi happens to be
> provable in some generally accepted stronger theory such as ZF?
For the Rosser sentence, it is provable in the stronger theory
PA + Con(PA). I have no comment re the "relevance" of this.
> The Paris-Harrington sentence implies Con(PA), so we don't have
> Con(PA)->Con(PA+ph), and I wouldn't know if we have
> Con(PA)->Con(PA + not ph).
The Partis Harrington princeiple is equivalent over PA to the
1-consistency of PA. Hence ph implies Con(PA) over PA. So
PA does not prove Con(PA) --> Con(PA + ph) by Godel II.
Of course, Con(PA) --> Con(PA + ph) is *true* since its conclusion
More information about the FOM