Théorème de Diaconescu

Soit P une proposition quelconque. En utilisant l'axiome de compréhension, on définit deux ensembles

${\displaystyle {\begin{matrix}U=\{x\in \{0,1\}:P\vee (x=0)\}\\V=\{x\in \{0,1\}:P\vee (x=1)\}\ .\end{matrix}}}$

Remarquons que dans la théorie classique, U et V seraient simplement

${\displaystyle {\begin{matrix}U={\begin{cases}\{0,1\},&{\mbox{si }}P\\\{0\},&{\mbox{si }}\neg P\end{cases}}&\;&V={\begin{cases}\{0,1\},&{\mbox{si }}P\\\{1\},&{\mbox{si }}\neg P\end{cases}}\end{matrix}}}$

mais ces équivalences sont fondées sur le principe du tiers exclu, sans lequel on ne peut affirmer que «P ou ¬P».

L'axiome du choix affirme l'existence d'une fonction de choix f pour l'ensemble {U,V}, c'est-à-dire qu'il existe une fonction f telle que

${\displaystyle (f(U)\in U)\land (f(V)\in V)}$

et par définition de ces deux ensembles, cela signifie que

${\displaystyle [P\vee (f(U)=0)]\wedge [P\vee (f(V)=1)]}$

d'où, puisque 0≠1,

${\displaystyle P\vee (f(U)\neq f(V))~.}$

D'autre part, comme

${\displaystyle P\to (U=V)}$ par l'axiome d'extensionnalité,

on a ${\displaystyle P\to (f(U)=f(V))~,}$

donc ${\displaystyle (f(U)\neq f(V))\to \neg P}$ par contraposition.

De ${\displaystyle P\vee (f(U)\neq f(V))}$ et ${\displaystyle (f(U)\neq f(V))\to \neg P}$ on déduit :

${\displaystyle P\vee \neg P~.}$

Cela prouve que l'axiome du choix implique la loi du tiers exclu pour toutes propositions P auxquelles s'applique l'axiome de compréhension. La théorie classique des ensembles accepte cet axiome sans restriction, mais pour le constructivisme il n'est pas acceptable dans sa forme générale à cause de son imprédicativité. Néanmoins la théorie constructive des ensembles accepte une version prédicative de cet axiome : l'axiome de Σ₀-séparation, qui est l'axiome de compréhension limité aux propositions P dont les quantificateurs sont bornés. La preuve donne donc une forme de la loi du tiers exclu limitée aux propositions P de ce type ; cette forme restreinte du tiers exclu est toujours rejetée par les constructivistes, donc ils ne peuvent pas accepter la forme générale de l'axiome du choix non plus.

En théorie constructive des types, on peut parfois donner une preuve constructive de l'axiome du choix pour des types, mais à cause de la nature de ces types il s'agit de formes restreintes de l'axiome. Le tiers exclu ne peut s'en déduire, car on ne dispose pas de l'axiome d'extensionnalité.

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Diaconescu's theorem » (voir la liste des auteurs).