[FOM] Re: dichotomies/constructivity

[Adam Epstein]

Friedman writes:

> But there is a quick proof without this dichotomy. 

I grant that. In fact, the original teaser concerned monotone unions of
(not necesarily countable) Borel sets.



Would this sort of dichotomy, even one which might, as above, be evaded
through some more detailed discussion, be of more interest in arithmetic?
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?


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? 

For such a sentence, neither phi->Con(PA) nor (not phi)->Con(PA) is
provable in PA. Maybe there is some general construction for this,
but I've never seen such an assertion in any textbook.


2) In this situation, how would it be relevant if phi happens to be
provable in some generally accepted stronger theory such as ZF?



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).



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?