La théorie des ensembles a 150 ans. Ce n'est pas si vieux que cela comparé au théorème de Pythagore qui a 2500 ans. Et elle introduit un concept révolutionnaire qu'est l'élément, une variable qui peut désigner toute chose, et encore, l'expression "toute choses" parait trops restrictive. La seule chose certaine est la formule et non ce que désignent ses variables. C'est pourquoi les mathématiques se fondent sur la logique, une logique qui fonctionne mécaniquement sur la syntaxe et qui ne se préoccupe pas de ce que désignent les variables élémentaires.
La création du concept d'élément pouvant tout désigner va définir la logique du premier ordre, une logique où il n'y a à coté des variables booléennes qu'une seule classe de variable élémentaire, des variables capables de tout désigner...
Mais pour établire les bases linguistico-logique du calcul des prédicats, on doit utiliser le mécanisme d'extension du langage par déclaration existentielle de nouvelles variables, ce qui nous place directement dans une logique du second ordre.
Les démonstrations sont des calculs, c'est pourquoi on basera la théorie de la démonstration en logique du second ordre sur la théorie de la calculabilité. Il faut donc définir canoniquement un langage du second ordre suffisament riche pour atteindre le domaine de calculabilité d'une machine de Turing, pour ainsi fonder une théorie de la démonstration dans cette logique.
La logique du premier ordre introduit un premier type de variable dite élémentaire, non limitée, suceptible de désigner toute chose.
Pour introduire les variables élémentaires dans le calcul propositionnel qui est un calcul booléen, il est nécessaires d'introduire des prédicats qui transforment des éléments en un booléen, ainsi que par similitude, des foncteurs qui transforment des éléments en un élément.
On représente souvent les variables booléennes en majuscule et les variables élémentaires en minuscule. Les prédicats sont souvent notés en majuscule, comme le sont les variables booléennes qui constituent des prédicats nullaires. Les foncteurs sont souvents notés en miniscule, comme le sont les variables élémentaires qui constituent des foncteurs nullaires. Prédicats et foncteurs ont comme suffixe les symboles suivants `(".")`, `(".,.")`, `(".,.,.")`, etc., ou suivants `("...")`, `(".,...")`,`(".,.,...")`, etc., qui précisent leur arité. L'absence de suffixe dénote le type booléen ou le type élément.
L'opération d'unification de termes joue un rôle essentiel dans les démonstrations. C'est pourquoi l'arité variable est autorisée et placée toujours en fin de liste pour des raisons pratiques propre à l'unification, et qu'il y a donc un deuxième type de variable qu'est la liste finie d'éléments que l'on note préfixée par une étoile, `"*"x`. On verra par la suite que l'enrichissement du langage par l'ajout de variable liste finie, ne pouvant se placer qu'à la fin des listes, ne change pas la nature du langage qui reste toujours du premier ordre.
Considérons par exemple trois prédicats `A("."), B(".,."), C(".,...")`, les trois foncteurs `f("."), g(".,."), h(".,...")` et deux éléments `a,b`. Le suffixe `(".,...")` désigne une arité variable au moins égale à `1`. Si on se tient qu'à ces seuls prédicats et foncteurs et éléments, et si on s'en tient qu'au seul moyen de construction par emboitement clos, notre langage aura créé potentiellement une foule d'éléments qui correspond au domaine de Herbrand présenté ici :
`"<"f("."),g(".,."),h(".,..."),a,b">"`
C'est une algèbre libre. Les foncteurs générateurs sont mis entre crochet. C'est l'ensemble de tout les termes clos qu'il est possible de construire en emboitant autant de copies de foncteurs générateurs que l'on veut. A ce stade où nous n'avons pas de théorie des ensembles, le domaine de Herbrand s'identifie à un programme énumérant tout ses éléments, que l'on représente par une grammaire où l'opérateur point-virgule est l'opérateur de séquence aplatie :
`E←{a,b,f(E),g(E ";" E),h(E ";" "*"E))}`
`"*"E←{(), (E), (E ";" "*"E)}`
On définie les modèles pour la logique du premier ordre comme suit : Chaque prédicats générateurs c'est à dire faisant partie de la présentation du langage, s'appliquent à chaque n-uplets d'éléments du domaine de Herbrand pour former des variables booléennes. L'instanciation de toutes ces variables booléennes constitue un modèle du premier ordre. N'ayant pas introduit le prédicat d'égalité, nous avons décrit ce qu'est un modèle d'algèbre libre. Dans notre exemple, pour chaque élément `x` du domaine de Herbrand, deux variables booléennes `A(x)` et `B(x)` sont créés. L'ensemble de toutes ces variables booléennes se note :
`{A("."),B(".")}"<"f("."),g(".,."),h(".,..."),a,b">"`
Exemples de variables booléennes : `A(g(a,f(a))), B(h(a,b,a,b))`. L'instanciation de toutes ces variables booléennes constitue un modèle. Le prédicat déterminant ses propres valeurs booléennes, le modèle est donc défini par les prédicats générateurs.
En logique du premier ordre, il est impossible de définir l'infini. Aucune preuve ne peut garantir cet infini recherché.
Le prédicat unaire `A` que l'on note parfois en précisant son arité `A(".")` doit être préalablement déclaré comme faisant partie du langage. Cela se fait en logique du second ordre où il y a une deuxième classes de variable désignant des prédicats :
`EEA("."),`
Il est à noter que cette deuxième classe est incluse dans la première classe, puisque par principe l'élément peut tout désigner. Une fois déclaré `EEA("."),` ce qui enrichit le langage d'un prédicat unaire `A`, il peut être appliqué à n'importe quel élément. Le prédicat `A` désigne tout les éléments `x` tel que `A(x)`, c'est à dire quelque chose qui s'apparente à un ensemble mais qui est plus générale puisque nous n'avons posé aucune théorie concernant le prédicat `A` autre que sa déclaration, `EEA(".")`.
Le prédicat peut être appliqué à n'importe quel élément, et constitue lui-même un élément. Il peut donc s'appliquer à lui-même. Pour désigner le prédicat en tant qu'élément, on étend le langage en permettant d'écrire le prédicat sans l'appliquer. Le terme `A(A)` désigne donc un booléen.
Il convient à chaque fois de vérifier si l'extension du langage ne crée pas d'ambiguité. Et ici il peut y avoir une ambiguité avec les prédicats d'arité variables. Considérons un prédicat d'arité variable `EEP("...")`. Pour éviter de confondre le prédicat `P` interprété comme élément, et sa valeur booléenne obtenue lorsqu'on l'applique à une liste vide d'élément, on notera `P()` pour exprimer l'application de `P` à la liste vide d'élément.
La définition de l'élément pose une difficulté puisqu'il peut désigner toute chose. Une manière de diviser le problème consiste à lui donner un type, et de reporter le problème de la limite sur ce que peut désigner un type. Et chaque type s'accompagne d'un enrichissement du langage pour pouvoir écrire un élément de ce type.
Citons quelques éléments qui sont à notre disposition immédiate : les booléens, les éléments, les prédicats, les énoncés du 1er ordre, les énoncés du 2d ordre, et nous verrons par la suite d'autres types d'élément plus complexes. Ainsi ces 5 expressions où le type de l'élément est spécifié au dessus, sont des booléens inconnus :
`A(overset("Booléen")(0))`, `A(overset("Elément")(a))`, `A(overset("Prédicat")(A))`, `A(overset("Enoncés 1er ordre")(EEx, A(x)))`, `A(overset("Enoncés 2d ordre ")(EEX("."), X(overset("Prédicat")(X))))`
Le prédicat `A`, tel une fonction caractéristique, désigne quelque chose qui s'apparente à un ensemble, mais qui est plus générale puisque nous n'avons posé aucune théorie. Notez qu'à ce stade, nous n'avons pas encore défini l'égalité ni l'inégalité entre éléments, nous l'avons définit seulement entre booléens.
Peut-on définir un prédicat `A(".")` par n'importe quel formule ? bien sûr que non. En particulier on ne peut pas définir récurcivement le prédicat si on ne s'assure pas que la recursion s'arrête bien et donne une réponse cohérente. A ce stade et avec cette approche, le paradoxe de Russel ne constitue pas un paradoxe, et les fondements recherchés renouent avec le principe de calculabilité.
Les éléments, les prédicats et les foncteurs doivent être préalablement déclarés comme faisant partie du langage.
`EEA("."),EEB(".,."),EEC(".,..."),EEf("."), EEg(".,."), EEh(".,..."),EEa,EEb`
Une fois cette déclaration faite, le langage est enrichi de ces trois prédicats, de ces trois foncteurs, et de ces deux éléments. Il est à noter que le prédicat comme le foncteur sont de possibles éléments, puisque par principe l'élément peut tout désigner.
Le prédicat d'égalité est un prédicat particulier associé à un shéma d'axiome permettant de permutter des élément égaux dans toutes formules. Tant qu'il n'est pas introduit dans le langage et dans le système de démonstration, la nature de l'élément reste incomplète. Il convient alors de l'appeller sous un autre nom, mais quel nom ? Posons la questiuon à CHatGPT 4o :
En logique mathématique, l'égalité élémentaire est un prédicat (que l'on ajoute au langage logique) et qui est accompagné par un schéma d'axiomes permettant de permuter deux éléments égaux dans toutes formules (que l'on ajoute au système de démonstration).
Si nous définissons une logique sans le prédicat d'égalité, cela change la nature de l'élément. Quel nom commun autre que "élément" pourrions-nous donner à cet élément incomplet ?Très belle question, vraiment subtile ! Quand on enlève le prédicat d'égalité, l'élément (disons "x") perd la capacité fondamentale d'être comparé ou identifié avec un autre. Cela le rend plus "flottant", plus individuel mais aussi indistinct dans son essence.
Pour un nom commun qui évoque cette idée d'élément sans égalité, quelques suggestions naturelles pourraient être :
- atome (classique en logique sans égalité, mais un peu technique)
- point (souvent utilisé en topologie ou en théorie des modèles abstraits)
- individu (très courant en logique du premier ordre sans égalité)
- instance (moins courant mais intéressant philosophiquement)
- séparé (plus imagé : car sans lien d'égalité, il est seul)
- entité (général, neutre, assez philosophique)
Par exemple, en logique du premier ordre sans égalité, on parle souvent d'individus dans un domaine d'interprétation.
"Individu" serait sans doute le meilleur mot commun ici, car il souligne qu'on parle d'une chose qui existe "en soi", sans nécessairement pouvoir être confondue ou comparée à une autre.
Veux-tu que je te propose encore d'autres variantes selon que tu cherches un ton plus technique, poétique, ou philosophique ?
Les intuitionnistes exigent que les éléments soient calculables. Cela entraine des contraintes très fortes sur la définition des éléments. L'élément devient un terme d'un langage `Omega`, transcriptible sur le ruban d'une machine de Turing. Et le prédicat comme le foncteur devient un programme de taille finie qui constitue lui-même un terme du langage `Omega`, et qui appliqué à l'élément doit toujours s'arrêter en un temps fini, et retourner une des deux seuls réponses possibles `0` ou `1`. Cette exigence des intuitionnistes définira les sous-ensembles décidables de `Omega`.
Puis les intuisionnistes deviendront moins exigeant et n'exigeront que la semi-calculabilité des éléments. A savoir que le programme de construction sera autorisé à ne jamais s'arréter et donc à ne jamais donner de réponse. Et ils s'autoriseront à se placer à la fin des temps, ce qui est déjà fait à travers le constat de ne jamais s'arréter, pour décider des suites en cas de non-réponse.
Ici, on sort du simple fondement. On adopte un axiome pour permettre de concevoir des choses qui n'existent pas. Il s'agit d'un choix. Les deux choix sont possibles. Soit on s'autorise à se placer à la fin des temps et l'on peut procéder à de nouvelles constructions d'éléments. Ou soit on adopte le principe opposé, que l'on ne peut pas construire de nouveaux éléments à partir de la fin des temps.
La fondation classique n'impose pas la calculabilité des éléments ni leur semi-calculabilité. Mais une démonstration étant un calcul, la démonstration constitue un élément calculable, même si elle définit des éléments incalculables. C'est pourquoi, la fondation des mathématiques classique passe nécessairement par le principe de calculabilité appliqué aux démonstrations.
Il existe toute approche des mathématiques par la calculabilité, où l'on étend davantage le langage pour pouvoir exprimer de nouveaux éléments. Au départ, nous avons la structure d'algèbre libre composé de tous les termes clos qu'il est possible de construire avec autant de copies de foncteurs générateurs que nécessaire.
On peut construire des termes plus riches en se basant sur une notion plus générale que celle d'emboitement clos, qui est celle de calculabilité. Nous allons progressivement enrichire le langage pour pouvoir calculer d'autres foncteurs jusqu'à atteindre le domaine de calculabilité de Turing.
On définit un premier niveau de construction permettant de construire de nouveaux foncteurs. On utilise le symbole point "`"."`" comme argument pour désigner les arguments d'entrée du nouveau foncteur, et qui seront pris dans l'ordre de leur apparition.
Les expressions `g(".,"a)`, `g(".,"f("."))` désigne de nouveaux foncteurs. Les arguments du foncteur décrit par un terme de premier niveau sont désignés par les points dans l'ordre de leur apparition dans le terme.
Pour permuter ou dupliquer les arguments, on définit un deuxième niveau de construction. Le foncteur pourra se noter explicitement en déclarant ses arguments aux travers de variables muettes. Exemples :
`f = f(".") = x "|" f(x)`
`g = g(".,.") = (x,y) "|" g(x,y)`
`h = h(".,...") = (x,"*"x) "|" h(x,"*"x)`
`g(".,"a) = x "|" g(x,a)`
`f(f(".")) = x "|" f(f(x))`
`g(".,"f(".")) = (x,y) "|" g(x,f(y))`
`h(".,"a",.,"b",...") = (x,y,"*"x) "|" h(x,a,y,b,"*"x)`
Une fonction n'est pas forcement défini partout. Un premier filtre est mis en place dans l'appel de fonction. On procède à l'unification de la séquence d'appel avec la tête de la fonction. Si l'unification réussit, le corps de la fonction est retourné en susbstituant les variables par leur valeurs obtenues lors de l'unification. Si l'unification échoue, la fonction n'est pas définie. Exemple :
`k = (x,f(x)) "|" g(x,x)`
`k(a,f(a))` est défini et vaut `g(a,a)`, tandis que `k(a,a)` n'est pas défini.
Cette extension du langage implique que les variables déclarées constantes du langage soient toutes distinctes, une notion qui peut être ainsi introduite avant même l'introduction de l'égalité élémentaire.
Puis, la fonction est définie par une liste de fonctions. Et lors d'un appel, c'est la première fonction de la liste pour laquelle l'unification de l'appel fonctionne qui est actionnée. Exemple :
`k = {`
`(x,y,g(x,y)) "|" g(y,x)`
`f(x) "|" x`
`(x,y) "|" f(x)`
`}`
`k(f(b))` vaut `b`,
`k(a)` n'est pas défini,
`k(a,b)` vaut `f(a)`,
`k(a,b,g(a,b))` vaut `g(b,a)`,
`k(a,a,a)` n'est pas défini.
On généralise en remplaçant les conditions d'unification par des fonctions propositionnelles Exemple :
`k = {x,y|`
`P(x,y) => g(y,x)`
`Q(f(y)) => x`
`R(y,x) => g(y,f(x))`
`}`
Pour le cas particulier des entiers naturels, représenté par l'algèbre libre suivante : `EEs("."), EE0`
Les fonctions primitives récurcives de base sont :
L'élément générateur `0`
Les projections :
`pi_1 = (x,"*"x)|->x`
`pi_2 = (x,y,"*"x)|->y`
`pi_3 = (x,y,z,"*"x)|->z`
...
`pi_n = (x_1,x_2,x_3,...,x_n,"*"x)|->x_n`
...Le foncteur générateur `s(".")`
La fonction `f = sf"Recursion"(g,h)` est définie comme suit :
`f(0,"*"x) = g("*"x)`
`AAn, f(s(n),"*"x) = h(n,f(n,"*"x),"*"x)`Où `g` et `h` sont deux fonctions primitives récurcives quelconques, `AAg("*"x),AAh("*"x),`
On défini la fonction récurcive générale c'est à dire s'appliquant à une algèbre libre plutôt qu'aux seuls entiers naturels.
...
C'est en voulant définir l'infini qu'est apparue la nécessité de définir préalalement ce qu'est un ensemble. Mais avant de définir l'ensemble d'un point de vue classique, on définit une notion d'ensemble énuméré plus simple avec l'exigence intuitioniste forte et que l'on appelle énumérateur.
...
Et ont commence par décrire la clôture du domaine de Herbrand. Considérons par exemple des éléments `a,b` définissables et des fonctions `f("."), g(".,.")` définissables et une fonction propositionnelle `P(".")` définissable que l'on souhaite démontré valable pour tous les éléments engendrés par la sous-structure `"<"a,b,f("."),g(".,.")">"`. La récurrence générale affirme :
`((P(a)),(P(b)),(AAx P(f(x))), (AAxAAy P(g(x,y))) ) => AAx in "<"a,b,f("."),g(".,.")">" P(x)`
---- 25 avril 2025 ----