Accueil🇫🇷Chercher

Théorème de 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

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

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

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

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

d'où, puisque 0≠1,

D'autre part, comme

par l'axiome d'extensionnalité,

on a

donc par contraposition.

De et on déduit :

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 Σ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

  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
Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.