Théorème de Diaconescu

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Pour les articles homonymes, voir Diaconescu.

En logique mathématique, le théorème de Diaconescu, ou théorème de Goodman-Myhill, concerne la théorie des ensembles et les mathématiques constructives. Il énonce que dans une théorie constructive des ensembles (en) avec extensionnalité, le principe du tiers exclu (éventuellement restreint à certaines classes de propositions suivant la théorie en jeu) peut se déduire de l'axiome du choix. Il fut découvert en 1975 par Diaconescu[1] puis par Goodman et Myhill[2].

Démonstration[modifier | modifier le code]

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

\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

\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

(f(U)\in U)\land(f(V)\in V)

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

[P \vee (f(U) = 0)] \wedge [P \vee (f(V) = 1)]

d'où, puisque 0≠1,

P \vee (f(U) \neq f(V))~.

D'autre part, comme

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

on a P \to (f(U) = f(V))~,

donc (f(U) \neq f(V)) \to \neg P par contraposition.

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

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 cette axiome : l'axiome de Σ0-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é.

Notes[modifier | modifier le code]

  1. (en) R. Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society 51 (1975) 176-178
  2. (en) N. D. Goodman et J. Myhill, « Choice Implies Excluded Middle », Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 24 (1975) 461