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, pour déclarer ces prédicats, 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é. On construit canoniquement un langage du second ordre suffisament riche pour atteindre le domaine de calculabilité d'une machine de Turing, et pour pouvoir 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, susceptible de désigner toute chose. Et pour introduire ces éléments dans le calcul propositionnel qui est un calcul booléen, il est nécessaires d'introduire des prédicats qui transforment les éléments en booléens, Et pour créer une infinité d'autres éléments, il est nécessaire d'introduire des foncteurs qui transforment les éléments en d'autres éléments.
On représentera les variables booléennes souvent en majuscule et les variables élémentaires souvent en minuscule. Mais ce qui déterminera leur type sera l'usage du quantificateur `EE` ou `AA` qu'on ne réservera aux éléments et non aux booléens. Pour les bouléens, le quantificateur existentiel est remplacé par la disjonction, et le quantificateur universelle est remplacé par la conjonction :
`EEX "Booléen", P(X)` s'écriera `P(0) "ou" P(1)`
`AAX "Booléen", P(X)` s'écriera ` P(0) "et" P(1)`
Où `"Booléen"` qualifie le type de la variable `X`, et où la fonction `P(".")` désigne une formule quelconque de la logique des prédicats possédant une variable booléenne libre.
Les prédicats seront souvent notés en majuscule, comme le sont les variables booléennes qui constituent des prédicats nullaires. Les foncteurs seront souvent notés en minuscule, 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é. Et l'absence de suffixe dénote l'arité nullaire c'est à dire 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 représenté par un terme de type séquence est autorisée et placée toujours en fin de séquence pour des raisons propre à l'unification.
Une séquence d'éléments comprend une succession finie de variables éléments se terminant éventuellement par une variable séquence d'élément. la séquence puet être vide. La séquence peut ne contenir qu'un seul élément auquel cas la séquence est cet élément. Il y a donc un deuxième type de variable plus générlae que le type élément qu'est la séquence 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 séquence, ne pouvant se placer qu'au dernier terme d'une séquence, 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. À 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 de 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 étant considéré comme déterminant ses propres valeurs booléennes, le modèle est donc défini par les prédicats générateurs.
Les bases du raisonnement logique du premier ordre sont connues. Posons la question à ChatGPT 4o :
En logique mathématique, peux-tu décrire le système de démonstration de la logique du premier ordre ? Bien sûr ! Voici une description claire et structurée du système de démonstration de la logique du premier ordre :
1. Éléments de base
La logique du premier ordre (aussi appelée logique des prédicats) manipule :
- Symboles logiques :
- Connecteurs : `∧` (et), `∨` (ou), `→` (implique), `¬` (non)
- Quantificateurs : `∀` (pour tout), `∃` (il existe)
- Parenthèses pour structurer les formules
- Symboles non logiques :
- Variables : `x, y, z`, etc.
- Fonctions : `f, g`, etc. (avec un nombre fixé d'arguments)
- Constantes : `a, b`, etc.
- Prédicats : `P, Q`, etc. (avec un nombre fixé d'arguments)
Une formule est une combinaison finie de ces symboles, construite selon des règles précises.
2. Axiomes
Le système de démonstration repose sur un ensemble d'axiomes (formules considérées comme valides sans preuve). Typiquement, il y a :
Axiomes logiques : par exemple, des schémas d'axiomes comme
- `A"→"(B"→"A)`
- `(A"→"(B"→"C))"→"((A"→"B)"→"(A"→"C))`
- `("¬"A"→""¬"B)"→"(B"→"A)`
Axiomes pour les quantificateurs :
- `(∀x,A(x))→A(t)`
(si `∀x,A(x)` est vrai, alors `A(t)` est vrai pour n'importe quel terme `t`)
- `A(t)→∃x,A(x)`
Ces axiomes peuvent varier légèrement selon le système choisi (Hilbert, Gentzen, etc.).
3. Règles d'inférence
Ce sont les mécanismes permettant de déduire de nouvelles formules à partir de formules déjà établies.
- Règle de modus ponens (MP) :
- Si `A` et `A→B` sont démontrés, alors `B` est démontré.
- Règles pour les quantificateurs :
- Généralisation universelle : Si `A(x)` est démontré, et `x` n'apparaît pas libre dans une hypothèse, alors `∀x,A(x)` est démontré.
- Existentialisation : Si `A(t)` est démontré pour un terme `t`, alors `∃x,A(x)` est démontré
4. Définition d'une démonstration
Une démonstration (ou preuve) est une séquence finie de formules, où chaque formule est :
- Un axiome, ou
- Obtenue par application d'une règle d'inférence à des formules précédentes de la séquence.
Si on peut construire une telle séquence qui aboutit à une formule `A`, on dit que `A` est démontrable.
Notation : souvent on écrit `⊢A` pour dire "`A` est démontrable".
5. Commentaires
Ce type de système est syntaxique : il manipule des symboles selon des règles formelles, sans référence au "sens" ou à la "vérité" des formules.
Il est conçu pour capturer les inférences valides en sémantique : idéalement, si `"⊢"A`, alors `A` est vrai dans tous les modèles.
Dans les années 1930, Gödel a prouvé que ce type de système est complet pour la logique du premier ordre : toute formule valide est démontrable.
Hum... cela semble incomplet, le mécanisme d'unification n'est pas vraiment décrit. Voyons comment il applique ce qu'il dit. Demandons-lui de faire une démonstration toute simple.
Démontre dans ce système `"¬"(∀x,P(x)) "→" (∃x,"¬"P(x))` Parfait, allons-y étape par étape !
On veut démontrer dans un système de type Hilbert :
`"¬"(∀x,P(x))"→"(∃x,"¬"P(x))`
On va utiliser uniquement :
- des axiomes logiques,
- les axiomes pour les quantificateurs,
- modus ponens.
Stratégie :
- Supposons `"¬"(∀x,P(x))`.
- Montrons que `∃x,"¬"P(x)` suit.
En intuition : Si ce n’est pas vrai que `P(x)` pour tout `x`, alors il existe au moins un `x` pour lequel `P(x)` est faux.
Démonstration détaillée :
1. Utilisons le raisonnement par l'absurde (c'est une technique standard en Hilbert) :
On va supposer le contraire de ce que l'on veut prouver et arriver à une contradiction.
Supposons :
- `"¬"(∀x,P(x))` [hypothèse]
- `"¬"(∃x,"¬"P(x))` [on suppose que la conclusion est fausse]
2. Utilisons la logique classique :
On sait que :.
`"¬"(∃x,"¬"P(x))≡∀x,"¬¬"P(x)`
(ça vient de la négation du quantificateur existentiel : ` "¬"(∃x,A(x))≡∀x,"¬"A(x)`
Donc `"¬"(∃x,"¬"P(x))` implique `∀x,"¬¬"P(x)`.
Mais en logique classique, la double négation donne :
`"¬¬"P(x)≡P(x)`
Donc :
`∀x,P(x)`
Donc on a obtenu `∀x,P(x)`.
3. Contradiction :
On a :
D'une part `"¬"(∀x,P(x))` (hypothèse)
D'autre part `∀x,P(x)` (conclusion intermédiaire)
Contradiction !
Donc notre hypothèse `"¬"(∃x,"¬"P(x))` est fausse, c’est-à-dire que :
`"∃"x,"¬"P(x)`
Donc :.
`"¬"(∀x,P(x))"→"(∃x,"¬"P(x))`
est démontré.
Résumé de la preuve formelle :
`"¬"(∀x,P(x))` Hypothèse Supposons `"¬"(∃x,"¬"P(x))` Supposition pour l'absurde `∀x,"¬¬"P(x)` Par définition de la négation de l'existentiel `∀x,P(x)` Élimination de la double négation Contradiction entre (1) et (4) Contradiction `∃x,"¬"P(x)` Par l'absurde `"¬"(∀x,P(x))"→"(∃x,"¬"P(x))` Déduction Veux-tu aussi que je te l'écrive sous forme 100 % hilbertienne avec uniquement axiomes + modus ponens, étape par étape comme sur une vraie copie de logique formelle ?
(Ça peut être un peu plus long mais hyper rigoureux !)
Montre comment en utilisant les règles d'inférences (règles pour les quantificateurs) tu peux démontrer `"¬"(∃x,P(x)) "→" ∀x,"¬"P(x)` Super demande ! Tu veux voir comment utiliser vraiment les règles d'inférence pour démontrer :
`"¬"(∃x,P(x))"→"∀x,"¬"P(x)`
en logique du premier ordre.
Ici, on va utiliser :
- Modus ponens (MP),
- Règles d'inférence sur les quantificateurs :
- Existentialisation : de `A(t)` on peut déduire `∃x,A(x)`,
- Généralisation : de `A(x)` on peut déduire `∀x,A(x)` sous certaines conditions.
Plan d'attaque :
Supposons `"¬"(∃x,P(x))` et montrons que pour tout `x`, `"¬"P(x)`.
On doit donc démontrer `∀x,"¬"P(x)`, c’est-à-dire montrer que pour un `x` arbitraire, `"¬"P(x)`.
Démonstration en étapes :
- Hypothèse :
- `"¬"(∃x,P(x))` (hypothèse)
- Fixons une variable arbitraire `x_0` (un "`x`" quelconque).
- Montrons que `"¬"P(x_0)` :
- Supposons, pour obtenir une contradiction, que `P(x_0)`.
- Alors, par la règle d'existentialisation, on pourrait en déduire `∃x,P(x)` (puisque s’il existe un `x` qui satisfait `P`, alors `∃x,P(x)` est vrai).
- Mais on a `"¬"(∃x,P(x))` par hypothèse !
- Donc, contradiction.
- Conclusion : `"¬"P(x_0)`
- Puis : Par généralisation universelle, puisque `x_0` était arbitraire, on peut conclure `∀x,"¬"P(x)`.
- Donc : `"¬"(∃x,P(x))"→"∀x,"¬"P(x)`
Résumé proprement :
`"¬"(∃x,P(x))` Hypothèse Supposons un `x_0` arbitraire Supposons `P(x_0)` (pour l'absurde) Alors `∃x,P(x)` par existentialisation Contradiction avec `"¬"(∃x,P(x))` Donc `"¬"P(x_0)` Puis par généralisation : `∀x,"¬"P(x)` Conclusion : `"¬"(∃x,P(x))"→"∀x,"¬"P(x)` En langage plus formel avec les symboles :
- `"¬"(∃x,P(x))` (hypothèse)
- Fixe un `x`
- Suppose `P(x)`
- `P(x)"⇒"∃x,P(x)` (existentialisation)
- Contradiction avec `"¬"(∃x,P(x))`
- Donc `"¬"P(x)`
- Donc `∀x"¬"P(x)`
Veux-tu que je te fasse aussi une preuve encore plus stricte en style ultra-formel (avec numérotation ligne par ligne, à la manière d'un système Hilbert pur ou Fitch) ?
Ça te donnerait une idée ultra précise de comment ça se déroule dans un système automatique.
Mais on ne voit toujours pas le mécanisme d'unification mis en oeuvre. Possons-lui une question nécessitant cette unification.
Démontre dans ce système `(∀x,P(f(x)))→Ax,P(f(g(x)))` où `f` et `g` sont des foncteurs du langage. Excellente question ! On va démontrer dans un système de logique du premier ordre (style Hilbert, avec règles d’inférence pour les quantificateurs) la formule suivante :
`(∀x,P(f(x)))→∀x,P(f(g(x)))`
où :
- `f` et `g` sont des foncteurs (fonctions unaires ici),
- `P` est un prédicat unaire.
Intuition
Ce qu’on dit ici, c’est :
Si tous les `x` vérifient `P(f(x))`,
Alors tous les `x` vérifient `P(f(g(x)))`.
Cela revient à dire que, pour tout `x`, si `P(f(x))` est vrai en général, alors il l’est aussi pour tout `g(x)`, parce que `g(x)` est une expression valide du langage.
La clé est de remplacer la variable dans `∀x,P(f(x))` par un terme construit, ici `g(x)`.
Stratégie de démonstration
Utilisons :
- L’axiome d’instanciation universelle (ou "élimination du ∀") :
`(∀x,ϕ(x))→ϕ(t)`
pour n'importe quel terme fermé tt.
- Puis la généralisation universelle (ou "introduction du ∀") :
Si ` ϕ(x)` est prouvée sans hypothèse sur `x`, alors on peut conclure `∀x,ϕ(x)`.
✍️ Preuve étape par étape
On va démontrer :
`(∀x,P(f(x)))→∀x,P(f(g(x)))`
Étapes :
- Supposons `∀x,P(f(x))`
(hypothèse)
- On instancie `∀x P(f(x))` avec le terme g(x) :
Par instanciation universelle, on obtient :
`P(f(g(x)))`
- Comme `x` est arbitraire, on peut généraliser :
`∀x,P(f(g(x)))`
- Donc :
`∀x,P(f(x))→∀x,P(f(g(x)))`
✅ Conclusion
∀x P(f(x))→∀x P(f(g(x)))
∀xP(f(x))→∀xP(f(g(x)))est démontrable dans la logique du premier ordre, en utilisant uniquement :
l’instanciation universelle,
la généralisation universelle.
Souhaites-tu que je t’écrive cette démonstration sous forme formelle numérotée, avec les règles explicites à chaque ligne comme dans un système Hilbert ou Fitch ?
---- 1 mai 2025 ----
Formalisons le système de démonstration en créant un langage adapté et écrivons l'algorithme du démonstrateur automatique tatonnant au hasard.
---- 30 avril 2025 ----
nous allons formaliser un système de démonstration mais en partant d'une hypothèse plus simple où le prédicat d'égalité n'existe pas.
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 ----