The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hello,

 I suspect thet the statement "Every (recursive, non empty) subset
of a well ordered set has a least element" cannot be intuitionnistically
proven. All the proofs I know use classically the impossibility of
building an infinite decreasing sequence. On the other side, I couldn't
find any algorithm for finding such an element, starting from the
non-emptyness witness.

 Is that true?
 It is is, where can I find a formal argument (e.g. reduction to a
 known problem) ?

Thenks in advance,

Pierre


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.