Epsilon de Hilbert

L'Epsilon de Hilbert est une extension d'un langage formel par l'opérateur epsilon, où celui-ci se substitue aux quantificateurs dans le langage en tant que méthode conduisant à une preuve de la cohérence pour l'extension du langage formel. L'opérateur epsilon et la méthode de substitution epsilon sont généralement appliqués à un calcul de prédicats, suivis par une démonstration de la cohérence. Le calcul des prédicats étendu par l'opérateur epsilon est ensuite étendu et généralisé pour couvrir les objets mathématiques, les classes et les catégories pour lesquelles on veut montrer la cohérence, en s'appuyant sur la cohérence déjà montrée à des niveaux antérieurs.

Opérateur Epsilon

Notation de Hilbert

Pour tout langage formel L, on prolonge L par adjonction de l'opérateur epsilon afin de redéfinir la quantification :

• $(\exists x)A(x)\ \equiv \ A(\epsilon x\ A)$
• $(\forall x)A(x)\ \equiv \ A(\epsilon x\ (\neg A))$

L'interprétation voulue de εx A est que certaines valeurs de x satisfont à A, si elles existent. En d'autres termes, εx A renvoie un certain élément t tel que A(t) est vrai, sinon elle renvoie un terme arbitraire ou choisi par défaut. Si plus d'un terme vérifie A, alors n'importe lequel de ces termes (qui rend A vrai) peut être choisi, de manière non-déterministe. Il est nécessaire de définir l'égalité en vertu de L, et les seules règles nécessaires pour L prolongé par l'opérateur epsilon sont modus ponens et la substitution d' A(t) pour remplacer A(x) pour tout terme t.

Notation de Bourbaki

Dans la Théorie des Ensembles de N. Bourbaki, les quantificateurs sont définis comme suit :

• $(\exists x)A(x)\ \equiv \ (\tau _{x}(A)|x)A$
• $(\forall x)A(x)\ \equiv \ \neg (\tau _{x}(\neg A)|x)\neg A\ \equiv \ (\tau _{x}(\neg A)|x)A$

où A est une relation dans L, x est une variable ; et $\tau _{x}(A)$ juxtapose un $\tau$ à gauche de A, remplace toutes les occurrences de x avec $\square$ et les relie à $\tau$. Soit Y un assemblage, (Y|x)A désigne le remplacement de toutes les variables x dans A avec Y.

Cette notation est équivalente à la notation de Hilbert et est lue de la même manière. Elle est utilisée par Bourbaki pour définir le cardinal d'affectation puisqu'il n'utilise pas l'axiome de remplacement.

Définir des quantificateurs de cette manière mène à un grand manque d'efficacité. Par exemple, l'expansion, à l'aide de cette notation, de la définition originale de Bourbaki du nombre un a une longueur d'environ 4,5 × 10¹², et pour une édition ultérieure de Bourbaki qui combine cette notation avec la définition de Kuratowski des paires ordonnées, ce nombre atteint environ 2,4 × 10⁵⁴.

Approches modernes

Le programme de Hilbert pour les mathématiques était de justifier des systèmes formels comme cohérents par rapport à des systèmes constructifs ou semi-constructifs. Alors que les résultats de Gödel sur l'incomplétude rendirent le programme de Hilbert stérile dans une grande mesure, les chercheurs contemporains considèrent que l'epsilon de Hilbert fournit des solutions de rechange pour approcher les preuves de cohérence systémique comme décrit dans la méthode de substitution epsilon.

Méthode de substitution epsilon

Une théorie soumise à un contrôle de cohérence est d'abord incorporée dans un epsilon de Hilbert approprié. Deuxièmement, un processus est développé pour la réécriture des théorèmes quantifiés afin que ceux-ci soient exprimés en termes d'opérations epsilon par l'intermédiaire de la méthode de substitution epsilon. Enfin, il doit être montré que le processus normalise le processus de réécriture, de sorte que les théorèmes réécrits satisfont les axiomes de la théorie.

Références

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Epsilon calculus » (voir la liste des auteurs).
• "Epsilon Calculi". Internet Encyclopedia of Philosophy.
• Moser, Georg; Richard Zach. The Epsilon Calculus (Tutorial). Berlin: Springer-Verlag. OCLC 108629234.
• Avigad, Jeremy; Zach, Richard (November 27, 2013). "The epsilon calculus". Stanford Encyclopedia of Philosophy.
• Bourbaki, Éléments de mathématique, Théorie des ensembles. Springer. Réimpression inchangée de l'édition originale de 1970, (ISBN 978-3-540-34034-8).