Recherche:

Vrai et Faux étant eux-même des propositions, on peut même dire qu'il existe un unique booléen b tel que [x > Vrai, y > Faux]b. (pas besoin du =Vrai).

Maintenant, ça va pas te donner la fonction...

on en a bien un (et un seul) c'est le quantificateur existentiel. Rappelle toi qu'on a défini tous les autres opérateurs, (et le = aussi, ce qui répond à ta question) en termes du quantificateur...

Ben ce terme est de type ?q:O. (!1x:Boole.q) => Boole ce qui correspond pas vraiment à la question posée :) Ici tu te donnes une preuve de !1x:Boole.q pour pouvoir appliquer l'opérateur de...

Je peux difficilement te dire comment l'utiliser dans la question 26 sans te donner la réponse à la question 26. Cependant, je peux répondre à tes premières questions ce qui te donne comment on...

Désolé :) Je trouve qu'ils se complètent bien en tout cas.


Je vous le concède mais vous pinaillez un peu ;) Le but était de donner une intuition à kaukau plus qu'autre chose. Pour être exact, je...

Salut ta confusion vient du fait que tu n'as pas compris ce qu'est un type somme en maths. Tu connais le produit cartésien de deux ensembles A et B, qui consiste à prendre l'ensemble des couplets...

Oui c'est exactement ça :-)

Sans donner la réponse à la question proprement dite, la réponse à votre sous question est que ce terme c n'est pas de type W(E[b/x]) puisqu'un terme de preuve de W(E[b/x]) s'obtiendra ici par...

Question 18:
La question 18 propose de prouver ?p:O.?q:O.~(p|q) => (~p & ~q). Voilà le terme que je propose :

On commence donc par considérer deux propositions p et q, ainsi qu'une preuve H du...

Il se trouve qu'on a posté exactement en même temps sans pourtant s'être mis d'accord avec le DrTopos mais c'est bien, ça me fait moins de commentaires à faire sur les questions 17 et 18 :)
...

Bon je vais reprendre mes réponses des questions 15 à 19 en détaillant le pourquoi du comment, histoire que ceux d'entre vous qui essayent de suivre puissent comprendre de quoi il retourne :)
...

Au départ le CoC (Calcul des Constructions) c'est en gros du lambda-calcul typé d'ordre supérieur où les types sont des valeurs de première classe. Par rapport à MartinLöf la différence c'est en...

Pour répondre à certaines de vos interrogations Dr T., l'axiome de Proof-irrelevance, ainsi que beaucoup d'autres qui sont parfois plus forts (ie qui l'impliquent) comme l'extensionnalité et le tiers...

Ben en ce qui concerne le Faux, les deux présentations sont strictement équivalentes : en fait forall P.P correspond exactement au schéma d'induction associé à un inductif sans constructeur....

Pour prouver ~~q, il faut prouver que ~q est absurde, ou encore que ~q => Faux.
Or, dans le formalisme du DrTopos (et pas seulement), Faux est en fait défini comme "pour tout P, P". Autrement dit,...

(q:O) |-> ((urd : W(q)) -> (abs : W(~q)) -> (p: O) -> (abs urd) p).

Avec le terme Coq correspondant :


Theorem Q15 : forall Q : Prop, Q -> ~~Q.
Proof.
exact (fun Q urd abs => abs urd)....

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...