Discussion :

[Steki-kun]

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 voulue puisque ce booléen c'est forcément *+One (Vrai est toujours vrai, Faux ne l'est pas). C'est d'ailleurs la réponse à la question [je sais plus combien] : en l'absence du tiers-exclu, une fonction de O vers Boole va être constante (soit tout le temps Bvrai, soit tout le temps Bfalse). A toi d'adapter cet exemple en présence du tiers-exclu pour en faire la fonction voulue

[DrTopos]

Je vois que toute cette histoire n'a pas de secret pour Steki-kun. En particulier sa réponse à la question 27 est exacte: les fonctions constructives de O vers Boole sont toutes constantes. Ce résultat est connu sous le nom de ``principe d'uniformité de Troelstra''. Le démontrer n'est pas simple et peut se faire par les méthodes de la théorie de la démonstration (normalisation forte à la Tait), mais aussi par d'autres méthodes plus dans l'esprit topos, comme celles utilisées dans le livre de Lambek et Scott ``Introduction to Higher Order Categorical Logic''.

Pour aider kaukau (et tous ceux qui cherchent mais qui ne se montrent pas, s'il en existe) à avancer dans la construction d'une fonction f de O vers Boole telle que f(Vrai) = BVrai et f(Faux) = BFaux, je propose une question moins difficile et résolvant une partie du problème.

D'abord quelques définitions (bien connues). Une fonction f de type T -> U est surjective s'il y a un témoin de l'énoncé ?y:U !x:T y=f(x). De même elle est injective s'il y a un témoin de l'énoncé ?x:T ?y:T f(x) = f(y) => x=y. Elle est bijective si elle est à la fois injective et surjective.

Question 28. Montrer que si f de type T -> U est bijective, alors elle a un inverse.

Il s'agit bien sûr de construire à partir de f et de témoins de sa surjectivité et de son injectivité, un terme g de type U -> T et des témoins des énoncés ?x:T g(f(x)) = x et ?y:U f(g(y)) = y. Je précise que la réponse à la question 28 est constructive (pas d'utilisation du tiers exclu), mais que l'utilisation de l'opérateur de description y est indispensable.

[DrTopos]

Je donne la réponse à la question (non numérotée) du produit dans la catégorie des entiers strictement positifs avec pour flèches de n vers m les couples (n,m) tels que n divise m.

Dans cette catégorie, il existe un seul produit de n et m, qui est le PGCD de n et m. En effet, notons p un tel produit (s'il existe). On doit avoir des projections canoniques p -> n et p -> m, ce qui signifie que p divise à la fois n et m et donc que p divise PGCD(n,m) Par ailleurs, on a aussi des flèches f:PGCD(n,m) -> n et g:PGCD(n,m) -> m, puisque le PGCD de n et m divise n et m. On a donc la flèche <f,g>:PGCD(n,m) -> p par définition du produit. Or cette dernière flèche nous dit que PGCD(n,m) divise p. On a donc p=PGCD(n,m).

Voilà. C'était juste pour s'amuser un peu. Il y a bien sûr des tas d'autres exemples, mais je préfère refermer cette parenthèse.

Je n'ai pas oublié que je dois aussi parler des sommes dans divers langages, mais je suis très occupé en ce moment.

[kaukau]

Je relance ce topic!
Dr Topos, tu nous avais promis une petite explication sur les sommes...

[DrTopos]

Je relance ce topic!
Dr Topos, tu nous avais promis une petite explication sur les sommes...

En effet. Je n'ai pas oublié. Je suis seulement très occupé en ce moment. Mais je vais m'y coller sans tarder, puisque tu désires relancer ce fil. A bientôt.