The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

La reponse de Jean est correcte. Le principe que tu cherches a prouver
est connu sous le nom de principe de Markov. Il n'est pas realisable
en realisabilite modifiee pour la raison invoquee par Jean. Donc il
n'est pas prouvable dans le calcul des constructions.

Il est realisable, si on utilise une realisabilite generale ou on peut
coder la fonction de recherche sequentielle, et si on suppose que le
meme principe est vrai.
ie Markov |- P 
=> il existe un programme clos p tel que Markov |- ``p realise P''

Dans Coq, ce qu'il est possible de montrer est 
          (Ex [x:nat] P x= true)  -> {x:nat | P(x)=true}
C'est-a-dire de passer d'une vision non-informative de l'existence (ou
on ne calcule pas le temoin) a une vision informative ou on le calcule.
Pour cela on definit un ordre 
        R(y,x) ssi y>x et (n)n<=y => P(n)=false
le fait qu'il existe n tel que P(n)=true entraine que R est bien fonde
et on calcule le plus petit n en partant de 0.

Si le probleme est de raisonner de maniere classique sur un fragment
de la logique, alors il y a differentes possibilites a explorer.
Ajouter brutalement l'axiome de logique classique au niveau de Prop ou
bien utiliser des codages des connecteurs internes.

Christine.

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, URA 410 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 55 70       fax : (+33) (0)1 39 63 56 84
  Tatoo tel : 06 04 24 44 75 
   message numerique +1(pas urgent)-3(tres urgent) ou * + message vocal