The Coq mailing list

[Bas Spitters <B.Spitters AT cs.ru.nl>]

Dear Pierre,

How about the following argument?

Consider the set omega +1, that is, we consider the natural numbers and add a 
top element infinity. Now given a code e of a Turing machine we consider the 
subset:
{n: the Turing machine e stop after n steps on input e}+{infinity}
This set is clearly inhabited (non-empty) and recursive. However, suppose 
that 
we could compute the least element of each such set, then we can solve the 
halting problem.

Best,

Bas

On Sunday 01 May 2005 15:34, Pierre Casteran wrote:
>  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