{"id":2012,"date":"2023-06-29T17:47:33","date_gmt":"2023-06-29T09:47:33","guid":{"rendered":"https:\/\/dylech30th.me\/?p=2012"},"modified":"2023-06-29T23:51:55","modified_gmt":"2023-06-29T15:51:55","slug":"laxiome-du-choix-dans-le-domaine-de-la-theorie-intuitionniste-des-types","status":"publish","type":"post","link":"https:\/\/sora.ink\/archives\/2012","title":{"rendered":"L’axiome du choix, dans le domaine de la th\u00e9orie intuitionniste des types"},"content":{"rendered":"

\u2003\u2003L'axiome du choix, c'est un axiome qui signifie qu'il y a une fonction pour choisir un \u00e9l\u00e9ment d'une collection infinie des ensembles. Il est critiqu\u00e9 par beaucoup de constrictivistes car que l'existence de cette fonction est non-constructif, de telle fonction est suppos\u00e9 exister sans une construction explicite. Cepandent, ce axiome devient raisonnable quand il est formul\u00e9 dans la th\u00e9orie intuitionniste des types, mais avec une forme diff\u00e9rente. Pour expliquer comment est-il formul\u00e9, nous devons d'abord expliquer la formulation diff\u00e9rente.
\n\u2003\u2003Dans la th\u00e9orie intuitionniste des types (dans le texte suivant nous allons l'abr\u00e9geons en \u00ab ITT (De son nom en anglais, Intuitionistic Type Theory<\/em>)\u00bb), l'axiome du choix (dans le texte suivant nous allons l'abr\u00e9geons en \u00ab \\mathsf{AC}<\/span> \u00bb (De son nom en anglais, Axiom of Choice<\/em>) est formul\u00e9 en terme des relations, comme:<\/p>\n

D\u00e9finition: \\textsf{AC2}<\/span>:<\/strong>
\n\u2003\u2003Supposons qu'il y ait1<\/a><\/sup> une relation binaire R(x, y)<\/span> o\u00f9 x\\in A<\/span> et y\\in B<\/span>, alors pour chaque x\\in A<\/span>, il y a un y\\in B<\/span> tel que R(x, y)<\/span> ou (x, y)\\in R<\/span> implique qu'il y ait2<\/a><\/sup> une fonction de choix f:A\\rightarrow B<\/span> telle que pour chaque z\\in A<\/span>, nous ayons R(z, f(z))<\/span>. Formellement, il est \u00e9crit:<\/em><\/p>\n

(\\forall x\\in A.\\exists y\\in B. R(x, y))\\rightarrow (\\exists f:A\\rightarrow B. \\forall z\\in A. R(z, f(z))) \\tag{\\textsf{AC2}}\n<\/div>\n

Ce qui est \u00e9quivalent \u00e0:<\/p>\n

D\u00e9finition: \\textsf{AC2}<\/span>:<\/strong>
\n\u2003\u2003Chaque relation correspond \u00e0 une fonction f<\/span> telle que \\text{dom}(f)=R<\/span>.<\/em><\/p>\n

\u2003\u2003Maintenant nous devions prouver que \\textsf{AC2}<\/span> est \u00e9quivalent \u00e0 la formulation originale, ce qui est \\textsf{AC}<\/span>:<\/p>\n

D\u00e9finition \\textsf{AC}:<\/span><\/strong>
\n\u2003\u2003Pour chaque collection X<\/span> des ensembles non vides, il y a une fonction f<\/span> qui choisit un \u00e9l\u00e9ment x\\in A<\/span> pour chaque ensemble A\\in X<\/span>. Formellement, il est \u00e9crit:<\/em><\/p>\n

\\forall X.(\\empty\\notin X\\rightarrow \\exists f:X\\rightarrow \\bigcup_{X}\\ \\land\\ \\forall A\\in X. f(A)\\in A)\\tag{\\textsf{AC}}\n<\/div>\n

Ce qui est \u00e9quivalent \u00e0:<\/p>\n

D\u00e9finition \\textsf{AC}:<\/span><\/strong>
\n\u2003\u2003Le produit d'une collection des ensembles non vides est non vide.<\/em><\/p>\n

\u2003\u2003Pour prouver \\textsf{AC=AC2}<\/span>, d'abord, pour la direction (\\rightarrow<\/span>), soit \\mathcal{P_{\\backslash\\empty}}(S)<\/span> l'ensemble puissance de S<\/span> sans \\empty<\/span>, supposons que \\textsf{AC}<\/span> tienne, ce qui implique qu'il y a une fonction de choix pour chaque ensemble X<\/span>, \u00e0 savoir la fonction f:\\mathcal{P_{\\backslash\\empty}}(X)\\rightarrow X<\/span> telle que f(A)\\in A<\/span> pour chaque A\\in X<\/span>; maintenant soit R<\/span> une relation binaire sur A<\/span> et B<\/span>, soit f_B<\/span> la fonction de choix de B<\/span>, soit f_A<\/span> une fonction d\u00e9fini comme f_A(a)=f_B(\\lbrace b\\ |\\ R(a, b)\\rbrace)<\/span>, donc c'est \u00e9vident que \\text{dom}(f_A)=\\text{dom}(R)<\/span>: Si (a, b)\\in R<\/span>, alors f_B({b})<\/span> choisit b<\/span> et f_A(a)=b<\/span>, ce qui signifie que (a, b)\\in f_A<\/span>; si (a, b)\\in f_A<\/span>, alors f_A(a)=f_B(\\lbrace b\\ |\\ R(a, b)\\rbrace)=b<\/span>, donc par d\u00e9finition de f_B<\/span>, nous avons (a, b)\\in R<\/span>. Ensuite, pour la direction (\\leftarrow<\/span>), soit R<\/span> une relation binaire sur \\mathcal{P_{\\backslash\\empty}}(X)<\/span> et X<\/span> telle que R(a, b)<\/span> iff b\\in a<\/span>, alors la fonction f_R<\/span> ce qui a le m\u00eame domaine que R<\/span> est une fonction de choix pour X<\/span>: f_R(a)=b<\/span> o\u00f9 a\\in\\mathcal{P_{\\backslash\\empty}}(X)<\/span> implique b\\in a<\/span>.
\n\u2003\u2003Il est une v\u00e9rit\u00e9 bien connue que tout les deux \\textsf{AC}<\/span> et \\textsf{AC2}<\/span> n'est pas prouvable dans la logique intuitionniste, car il n'y a pas de m\u00e9thode de construire de telles fonctions, une raison importante \u00e0 cela est que nous n'avons pas rien pour \"construire\" ces fonctions: Pour prouver \\textsf{AC}<\/span>, nous devions fournir sa preuve, mais pour fournir les preuves, vous devez d'abord avoir des choses pour les construire, n\u00e9anmoins dans la logique intuitionniste des pr\u00e9dicats, il n'y a pas de tels choses, et c'est ici que la th\u00e9orie des types entre le terrain.<\/p>\n

Une th\u00e9orie qui est assez puissante pour prouver les propri\u00e9t\u00e9s de elle-m\u00eame<\/h3>\n

\u2003\u2003La th\u00e9orie des types est une th\u00e9orie plut\u00f4t sp\u00e9ciale, quand nous parlons des syst\u00e8mes formelles, il implique souvent deux th\u00e9ories: la th\u00e9orie des objets et la m\u00e9tath\u00e9orie, la permi\u00e8re est la th\u00e9orie \u00e0 propos des objets math\u00e9matiques qui sont recherch\u00e9, par exemple la th\u00e9orie des nombres r\u00e9els, la th\u00e9orie des groupes, et cetera<\/em>; la derni\u00e8re est plut\u00f4t int\u00e9ressante, en math\u00e9matiques, nous ne consid\u00e9rons pas souvent la th\u00e9orie lui-m\u00eame quand nous recherchons sur les objets comme les nombres r\u00e9els, nous ne prouvons jamais la correction des m\u00e9thode que nous utilisons, mais les m\u00e9thodes que nous utilisons sont peut-\u00eatre incorrects, nous avons besoin des m\u00e9thodes pour justifier la correction des th\u00e9ories elles-m\u00eames. Et voil\u00e0, nous avons les m\u00e9tath\u00e9ories, celles qui sont th\u00e9ories qui recherchent d'autres th\u00e9ories, cependant il y a un probl\u00e8me: si nous utilisons les m\u00e9tath\u00e9ories pour justifier les th\u00e9ories des objets, alors que devons-nous utiliser pour justifier les m\u00e9tath\u00e9ories? Et justifier les m\u00e9ta-m\u00e9tath\u00e9ories ad infinitum<\/em>? En fait, la correction de telles th\u00e9ories sont prouv\u00e9 en utilisant les fondements des math\u00e9matics<\/strong>, ceux qui sont les th\u00e9ories qui sont assez puissante pour prouver les propri\u00e9t\u00e9s de elles-m\u00eames, et les math\u00e9matiques sont interne \u00e0<\/a><\/em> elles<\/strong>, pour que nous n'avons pas besion des m\u00e9tath\u00e9ories sur m\u00e9tath\u00e9ories, car les objets sont d\u00e9fini dans cette th\u00e9orie, et cette th\u00e9orie est capable de raisonner sur elle-m\u00eame, de telle th\u00e9orie est \u00e0 la fois:<\/p>\n

    \n
  1. Les objets.<\/li>\n
  2. La th\u00e9orie des objets<\/li>\n
  3. La m\u00e9tath\u00e9orie de la th\u00e9orie des objets<\/li>\n
  4. La m\u00e9tath\u00e9orie de sa propre.<\/li>\n<\/ol>\n

    \u2003\u2003Ces ensemble impliquent que toutes les pr\u00e9positions, qu'elles soient3<\/a><\/sup> des objets, des th\u00e9ories, ou d'elle-m\u00eame, sont tous prouvable dans elle-m\u00eame. De telles th\u00e9ories pouvons \u00e0 la fois repr\u00e9senter les pr\u00e9positions et leurs preuves. Et la th\u00e9orie intuitionniste des types est une telle th\u00e9orie.<\/p>\n

    \n Pour clarifier, bien que la logique du premier ordre<\/em>, abr\u00e9ge en FOL<\/em>, de son nom en anglais: First-Order Logic, soit souvent utilis\u00e9 pour formuler les syst\u00e8mes axiomatiques, comme les syst\u00e8mes pour l'arithm\u00e9tique, il ne consid\u00e9r\u00e9 pas une fondement des math\u00e9matics: il n'y a aucun objets math\u00e9matiques qui sont interne \u00e0 elle.\n<\/p><\/blockquote>\n

    L'axiome du choix dans la th\u00e9orie intuitionniste des types<\/h3>\n

    \u2003\u2003Dans la ITT, il n'y a pas que des preuves, mais \u00e9galement les objets des preuves ceux qui sont les \\lambda<\/span>-termes, et prouver une pr\u00e9position revient \u00e04<\/a><\/sup> trouver un \\lambda<\/span>-terme du type correspondant, quant \u00e0 \\textsf{AC2}<\/span>, dans le symbolisme de la ITT c'est \u00e9crit:<\/p>\n

    (\\Pi \\textcolor{pink}x:\\textcolor{crimson}{A}.\\Sigma \\textcolor{pink}y: \\textcolor{crimson}{B(x)}. \\textcolor{turquoise}{R(x, y)})\\rightarrow (\\Sigma \\textcolor{pink}f:\\textcolor{crimson}{\\Pi x: A. B(x)}.\\Pi \\textcolor{pink}z:\\textcolor{crimson}A.\\textcolor{turquoise}{R(z, \\mathsf{Ap}(f, z))})\n<\/div>\n

    Pour \u00e9viter (avoid<\/em>) des confisions, nous utilisons les couleurs diff\u00e9rentes pour souligner5<\/a><\/sup> les parties diff\u00e9rentes dans l'expression: le rose<\/span> est binders (en anglais)<\/em>, la pourpre<\/span> est types des binders<\/em>, et la turquoise<\/span> est les expressions. \\Pi<\/span> represente \\Pi<\/span>-Types<\/a> et correspond \u00e0 \\forall<\/span> par l'isomorphism de Curry-Howard<\/em>, \\Sigma<\/span> represente \\Sigma<\/span>-Types<\/a> et correspond \u00e0 \\exists<\/span> par l'isomorphisme, remarquons que dans notre symbolisme, au lieu de \\Sigma y: B<\/span>, nous \u00e9crivons \\Sigma y: B(x)<\/span> o\u00f9 x: A<\/span>, cependant c'est d'accord pour B<\/span> pour d\u00e9pendre de x<\/span> ou non. De plus, nous d\u00e9finissons \\mathsf{Ap}(f, x)<\/span> \u00eatre f(x)<\/span>. Pour prouver ce type ou cette pr\u00e9position, nous devions trouver le \\lambda<\/span>-terme correspondant dans les marches6<\/a><\/sup> suivantes:<\/p>\n

      \n
    1. Supposons que nous ayons:\n
        \n
      1. La pr\u00e9misse 1: \\Pi \\textcolor{pink}x:\\textcolor{crimson}{A}.\\Sigma \\textcolor{pink}y: \\textcolor{crimson}{B(x)}. \\textcolor{turquoise}{R(x, y)}<\/span>, id est<\/em>, il y a \\phi<\/span> avec le type \\Pi \\textcolor{pink}x:\\textcolor{crimson}{A}.\\Sigma \\textcolor{pink}y: \\textcolor{crimson}{B(x)}. \\textcolor{turquoise}{R(x, y)}<\/span><\/li>\n
      2. La pr\u00e9misse 2: x\\in A<\/span><\/li>\n<\/ol>\n<\/li>\n
      3. Par \\Pi<\/span>-\u00c9limination<\/em>, nous avons \\mathsf{Ap}(\\phi, x): \\Sigma \\textcolor{pink}y:\\textcolor{crimson}{B(x)}.\\textcolor{turquoise}{R(x, y)}<\/span><\/p>\n<\/li>\n
      4. \n

        Par la cons\u00e9quence directe de \\Sigma<\/span>-\u00c9limination, nous avons la fonction de la projection droite \\mathsf{p}<\/span> et la projection gauche \\mathsf{q}<\/span>. Soit \\mathsf{Ap}(\\phi, x): \\Sigma \\textcolor{pink}y:\\textcolor{crimson}{B(x)}.\\textcolor{turquoise}{R(x, y)}<\/span>, appliquons \\mathsf{p}<\/span> nous obtenons \\mathsf{p}(\\mathsf{Ap}(\\phi, x)): \\textcolor{crimson}{B(x)}<\/span> et appliquons \\mathsf{q}<\/span> nous obtenons \\mathsf{q}(\\mathsf{Ap}(\\phi, x)): \\textcolor{turquoise}{R(x, \\mathsf{p}(\\mathsf{Ap}(\\phi, x)))}<\/span> par la d\u00e9finition de \\mathsf{q}<\/span>.<\/p>\n

        \n La raison de telle cons\u00e9quence est que par la BHK-Interpr\u00e9tation<\/em> et l'isomorphisme de Curry-Howard<\/em>, les \u00e9l\u00e9ments des \\Sigma<\/span>-types \\Sigma x: A. B(x)<\/span> sont les paires ordon\u00e9es<\/em> (a, b)<\/span> telles que B(a)<\/span> tienne, donc supposons que nous ayons \\omega:\\Sigma x:A.B(x)<\/span>, alors la projection naturelle droite \\mathsf{p}(\\omega)=\\mathsf{p}((a, b))<\/span> est d\u00e9fini \u00eatre7<\/a><\/sup> a<\/span>; et la projection naturelle gauche \\mathsf{q}(\\omega)=\\mathsf{q}((a, b))<\/span> est d\u00e9fini \u00eatre B[x\\mapsto \\mathsf{p}(\\omega)]<\/span>.\n<\/p><\/blockquote>\n<\/li>\n

      5. Par \\Pi<\/span>-Introduction<\/em> (\\lambda<\/span>-Abstraction<\/em>) sur x<\/span>, nous avons \\lambda z: A.\\mathsf{p}(\\mathsf{Ap}(\\phi, z)): \\textcolor{crimson}{\\Pi z:A. B(x)}<\/span>. Ce marche est n\u00e9cessaire pour d\u00e9charger la pr\u00e9misse 2.<\/p>\n<\/li>\n
      6. Par \\Pi<\/span>-\u00c9galit\u00e9<\/em> (\\eta<\/span>-Expansion<\/em>), nous avons: \\mathsf{Ap}(\\lambda z: A.\\mathsf{p}(\\mathsf{Ap}(\\phi, z)), z): \\textcolor{crimson}{B(x)}<\/span>, ce qui est \u00e9quivalent \u00e0 \\mathsf{p}(\\mathsf{Ap}(\\phi, z)):\\textcolor{crimson}{B(x)}<\/span>.<\/li>\n
      7. Alors nous avons R(x, \\mathsf{Ap}(\\lambda z: A.\\mathsf{p}(\\mathsf{Ap}(\\phi, z)), z))=R(x, \\mathsf{p}(\\mathsf{Ap}(\\phi, z)))<\/span><\/li>\n
      8. Ceci implique que \\mathsf{q}(\\mathsf{Ap}(\\phi, z)): \\textcolor{turquoise}{R(x, \\mathsf{Ap}(\\lambda z: A.\\mathsf{p}(\\mathsf{Ap}(\\phi, z)), z))}<\/span><\/li>\n
      9. Donc \\lambda z: A.\\mathsf{q}(\\mathsf{Ap}(\\phi, z)): \\Pi z:\\textcolor{crimson}A.\\textcolor{turquoise}{R(x, \\mathsf{Ap}(\\lambda z: A.\\mathsf{p}(\\mathsf{Ap}(\\phi, z)), z))}<\/span><\/li>\n
      10. Combinons 4. et 8. Par les associons ensemble, nous avons: (\\lambda z: A.\\mathsf{p}(\\mathsf{Ap}(\\phi, z)),\\lambda z: A.\\mathsf{q}(\\mathsf{Ap}(\\phi, z))): \\Sigma \\textcolor{pink}\\phi:\\textcolor{crimson}{\\Pi z: A. B(x)}.\\Pi z:\\textcolor{crimson}A.\\textcolor{turquoise}{R(x, \\mathsf{Ap}(\\lambda z: A.\\mathsf{p}(\\mathsf{Ap}(\\phi, z)), z))}=\\Sigma \\textcolor{pink}f:\\textcolor{crimson}{\\Pi z: A. B(x)}.\\Pi \\textcolor{pink}z:\\textcolor{crimson}A.\\textcolor{turquoise}{R(z, \\mathsf{Ap}(f, z))}<\/span>, remarquons que \\phi<\/span> est remplac\u00e9 par f<\/span>.<\/li>\n
      11. Abstracyons \\phi<\/span> en f<\/span>, nous avons:\\lambda f: \\Pi x:{A}.\\Sigma y: {B(x)}. {R(x, y)}(\\lambda z: A.\\mathsf{p}(\\mathsf{Ap}(f, z)),\\lambda z: A.\\mathsf{q}(\\mathsf{Ap}(f, z))): (\\Pi \\textcolor{pink}x:\\textcolor{crimson}{A}.\\Sigma \\textcolor{pink}y: \\textcolor{crimson}{B(x)}. \\textcolor{turquoise}{R(x, y)})\\rightarrow (\\Sigma \\textcolor{pink}f:\\textcolor{crimson}{\\Pi x: A. B(x)}.\\Pi \\textcolor{pink}z:\\textcolor{crimson}A.\\textcolor{turquoise}{R(z, \\mathsf{Ap}(f, z))})<\/span>. QED.<\/li>\n<\/ol>\n
        \n
        \n
          \n
        1. \n

          supposons que<\/em> follows subjunctive mood ↩︎<\/a>\n<\/li>\n

        2. \ntel que<\/em> follows subjunctive mood when it means \"such that\" ↩︎<\/a>\n<\/li>\n
        3. \nis this grammatically correct? ↩︎<\/a>\n<\/li>\n
        4. \nrevenir \u00e0<\/em>: amounts to ↩︎<\/a>\n<\/li>\n
        5. \nsouligner<\/em>: to emphasize ↩︎<\/a>\n<\/li>\n
        6. \nmarche<\/em>: steps ↩︎<\/a>\n<\/li>\n
        7. \nou d\u00e9fini comme \u00e9tant<\/em>, moins formelle ↩︎<\/a>\n<\/li>\n<\/ol>\n<\/div>\n","protected":false},"excerpt":{"rendered":"

          \u2003\u2003L’axiome du choix, c’est un axiome qui signifie qu’il y a","protected":false},"author":1,"featured_media":2048,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"kia_subtitle":"","footnotes":""},"categories":[61],"tags":[29,78,56,28],"class_list":["post-2012","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-61","tag-29","tag-78","tag-56","tag-28"],"_links":{"self":[{"href":"https:\/\/sora.ink\/wp-json\/wp\/v2\/posts\/2012","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/sora.ink\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/sora.ink\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/sora.ink\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/sora.ink\/wp-json\/wp\/v2\/comments?post=2012"}],"version-history":[{"count":34,"href":"https:\/\/sora.ink\/wp-json\/wp\/v2\/posts\/2012\/revisions"}],"predecessor-version":[{"id":2047,"href":"https:\/\/sora.ink\/wp-json\/wp\/v2\/posts\/2012\/revisions\/2047"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/sora.ink\/wp-json\/wp\/v2\/media\/2048"}],"wp:attachment":[{"href":"https:\/\/sora.ink\/wp-json\/wp\/v2\/media?parent=2012"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/sora.ink\/wp-json\/wp\/v2\/categories?post=2012"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/sora.ink\/wp-json\/wp\/v2\/tags?post=2012"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}