[FOM] Re: dichotomies/constructivity

[Harvey Friedman]

>
Epstein writes:

>Would this sort of dichotomy, even one which might, as above, be evaded
>through some more detailed discussion, be of more interest in arithmetic?

This dichotomy issue seems to be of clear interest in the context of 
issues of constructivity. If the underlying mathematics is far 
removed from constructivity, then the burden of proof lies on the 
person suggesting that it is interesting.

Years ago, I looked at versions of set theory with intuitionistic 
logic, a lot with Andre Scedrov. Also at versions of set theory where 
bounded quantification is treated classically, but not unbounded 
quantification. However, in connection with the continuum hypothesis, 
I don't see how to make sense of what you are probably trying to do. 
I think, however, that it is quite possible that it could be made 
sense of.

>Let's not fixate on the Riemann Hypothesis, which might well be a red
>herring; rather, why not try to cook up something like what we have in ZF,
>where both CH and its negation are provably equiconsistent with the
>base theory?


Yes. The Rosser sentence.

>
>
>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?


Let R be the Rosser sentence "every proof in PA of this sentence has 
a shorter proof in PA of the negation of this sentence". I shouldn't 
say "the" but rather "a". By "shorter" I mean with "smaller godel 
number".

DIGRESSION. I recall seeing some paper (JSL??) concerning uniqueness 
of Rosser sentences. Of course, this is most interesting with a 
completely standard godel numbering. I don't know if the question was 
entirely satisfactorily resolved.

The well known result is:

PA proves Con(PA + R) iff Con(PA) iff Con(PA + not R).
>
>2) In this situation, how would it be relevant if phi happens to be
>provable in some generally accepted stronger theory such as ZF?

R is provable in PA + Con(PA).

>
>3) Are there any such sentences of some mathematical interest?
>
>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).

We certainly have Con(PA ) implies Con(PA + not PH).

Let PH(k) be PH with exponent k. It is well known that for each k, 
PH(k) is provable in PA.

Consider

*) the least k for which PH(k) fails is even.

This is of marginal mathematical interest, of course.

Then

PA proves Con(PA) iff Con(PA + *) iff Con(PA + not *).

>
>
>4) Given such a sentence phi, suppose that some actual theorem of PA could
>be established via the dichotomy phi or (not phi), but perhaps not so
>readily, or even not at all, otherwise. Is this even a meaningful
>speculation? Would there be any foundational significance to such a
>phenomenon?


In the ideas surrounding what I think you are driving at, the only 
thing I am confident is important is to come up with some real 
examples of arithmetic theorems that can be shown to have no 
constructive (intuitionistic) proofs. This is distinct from the 
question of arithmetical theorems that have no finitary or 
predicative proofs or no proofs within ZFC. The only example I know 
of is the trivial theorem

THEOREM. Any polynomial of several variables with integer 
coefficients assumes a value of least magnitude over the integers.

This is not provable in any reasonable intuitionistic system, using 
the negative solution to Hilbert's 10th problem.