[FOM] Re: dichotomies/constructivity

[Robert M. Solovay]

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
is true.

	--Bob Solovay