[FOM] Re: dichotomies/constructivity
friedman at math.ohio-state.edu
Wed Sep 11 04:25:45 EDT 2002
>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
>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
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
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.
*) the least k for which PH(k) fails is even.
This is of marginal mathematical interest, of course.
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
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.
More information about the FOM