Théorème de Diaconescu - Diaconescu's theorem

En logique mathématique , le théorème de Diaconescu , ou théorème de Goodman-Myhill , déclare que l' axiome complet du choix est suffisant pour dériver la loi du milieu exclu , ou des formes restreintes de celui-ci, dans la théorie constructive des ensembles . Il a été découvert en 1975 par Radu Diaconescu et plus tard par Goodman et Myhill . Déjà en 1967, Errett Bishop posait le théorème comme un exercice (Problème 2 à la page 58 dans Fondements de l'analyse constructive ).

Preuve

Pour toute proposition , nous pouvons construire les ensembles${\ displaystyle P \,}$

${\ displaystyle U = \ {x \ in \ {0,1 \} :( x = 0) \ vee P \}}$

et

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

Ce sont des ensembles, utilisant l' axiome de la spécification . Dans la théorie classique des ensembles, cela équivaudrait à

${\ displaystyle U = {\ begin {cases} \ {0,1 \}, & {\ mbox {if}} P \\\ {0 \}, & {\ mbox {if}} \ neg P \ end { cas}}}$

et de même pour . Cependant, sans la loi du milieu exclu, ces équivalences ne peuvent être prouvées; en fait, les deux ensembles ne sont même pas prouvés finis (au sens habituel d'être en bijection avec un nombre naturel , bien qu'ils le seraient au sens de Dedekind ). ${\ displaystyle V \,}$

En supposant l' axiome de choix , il existe une fonction de choix pour l'ensemble ; c'est-à-dire une fonction telle que ${\ displaystyle \ {U, V \} \,}$${\ displaystyle f \,}$

${\ Displaystyle [f (U) \ in U] \ wedge [f (V) \ in V]. \,}$

Par la définition des deux ensembles, cela signifie que

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

ce qui implique ${\ Displaystyle (f (U) \ neq f (V)) \ vee P.}$

Mais puisque (par l' axiome d'extensionnalité ), donc , donc ${\ displaystyle P \ à (U = V)}$${\ Displaystyle P \ à (f (U) = f (V)) \,}$

${\ Displaystyle (f (U) \ neq f (V)) \ to \ neg P.}$

Ainsi, comme cela pourrait être fait pour n'importe quelle proposition, ceci complète la preuve que l'axiome du choix implique la loi du milieu exclu. ${\ displaystyle \ neg P \ vee P.}$

La preuve repose sur l'utilisation de l'axiome de séparation complète. Dans les théories constructives des ensembles avec seulement la séparation prédicative , la forme de P sera limitée aux phrases avec des quantificateurs liés uniquement, ne donnant qu'une forme restreinte de la loi du milieu exclu. Cette forme restreinte n'est toujours pas acceptable d'un point de vue constructif.

Dans la théorie des types constructifs , ou dans l' arithmétique de Heyting étendue avec des types finis, il n'y a généralement pas de séparation du tout - les sous-ensembles d'un type reçoivent des traitements différents. Une forme de l'axiome du choix est un théorème, mais le milieu exclu ne l'est pas.

Remarques