L'axiome du choix, c'est un axiome qui signifie qu'il y a une fonction pour choisir un élément d'une collection infinie des ensembles. Il est critiqué par beaucoup de constrictivistes car que l'existence de cette fonction est non-constructif, de telle fonction est supposé exister sans une construction explicite. Cepandent, ce axiome devient raisonnable quand il est formulé dans la théorie intuitionniste des types, mais avec une forme différente. Pour expliquer comment est-il formulé, nous devons d'abord expliquer la formulation différente.
  Dans la théorie intuitionniste des types (dans le texte suivant nous allons l'abrégeons en « ITT (De son nom en anglais, Intuitionistic Type Theory)»), l'axiome du choix (dans le texte suivant nous allons l'abrégeons en « \mathsf{AC} » (De son nom en anglais, Axiom of Choice) est formulé en terme des relations, comme:

Définition: \textsf{AC2}:
  Supposons qu'il y ait1 une relation binaire R(x, y) où x\in A et y\in B, alors pour chaque x\in A, il y a un y\in B tel que R(x, y) ou (x, y)\in R implique qu'il y ait2 une fonction de choix f:A\rightarrow B telle que pour chaque z\in A, nous ayons R(z, f(z)). Formellement, il est écrit:

(\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}}

Ce qui est équivalent à:

Définition: \textsf{AC2}:
  Chaque relation correspond à une fonction f telle que \text{dom}(f)=R.

  Maintenant nous devions prouver que \textsf{AC2} est équivalent à la formulation originale, ce qui est \textsf{AC}:

Définition \textsf{AC}:
  Pour chaque collection X des ensembles non vides, il y a une fonction f qui choisit un élément x\in A pour chaque ensemble A\in X. Formellement, il est écrit:

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

Ce qui est équivalent à:

Définition \textsf{AC}:
  Le produit d'une collection des ensembles non vides est non vide.

  Pour prouver \textsf{AC=AC2}, d'abord, pour la direction (\rightarrow), soit \mathcal{P_{\backslash\empty}}(S) l'ensemble puissance de S sans \empty, supposons que \textsf{AC} tienne, ce qui implique qu'il y a une fonction de choix pour chaque ensemble X, à savoir la fonction f:\mathcal{P_{\backslash\empty}}(X)\rightarrow X telle que f(A)\in A pour chaque A\in X; maintenant soit R une relation binaire sur A et B, soit f_B la fonction de choix de B, soit f_A une fonction défini comme f_A(a)=f_B(\lbrace b\ |\ R(a, b)\rbrace), donc c'est évident que \text{dom}(f_A)=\text{dom}(R): Si (a, b)\in R, alors f_B({b}) choisit b et f_A(a)=b, ce qui signifie que (a, b)\in f_A; si (a, b)\in f_A, alors f_A(a)=f_B(\lbrace b\ |\ R(a, b)\rbrace)=b, donc par définition de f_B, nous avons (a, b)\in R. Ensuite, pour la direction (\leftarrow), soit R une relation binaire sur \mathcal{P_{\backslash\empty}}(X) et X telle que R(a, b) iff b\in a, alors la fonction f_R ce qui a le même domaine que R est une fonction de choix pour X: f_R(a)=b où a\in\mathcal{P_{\backslash\empty}}(X) implique b\in a.
  Il est une vérité bien connue que tout les deux \textsf{AC} et \textsf{AC2} n'est pas prouvable dans la logique intuitionniste, car il n'y a pas de méthode de construire de telles fonctions, une raison importante à cela est que nous n'avons pas rien pour "construire" ces fonctions: Pour prouver \textsf{AC}, nous devions fournir sa preuve, mais pour fournir les preuves, vous devez d'abord avoir des choses pour les construire, néanmoins dans la logique intuitionniste des prédicats, il n'y a pas de tels choses, et c'est ici que la théorie des types entre le terrain.

Une théorie qui est assez puissante pour prouver les propriétés de elle-même

  La théorie des types est une théorie plutôt spéciale, quand nous parlons des systèmes formelles, il implique souvent deux théories: la théorie des objets et la métathéorie, la permière est la théorie à propos des objets mathématiques qui sont recherché, par exemple la théorie des nombres réels, la théorie des groupes, et cetera; la dernière est plutôt intéressante, en mathématiques, nous ne considérons pas souvent la théorie lui-même quand nous recherchons sur les objets comme les nombres réels, nous ne prouvons jamais la correction des méthode que nous utilisons, mais les méthodes que nous utilisons sont peut-être incorrects, nous avons besoin des méthodes pour justifier la correction des théories elles-mêmes. Et voilà, nous avons les métathéories, celles qui sont théories qui recherchent d'autres théories, cependant il y a un problème: si nous utilisons les métathéories pour justifier les théories des objets, alors que devons-nous utiliser pour justifier les métathéories? Et justifier les méta-métathéories ad infinitum? En fait, la correction de telles théories sont prouvé en utilisant les fondements des mathématics, ceux qui sont les théories qui sont assez puissante pour prouver les propriétés de elles-mêmes, et les mathématiques sont interne à elles, pour que nous n'avons pas besion des métathéories sur métathéories, car les objets sont défini dans cette théorie, et cette théorie est capable de raisonner sur elle-même, de telle théorie est à la fois:

  1. Les objets.
  2. La théorie des objets
  3. La métathéorie de la théorie des objets
  4. La métathéorie de sa propre.

  Ces ensemble impliquent que toutes les prépositions, qu'elles soient3 des objets, des théories, ou d'elle-même, sont tous prouvable dans elle-même. De telles théories pouvons à la fois représenter les prépositions et leurs preuves. Et la théorie intuitionniste des types est une telle théorie.

Pour clarifier, bien que la logique du premier ordre, abrége en FOL, de son nom en anglais: First-Order Logic, soit souvent utilisé pour formuler les systèmes axiomatiques, comme les systèmes pour l'arithmétique, il ne considéré pas une fondement des mathématics: il n'y a aucun objets mathématiques qui sont interne à elle.

L'axiome du choix dans la théorie intuitionniste des types

  Dans la ITT, il n'y a pas que des preuves, mais également les objets des preuves ceux qui sont les \lambda-termes, et prouver une préposition revient à4 trouver un \lambda-terme du type correspondant, quant à \textsf{AC2}, dans le symbolisme de la ITT c'est écrit:

(\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))})

Pour éviter (avoid) des confisions, nous utilisons les couleurs différentes pour souligner5 les parties différentes dans l'expression: le rose est binders (en anglais), la pourpre est types des binders, et la turquoise est les expressions. \Pi represente \Pi-Types et correspond à \forall par l'isomorphism de Curry-Howard, \Sigma represente \Sigma-Types et correspond à \exists par l'isomorphisme, remarquons que dans notre symbolisme, au lieu de \Sigma y: B, nous écrivons \Sigma y: B(x) où x: A, cependant c'est d'accord pour B pour dépendre de x ou non. De plus, nous définissons \mathsf{Ap}(f, x) être f(x). Pour prouver ce type ou cette préposition, nous devions trouver le \lambda-terme correspondant dans les marches6 suivantes:

  1. Supposons que nous ayons:
    1. La prémisse 1: \Pi \textcolor{pink}x:\textcolor{crimson}{A}.\Sigma \textcolor{pink}y: \textcolor{crimson}{B(x)}. \textcolor{turquoise}{R(x, y)}, id est, il y a \phi avec le type \Pi \textcolor{pink}x:\textcolor{crimson}{A}.\Sigma \textcolor{pink}y: \textcolor{crimson}{B(x)}. \textcolor{turquoise}{R(x, y)}
    2. La prémisse 2: x\in A
  2. Par \Pi-Élimination, nous avons \mathsf{Ap}(\phi, x): \Sigma \textcolor{pink}y:\textcolor{crimson}{B(x)}.\textcolor{turquoise}{R(x, y)}

  3. Par la conséquence directe de \Sigma-Élimination, nous avons la fonction de la projection droite \mathsf{p} et la projection gauche \mathsf{q}. Soit \mathsf{Ap}(\phi, x): \Sigma \textcolor{pink}y:\textcolor{crimson}{B(x)}.\textcolor{turquoise}{R(x, y)}, appliquons \mathsf{p} nous obtenons \mathsf{p}(\mathsf{Ap}(\phi, x)): \textcolor{crimson}{B(x)} et appliquons \mathsf{q} nous obtenons \mathsf{q}(\mathsf{Ap}(\phi, x)): \textcolor{turquoise}{R(x, \mathsf{p}(\mathsf{Ap}(\phi, x)))} par la définition de \mathsf{q}.

    La raison de telle conséquence est que par la BHK-Interprétation et l'isomorphisme de Curry-Howard, les éléments des \Sigma-types \Sigma x: A. B(x) sont les paires ordonées (a, b) telles que B(a) tienne, donc supposons que nous ayons \omega:\Sigma x:A.B(x), alors la projection naturelle droite \mathsf{p}(\omega)=\mathsf{p}((a, b)) est défini être7 a; et la projection naturelle gauche \mathsf{q}(\omega)=\mathsf{q}((a, b)) est défini être B[x\mapsto \mathsf{p}(\omega)].

  4. Par \Pi-Introduction (\lambda-Abstraction) sur x, nous avons \lambda z: A.\mathsf{p}(\mathsf{Ap}(\phi, z)): \textcolor{crimson}{\Pi z:A. B(x)}. Ce marche est nécessaire pour décharger la prémisse 2.

  5. Par \Pi-Égalité (\eta-Expansion), nous avons: \mathsf{Ap}(\lambda z: A.\mathsf{p}(\mathsf{Ap}(\phi, z)), z): \textcolor{crimson}{B(x)}, ce qui est équivalent à \mathsf{p}(\mathsf{Ap}(\phi, z)):\textcolor{crimson}{B(x)}.
  6. 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)))
  7. 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))}
  8. 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))}
  9. 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))}, remarquons que \phi est remplacé par f.
  10. Abstracyons \phi en f, 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))}). QED.

  1. supposons que follows subjunctive mood ↩︎

  2. tel que follows subjunctive mood when it means "such that" ↩︎
  3. is this grammatically correct? ↩︎
  4. revenir à: amounts to ↩︎
  5. souligner: to emphasize ↩︎
  6. marche: steps ↩︎
  7. ou défini comme étant, moins formelle ↩︎