Ssreflect Users Discussion List

[Kevin Buzzard <>]

On 14 June 2017 at 18:59, Emilio Jesús Gallego Arias
<>
 wrote:

[snip]

> Indeed, AFAICT the proof is fully carried out within the logical system
> of Coq, which doesn't validate the full Axiom of Choice and is, TTBOMK
> is weaker than (classical) ZFC.

I've chased this up now, and my understanding of it (largely based on
"Sets in Types, Types in Sets by Benjamin Werner") is that (CIC + some
type version of axiom of choice + infinitely many universes) is
basically the same strength as ZFC + infinitely many inaccessible
cardinals. In particular Coq (which I believe is CIC but the type of
a type is a type in a bigger universe so there are infinitely many
universes) as it stands is going to be a lot stronger than ZFC.

My original question / hope was that we would be able to formally
translate the proof of the odd order theorem given by Coq into ZFC. I
now suspect that this cannot follow *formally*, because Coq seems to use
a deduction system which his much stronger than ZFC (existence of just
one inaccessible cardinal is enough to prove consistency of ZFC).

However my understanding of Theorem 16 of Werner's paper is that if
one could machine verify that the proof really took place in the
*fragment* of (CIC + excluded middle + some appropriate choice
function) where we only use universes up to Type_1.

On the face of it, this might be verifiable. Although I am just
beginning to study the odd order proof, my impression is that this
"standard style" mathematical proof would translate into an argument
in Coq that did not ever start asking what the type of a type was; it
should surely be taking place within some user-defined types like
groups, representations etc.

In short -- has there been a computer verification of a ZFC-only proof
of the odd order theorem?

Kevin

>
> Inside Coq, you can see what axioms a particular theorem may depend on
> using the "Print Assumptions Theorem_name." command.
>
> Note however that while Coq doesn't fully validate the excluded-middle
> principle "forall P : Proposition, P \/ ~P", it does validate it for a
> large subset of such propositions. In particular, boolean, or decidable
> propositions enjoy the EM property.
>
>> Now if on the other hand one were to start considering formalising the
>> proof of Fermat's Last Theorem, say, then one would need a whole bunch
>> of delicate real analysis (for the trace formula part of the argument
>> where one proves that the 3-torsion of an elliptic curve is modular if
>> irreducible) and in this part of the argument I am sure that AC will
>> be used a lot. It would seem natural to me more generally to start
>> proving results from many pure mathematics courses at undergraduate
>> level, assuming one is working in a first order theory and working
>> under the axioms of ZFC (this is, it seems to me, what is implicitly
>> going on in many undergraduate level pure courses).
>
> Lets call Coq's logic CIC, note that indeed CIC + AC is consistent,
> so in this case you can (and it may make lots of sense) to add these
> additional axioms to your development.
>
> This is not usually a problem, and there are techniques that will
> translate a classical proof with choice to a constructive one if you
> really need it (however they always carry some form of overhead).
>
>> I am hoping to understand more over the next few days. I would be very
>> interested in any pointers that people may have where I could learn
>> more about what one literally means precisely by "the odd order
>> theorem has been verified".
>
> Are you aware of the main paper about the formalization?
>
> https://hal.inria.fr/hal-00816699/file/main.pdf
>
> Best regards,
> E.