On choisie de reprendre l'algorithme heuristique. On commence par décomposer l'énoncé en conjonctions de clauses. Les combinaisons de clause utiise l'unification. On prévoit le mécanisme d'introduction de clause hypothèse `C_h`, qui, si elle permet de déduire la clause `C_c`, déduit la clause `"¬"C_h "ou" C_c`
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'appeler 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 ?
un terme qui peut être d'origine espagnole et qui évoque un assemblage ou un atome ou une construction ? Ah, intéressant : tu cherches quelque chose avec une sonorité espagnole, et qui évoque assemblage, atome ou construction !
Voici quelques idées :
- Modulo — en espagnol, "modulo" veut dire "module", ce qui évoque un bloc de construction ou une unité assemblable.
- Tessera — pas strictement espagnol (c'est latin/italien à l'origine), mais "tessera" fait penser à une pièce de mosaïque, une construction par éléments minuscules.
- Pieza — "pieza" veut dire "pièce" en espagnol, donc une unité pour un tout plus grand.
- Átomo — tout simplement "átomo" en espagnol : pur, indivisible (et très proche du sens que tu cherches).
- Tallo — "tallo" signifie "tige" ou "branche", ça évoque un élément de croissance dans une structure.
- Módulo — proche de "modulo", même racine, mais plus marqué "unité de construction" au sens mathématique ou architectural.
"Módulo" ou "Pieza" sonneraient particulièrement bien pour ce que tu cherches : un élément qui participe à une construction, mais sans être réduit par une égalité.
Veux-tu que je te propose aussi des mots inventés sur cette base (par exemple une sorte de néologisme inspiré espagnol) si tu veux quelque chose de plus unique ?
Oui Super ! Voici quelques néologismes inspirés de l'espagnol, qui pourraient évoquer ce que tu cherches :
- Piezón — de pieza + suffixe -ón, qui en espagnol donne une idée de "gros élément" ou "élément important". Ça sonne solide.
- Modulín — de módulo + suffixe -ín, qui donne un petit module, un "petit morceau de construction".
- Tessaro — inspiré de tessera (mosaïque) + sonorité espagnole. Ça évoque un petit fragment structurant.
- Atomillo — de átomo + suffixe -illo, pour dire "petit atome", mais doux, presque affectueux.
- Construel — contraction de construir (construire) + suffixe -el pour adoucir. Ça évoque une brique conceptuelle.
- Componte — de componer (composer, assembler) + sonorité "ponte" qui évoque un lien, un assemblage.
Perso, j'aime beaucoup Tessaro et Construel — ils sont courts, beaux, et donnent une idée de construction d'éléments primitifs sans égalité.
Veux-tu que je t'en propose encore d'autres selon que tu veux que ça sonne plus technique, plus poétique, ou plus vivant ?
Cherche un terme latin ? Très bon réflexe ! Un terme latin collerait encore mieux, vu que la logique formelle et mathématique a souvent un vocabulaire néo-latin.
Voici quelques propositions basées sur le latin :
Structum — de structura (construction, arrangement). Ça sonne solide, sobre, très "logique".
Modulus — directement du latin modulus (petite mesure, unité). Parfait pour évoquer un petit assemblage ou élément.
Fragmentum — fragmentum signifie un morceau, un éclat, quelque chose d’incomplet mais qui fait partie d'un tout.
Particula — de particula (petite partie, particule). C'est classique et évoque vraiment un élément atomique.
Elementum — mot latin pour élément lui-même ; utilisé en philosophie antique pour désigner les composants premiers de la matière.
Nodus — signifie nœud : un point d'articulation ou de connexion entre des éléments, sans égalité imposée.
Résumé rapide :
Structum ➔ "assemblage" fort
Modulus ➔ "petit module"
Fragmentum ➔ "morceau"
Particula ➔ "particule"
Elementum ➔ "élément"
Nodus ➔ "nœud"
Structum serait magnifique si tu veux évoquer un élément de construction sans égalité : on sent qu'il participe d'une structure, mais sans devoir être égal à un autre.
Veux-tu que je te propose aussi des compositions originales (comme des mots composés latins) pour créer un mot vraiment unique ?
Un élément dans un langage logique ne contenant pas le prédicat d'égalité pourra s'appeller un élémentum si on souhaite rappeler que sa définition est faite sans l'usage du prédicat d'égalité. Considérons par exemple le modèle suivant où le prédicat d'égalité n'existe pas :
`{A("."),B(".,.")}"<"f("."),g(".,."),a,b">"`
C'est une algèbre libre engendrée par f("."),g(".,."),a,b et sur laquelle on a défnit deux prédicats A("."),B(".,."). L'absence du prédicat d'égalité nous interdit de vouloir quotienter la structure. Considérons l'énoncé `EEc, A(f(c))`. En se plaçant dans la portée de cette déclaration de variables existancielle on procède à une extension du langage par l'ajout de l'élément `c` et par l'ajout au système de démonstration de l'axiome `A(f(c))`, créant une algèbre libre engendrée par `f("."),g(".,."),a,b,c`.
Puis on introduit une égalité en procédant par plusieurs étapes. La première étape est l'égalité informatique `≝` s'appliquant à une nouvelle variable définie de façon unique. Par exemple :
`EEe, e≝g(a,b)`
C'est une déclaration d'une nouvelle variable `e`, et cela ajoute au système de démonstration la possibilité de substituter la variable `e` par `g(a,b)` dans toutes les formules.
---- 27 avril 2024 ----
En logique du premier ordre, il est impossible de définir l'infini. Aucune preuve du premier ordre 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 variables désignant des prédicats, comme suit :
`EEA("."),`
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 tous les éléments `x` tel que `A(x)`, et un second tous les éléments `y` tel que `"¬"A(y)`. C'est à dire quelque chose qui s'apparente à un ensemble et à son complément, mais qui est plus générale qu'un ensemble puisque nous n'avons posé aucune théorie concernant le prédicat `A` autre que sa déclaration, `EEA(".")`.
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 d'élément. 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 générateurs, les prédicats générateurs, 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.
Il est à noter que cette deuxième classe de variable est incluse dans la première classe, puisque par principe l'élément peut tout désigner. 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 à un élément. Le terme `A` désignera l'élément qui désigne le prédicat `A(".")` . Le terme `A(A)` désignera le prédicat `A` appliqué à l'élément désignant le prédicat `A`.
Il convient à chaque fois de vérifier si l'extension du langage ne crée pas d'ambiguité. Et ici il peut y avoir des ambiguités avec les prédicats nullaires et aussi avec les prédicats d'arité variables.
Ainsi nous pouvons procéder à cette extension du langage, transformant par exemple le modèle :
`{A("."),B(".,.")}"<"f("."),g(".,."),a,b">"`
en ce modèle :
`{A("."),B(".,.")}"<"f("."),g(".,."),a,b,A,B">"`
Cela revient à faire à chaque fois que l'on étend le langage en ajoutant un prédicat non-nullaire, à ajouter un élément de même nom. Exemple :
`EEB(".,."), EEB`
Mais cette extension n'est pas limitée qu'aux seuls prédicats générateurs, elle s'applique à tous les prédicats définissables. Exemple :
`P(x,y) ≝ EEz, AAt, B(g(x,z),g(y,t))`
La définission de P(".,.") constitue une déclaration d'un nouveau prédicat, et ajoute au système de démonstration la substitution unification dans toute formule de `P("e_1,e_2")` par la formue `EEz, AAt, B(g(e_1,z),g(e_2,t))`. Et elle ajoute l'élément `P` comme élément générateur.
Mais cette extension n'est pas limité aux seuls prédicats définissables, elle s'applique à tous les nouveaux prédicats, qui sont identique à des prédicats générateurs apparaissant dans un nouveau contexte. La boucle est ainsi bouclée. Exemple :
`EE P(".,."), AAx,EEy,B(P(x,y),P(y,x))`
La déclaration de P(".,.") constitue une déclaration d'un nouveau prédicat, et ajoute au système de démonstration l'axiome `AAx,EEy,B(P(x,y),P(y,x))`. Et elle ajoute l'élément `P` comme élément générateur.
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 non-nullaire comme le foncteur non-nullaire sont de possibles éléments, puisque par principe l'élément peut tout désigner, et que le choix de pouvoir les exprimer semble être notre première construction.
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`. Le prédicat 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`. Le foncteur appliqué à l'élément doit toujours s'arrêter en un temps fini, et retourner sur le ruban une transcription d'un élément. 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 une approche des mathématiques par la calculabilité, où l'on agrandit 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.
Commençons sans le prédicat d'égalité, par étabir les premiers niveaux de construction des élèmentums.
On définit un premier niveau de construction permettant de construire de nouveaux élèmentum, par composition close de foncteurs, c'est le domaine de Herbrand.
On définit un second 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 troisième niveau de construction. Le foncteur pourra se noter explicitement en déclarant ses arguments aux travers de variables muettes. Exemples de nouveaux foncteurs :
`(x,"*"x) "|" h(x,"*"x)`
`x "|" g(x,a)`
`x "|" f(f(x))`
`(x,y) "|" g(x,f(y))`
`(x,y,"*"x) "|" h(x,a,y,b,"*"x)`
Dans ce troisième niveau, on définit l'égalité informatique, une égalité entre programme. Cela est possible car cette égalité est un prédicat calculable. Exemples :
`f(".") = `x "|" f(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),`
---- 27 avril 2025 ----
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 ----