The Coq mailing list

[roconnor AT theorem.ca]

On Thu, 3 May 2018, Freek Wiedijk wrote:

> Hi Russell,
>
> > > To give this a little twist: is a classical proof that
> > > a constructive proof exists just as good as having a
> > > constructive proof?  Or does the latter give you something
> > > extra?
> >
> > It is just as good.
> >
> > A classical proof that a constructive proof exists is a Sigma_1 sentence. By
> > Goedel's Dialetical interpretation all Pi_2 (and hence Sigma_1) sentences
> > provable classically are provable constructively.  So it we can mechanically
> > transform it into a constructive proof that a constructive proof exists, from
> > which one can extract said constructive proof.
>
> I guess you're talking about HA versus PA here?
>
> But what if my "classical proof" is from ZF?  Or from ZFC?
> Or from a consistent extension of ZFC by throwing in some
> large cardinal axioms?  Is that classical proof then still
> just as good?

By Schoenfield's absolutelness theorem ZFC is conservative over ZF for 
Pi^1_2 and Sigma^1_2 sentences, so the axiom of choice can be eliminated.

As for ZF, I don't know.  I seem to recall I was told that this Dialectica 
style argument extends when adding stronger comprehension axioms.  I 
strongly suspect that even with ZF we can make Pi_2 (and Sigma_1).

On second thought, do we have Sigma_1 soundness for ZF?

If we assume ZF is sound. That means if there classically exists a 
constructive proof of X then it is true that there exists a constructive 
proof of X.  So now all we need to do is enumerate all constructive proofs 
until we find one that is a proof of X.

I suspect that we can even use the proof theoretical strength of ZF to 
even come up with a ridiculous, but computable, bound on how far we have 
to search as a function of the size of the proof in ZF.  As we add large 
cardinal axioms this bounding function grows even faster.  Acutally, this 
is staring to sound like how the Dialetica argument works.

Of course if ZF+some particular large cardinal is unsound then you cannot 
trusts its proofs anyways.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''