The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

> It is certainly true, and I would also argue that the law of the excluded
> middle is completely embedded in "Fields Medal mathematics". The bright
> young mathematicians look up to the Fields Medallists, and are taught on
> day one that Prop = bool and hence that the law of the excluded middle is
> an axiom. This will be an extremely hard cycle to break. I agree that young
> people are more and more coming into mathematics departments with a
> knowledge of programming and this is what I want to tap into, but rejecting
> LEM would not be a suggestion which would be taken seriously by anybody in
> our department. In fact I do not know of a mathematics department anywhere
> in the world where undergraduates are not told that LEM is true right from
> the start, and most lecturers. It would be interesting to find examples of
> International Mathematical Olympiad questions which would be unsolvable
> without LEM.

I have learned to consider LEM with suspicion, but at the same time, LEM
doesn't need to be an axiom.  You simply need to define

    classical-or A B = ¬(¬A ∧ ¬B)

and then you can easily prove

    LEM : (A : Type) -> classical-or A (¬ A)

and this LEM is much more honest, IMO (in the sense that it doesn't say
"it's true" but "it's not inconsistent").

It's not as convenient to use, admittedly, but you could argue that it's
"a small matter of tooling".


        Stefan