Bon, alors, je suis de retour sur developpez.net après de longs mois d'absence et je vois qu'il s'y passe des trucs très intéressants :P Malheureusement, j'ai pas eu le temps de lire les 6 pages de posts, je me suis contenté de la syntaxe donnée dans le post #2, donc j'espère que vous ne m'en voudrez pas si je suis à côté de la plaque.
Alors, la réponse courte : ce terme est bien typé et c'est une preuve de !x:T.?y:U.E => ?y:U.!x:T.E, en d'autres termes la permutation des deux quantificateurs.
La réponse longue : on suppose une preuve p du fait qu'il existe un x de type T tel que pour tout y de type U, E(implictement de x,y) est vrai. On suppose également un élément y de type U. Avec tout ça, on sent bien qu'on va montrer qu'il existe un x tel que E est vrai (avec le y supposé, qui n'est plus libre, donc je devrais écrire E[y/y] en toute rigueur, mais bon...). En d'autre termes, on va construire une preuve de !x:T.E.
Alors en maths, c'est facile, on dirait. Ici on est en codage du second ordre, donc pour détruire un quantificateur existentiel !x:T.Q, on l'applique simplement à la propriété P que l'on veut établir, puis à une preuve de ?x:T.Q=>P. Autrement dit, on montre que n'importe quel x de type T vérifiant Q fait l'affaire pour montrer P.Citation:
D'après p, il existe x tel que pour tout y, E est vrai. En appliquant à notre y à nous, on a bien trouvé un x tel que E est vrai.
Ca se traduit bien par le fait que le terme de la question commence précisément par p(!x:T.E), donc par l'utilisation de l'hypothèse existentiellement quantifiée p pour établir !x:T.E. Là, pas besoin de comprendre le reste, on sait déjà que si le terme est bien typé il aura ce type là (ou tout du moins un suffixe commun, si jamais le machiavélique DrT. l'appliquait à son tour à une nouvelle proposition q, etc etc).
Mais vérifions quand même la suite :) On veut donc appliquer p(!x:T.E) à une preuve du fait que "pour tout x, si ce x est tel que E pour tout y, alors !x:T.E". Donc on prend un x:T, une preuve r du fait que ?y:U.E :
on note au passage qu'on utilise l'isomorphisme W(?y:U.E) ~~ (y:U) -> W(E). Il nous reste, armés de toutes ces hypothèses, à retourner une preuve du fait qu'il existe bien un x tel que E est vrai. Or, r(y) est une preuve de E, donc la paire de heyting <x,r(y)> relie précisément un élément x de type T et un "témoin" du fait que E(x) est vrai, et a en particulier le type voulu !x:T.E.Citation:
p(!x:T E)((x:T) |-> (r: (y:U) -> W(E)) |-> ...)
Voilà j'ai essayé d'être didactique comme ça si je me suis trompé on m'en voudra moins et merci à ceux qui auront lu jusqu'en bas :coucou: