Ssreflect Users Discussion List

Sorry for being very late to this thread, but I have some comments.

Regarding the use of the Axiom of Choice for something like Fermat's last 
theorem, we can lean on some meta-logical theorems here.  Specifically 
Shoenfield's absoluteness theorems states that in ZF, the axiom of choice 
is conservative over Sigma^1_2 / Pi^1_2 formulas in the analytic 
heirarchy.  Since the statement of Fermat's last theorem lives well below 
that level of complexity, we know that if ZFC proves Fermat's last 
theorem, then ZF proves Fermat's last theorem.  So, in principle, all uses 
of the axiom of choice can be eliminated from the proof.

Goedel's Dialeticia interpretation proves that every Pi^0_2 formula that 
is provable in Peano Arithmetic can be proven without excluded middle (in 
a system called Heyting Arithmetic).  Again, Fermat's last theorem is 
below this level in the arithemetic heirarchy and can be proven without 
excluded middle, if it can be proven in Peano Arithmetic.

I strongly suspect that Fermat's last theorem can be proven in Peano 
Arithmetic.  However, even if FLT does require stronger induction 
principles than PA provides, I believe this Dialetica interpretation 
result is resonably robust and Fermat's last theorem can be proven without 
excluded middle (and by Shoenfield's absoluteness theorem, also without 
the axiom of choice).


Although it has been several years, I worked primarily on the Galois 
theory used in the proof of the Odd Order theorem.  My main goal was to 
prove the fundamental theorem of Galois theory.  Technically this when a 
little beyond what was needed for the Odd Order theorem, but essentially 
all the results leading up to the fundamental theorem of Galois theory 
(mostly about when you get separable field extensions) was needed for the 
Odd Order theorem.

The work on Galois theory is limited to field and field extensions with 
decidable equality and satisfying countable choice.  However, this is a 
distinction that only exists in constructive mathematics.  In classical 
set theory, every equality is decidable, and every set has choice, 
whether countable or not.

On Fri, 16 Jun 2017, Assia Mahboubi wrote:

> Dear Kevin,
>
> Le 14/06/2017 à 17:05, Kevin Buzzard a écrit :
> > Now Emilio has pointed me to the ssreflect mailing list let me explain
> > what I believe will be a stumbling-block for me later. My impression
> > from reading the Feit-Thompson Coq paper by Gonthier et al is that the
> > Coq proof of F-T is all done in "constructible mathematics",
>
> Indeed. This proof is formalized in the type theory implemented by the Coq
> system, without adding any extra "axiom". This logic described by Coq's type
> theory is a constructive one and in particular, the axiom of excluded middle
> cannot be derived from the rules of this logic.
>
> The intuition being that in this logic, any provable statement can be 
> "realised"
> as an effective procedure.
>
> > so we are
> > probably not using the Axiom of Choice.
>
> True, we are not using the strongest form of the Axiom of Choice, which cannot
> be derived either from the rules of Coq's logic. But actually we are using a
> weaker one, which can be derived in Coq's logic, the so-called axiom of
> countable choice. In this context, it is expressed as :
>
> 1) if a type T has only countably many inhabitants,
> 2) if P is a predicate such that the disjunction P(x, y) \/ not P(x,y) holds 
> for
> any x, y (remember we do not have excluded middle)
> 3) and is for any inhabitant x of T, there is a y such that P(x,y)
> 4) then you can forge a choice function f, such that P(x, f(x))
> 5) (in fact you also know that f is the same for all the equivalent Ps).
>
> The intuition is that 2) expresses that for any x, looking for a witness w 
> such
> that P(x,w) holds is a terminating process. Thus it is easy to elect a 
> canonical
> witness for any x : just use the canonical enumeration of the inhabitants of T
> provided by 1) to test the elements of T in order, and pick the first w that
> verifies P(x,w).
>
> > 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.
>
> This is really interesting. If it is easy for you, I would be interested in
> pointers to places in this proof where you think that stronger forms of choice
> than countable choice (dependent choice? or even a Zorn-like choice?) is
> required in the proof.
>
> > 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).
>
> I understand that this is a natural idea, and I agree that this is what is
> pointed out in the textbooks that have a few words about foundations.
>
> But I am not sure that this would actually work in practice, when "what is
> implicitly going on" has to be made explicit.
>
> One of the things that the computer does not (cannot) check, is that the 
> formal
> sentence written in the low level language of logic actually describes what 
> you
> have in mind as a human mathematician. It will never prevent a user to call a
> cat what is defined as a dog. Only the human eye can validate that a formal
> theory speaks about what it pretends to.
> At the same time, the mechanical proof checker needs several orders of 
> magnitude
> more details than the trained eye of a human reader, in order to make sense 
> of a
> mathematical statement. If this noisy part of mathematical sentences are 1)
> provided by hand 2) displayed entirely to the human eye, formalisation soon
> becomes intractable. The choice of the logical system underlying a proof
> assistant has a significant impact on the way to deal with this issue and the
> choice of a first order language is probably not the best for the purpose of
> mechanised proof-checking.
>
>
> > However my impression is that this
> > is not what is going on in the Feit-Thompson work.
>
> Indeed, it is not. The formalisation takes place in the so-called Calculus of
> Inductive Constructions (CIC), which is a flavour of type theory. It uses the
> so-called "propositions-as-types" paradigm to identify some types of the 
> system
> with mathematical statements and typing rules with axioms of the logic. In
> particular, the logic provided by CIC is a higher-order logic.
>
> > I know that ZFC has
> > been implemented in Coq.
>
> I would say that implementing ZFC in Coq serves a different purpose. If you 
> are
> interested in expressing proofs in set theory, it is probably better to use a
> system like Mizar (*) from the beginning.
>
> (*) https://en.wikipedia.org/wiki/Mizar_system
>
> > What I am currently unclear about is
> > precisely which axioms were used to prove Feit-Thompson in Coq;
>
> It is not easy to provide a short answer, as in type theory, the frontier
> between logic and language is blurred. Let me try, may be others on this list
> will improve my first stab: it uses the standard rules of higher order logic, 
> in
> its constructive form where no excluded middle or double-negation elimination 
> is
> available. Moreover, it uses the axioms governing the inductive types of CIC :
> for instance the user is allowed at will to introduce an inductive type called
> for instance, nat, introduced as a new type constant, and the definition of 
> this
> type also introduces new constants (say O, with arity 0 and S, with arity 1) 
> in
> the language, plus an "axiom" which asserts that the inhabitants of nat are 
> the
> smallest collection of terms generated by O and S. This axiom would in fact 
> be a
> statement of the recurrence principle on natural numbers.
>
> > my
> > current lack of understanding is such that I am currently still
> > confused about what role the law of the excluded middle plays.
>
> The law of excluded middle (EM) is not necessary for this proof. EM is not
> needed for instance to reason by case analysis on the equality of two 
> arbitrary
> natural numbers, because there is an effective way to compare two natural
> numbers. There is no need for EM either to reason by case analysis on the
> primality of a natural number, because there exist effective, complete,
> primality tests. Of course, when working in a constructive framework demands
> implementing these effective procedure, and proving formally their 
> correctness,
> before being allowed to use these case analyses in proofs. But this is what is
> actually done in the formal proof of the Feit-Thompson theorem.
>
> In fact, you can even reason constructively by case analysis on a first order
> statement, provided that it belongs to a first order theory which is 
> decidable.
> The logical language of Coq is expressive enough for the purpose of stating 
> this
> nature of theorems. For instance, we provided formal proofs for the 
> decidability
> of the theories of real closed fields and algebraically closed fields (and of
> course finite ones).  In particular, we can reason by case analysis on a
> first-order statement of the first-order theory of the fields of (complex or
> real) algebraic numbers. This nature of decidability result is used at least 
> in
> one place in representation theory, for the definition of socles.
>
> The character theory and complex representation part of the proof is thus
> formalized by replacing the field of complex numbers by the field of algebraic
> complex numbers, which is harmless in this case, and removes the need for EM.
> Moreover algebraic complex numbers form a countable type, which thus has a
> choice principle.
>
> > ... I suspect that the statement is _not_ "the
> > proof was verified in ZFC",
>
> Indeed, it is not.
>
> > however this might well be a consequence
> > of what was actually done; I suspect it was verified in a weaker axiom
> > system.
>
> I would say that the fragment of CIC required by the proof is definitively
> weaker than ZCF, although I do not know how this could be checked by 
> mechanical
> means.
>
> assia
>
> > Kevin
> >
> > On 14 June 2017 at 15:05, Emilio Jesús Gallego Arias 
> > <>
> >  wrote:
> > > Hi Kevin,
> > >
> > > [addressing this to the ssreflect list where the true experts on the
> > > proof can see it]
> > >
> > > Kevin Buzzard 
> > > <>
> > >  writes:
> > >
> > > > I have the current ssreflect installed and it works fine for me in Coq
> > > > 8.6 too. On reflection I think that my question is perhaps for the
> > > > maintainers of the Feit-Thompson proof. It had not occurred to me that
> > > > one might need to maintain a proof!
> > >
> > > I am not sure if you are referring to the proof in the old directory,
> > > but note that the proof is maintained (and works for me) in the github
> > > repository I pointed to:
> > >
> > > https://github.com/math-comp/math-comp/blob/master/mathcomp/odd_order/stripped_odd_order_theorem.v
> > >
> > > That is to say, I think that if you use Coq 8.6 you should not rely on
> > > the original published file.
> > >
> > > E.

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