- 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 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
- (en) R. Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society 51 (1975) 176-178
- (en) N. D. Goodman et J. Myhill, Choice Implies Excluded Middle, Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik 24 (1975) 461
- (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)
Catégories :- Théorie des ensembles
- Logique mathématique
- Théorème de mathématiques
![[P \vee (f(U) = 0)] \wedge [P \vee (f(V) = 1)]](9/fe903b966555c7c17590ac64fd4dd3e1.png)
Wikimedia Foundation. 2010.
