Publicité
+ Répondre à la discussion
Page 9 sur 9 PremièrePremière ... 56789
Affichage des résultats 161 à 165 sur 165
  1. #161
    Membre confirmé Avatar de Steki-kun
    Profil pro
    Inscrit en
    janvier 2005
    Messages
    222
    Détails du profil
    Informations personnelles :
    Âge : 31
    Localisation : France, Paris (Île de France)

    Informations forums :
    Inscription : janvier 2005
    Messages : 222
    Points : 255
    Points
    255

    Par défaut

    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
    I'm the kind of guy that until it happens, I won't worry about it. - R.H. RoY05, MVP06

  2. #162
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    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.

  3. #163
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    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.

  4. #164
    Nouveau Membre du Club
    Inscrit en
    janvier 2007
    Messages
    64
    Détails du profil
    Informations personnelles :
    Âge : 35

    Informations forums :
    Inscription : janvier 2007
    Messages : 64
    Points : 39
    Points
    39

    Par défaut

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

  5. #165
    Membre éclairé

    Inscrit en
    août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 64

    Informations forums :
    Inscription : août 2005
    Messages : 417
    Points : 330
    Points
    330

    Par défaut

    Citation Envoyé par kaukau Voir le message
    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.

Liens sociaux

Règles de messages

  • Vous ne pouvez pas créer de nouvelles discussions
  • Vous ne pouvez pas envoyer des réponses
  • Vous ne pouvez pas envoyer des pièces jointes
  • Vous ne pouvez pas modifier vos messages
  •