The Coq mailing list

[Jean Goubault-Larrecq <Jean.Goubault AT dyade.fr>]

    Salut David,
David Monniaux wrote:

> I have a (maybe) naive question: while
> (X: Set) (P: X->bool) ~(x: X) (P x)=false -> (EX x: X | (P x)=true)
> is obviously false (without a classical axiom), is it possible to prove it
> for X=nat ?

    J'ai l'impression que non: ce que dit H : ~(x: nat) (P x)=false, c'est 
qu'il

n'y a pas de preuve de (x: nat) (P x)=false.  Si tu prends une interpretation
de style realisabilite (a la Kleene) de ce dernier, ou les "preuves" d'une
formule sont des entiers (et ou on dit qu'un entier n realise, plutot qu'il
ne prouve la formule, et ou n realise F -> G si n est le code d'une machine
de Turing qui envoie tout m realisant F vers un entier realisant G, etc.), 
alors

un realiseur de (x: nat) (P x)=false est un code n de machine de Turing
qui envoie chaque entier x vers un entier realisant (P x)=false.
    Ce que dit donc H dans cette interpretation, c'est que le probleme
de savoir si (P x)=false n'est pas recursif en x: il n'y a pas de machine
de Turing de code n demande.  A partir de cette hypothese, il semble clair
qu'on aura du mal a deduire (EX x: nat | (P x)=true), qui lui dit que
l'ensemble des x tels que (P  x)=true est recursivement enumerable.
    Il suffit donc de prendre pour l'ensemble E des x tels que (P  x)=true
un ensemble non recursivement enumerable: son complementaire,
qui est l'ensemble des x tels que (P x)=false, n'est pas co-r.e.,
donc en particular pas recursif.  Ceci infirme alors ta proposition.
    Pour E, il suffit de prendre le complementaire du "halting set" K usuel
(l'ensemble des codes x des entiers tels que U(x) termine, ou
U est une machine de Turing universelle donnee), ce que je te laisse
faire...

    Si j'ai dit des imbecillites, pardonnez-moi d'avance...

    -- Jean.