Le calcul des prédicats

1) Introduction

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 la théorie de la démonstration découle de la théorie de la calculabilité. On construit canoniquement un langage suffisament riche pour atteindre le domaine de calculabilité d'une machine de Turing, et on en fait un langange des démonstrations.

2) Logique des prédicats

La logique du premier ordre introduit un premier type de variable dite élémentaire, non limitée, susceptible de désigner toute chose, et encore, le terme de chose est trop limitatif. 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 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 :

`overset("Booléen")(EEX), P(X)`    s'écriera    `P(0) "ou" P(1)`

`overset("Booléen")(AAX), 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 peut ê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érale 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.

2.1) Domaine de Herbrand

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)}`

2.2) Modèle

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.

3) Système de démonstration en logique du premier ordre

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 : Étape Formule Raison 1 `"¬"(∀x,P(x))`  Hypothèse 2 Supposons `"¬"(∃x,"¬"P(x))`  Supposition pour l'absurde 3 `∀x,"¬¬"P(x)`  Par définition de la négation de l'existentiel 4 `∀x,P(x)`  Élimination de la double négation 5 Contradiction entre (1) et (4) Contradiction 6 `∃x,"¬"P(x)`  Par l'absurde 7 `"¬"(∀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 : Étape Justification `"¬"(∃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. Posons-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)))​` 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 ?

 

 

Utilise une autre hypothèse qui est : `∀x,R(x,s(x))` où `s` est un foncteur unaire.

Très bonne idée ! Avec l’hypothèse : `∀x,R(x,s(x))` où `s` est un foncteur unaire, on peut démontrer que si `R` est symétrique et transitive, alors `R(x,x)` pour tout `x`. Autrement dit, on peut démontrer : Formule à démontrer    `(∀x,R(x,s(x))∧∀x∀y,(R(x,y)→R(y,x))∧∀x∀y∀z,((R(x,y)∧R(y,z))→R(x,z)))→∀x,R(x,x)`   Intuition Pour chaque `x`, on sait : `R(x,s(x))` par hypothèse directe, donc `R(s(x),x)` par symétrie, donc `R(x,x)` par transitivité entre `R(x,s(x))` et `R(s(x),x)`. Cette preuve fonctionne pour chaque `x`, donc on pourra conclure `∀x,R(x,x)`. Démonstration formelle (style Hilbert) On va démontrer :    `⊢(∀x,R(x,s(x))∧∀x∀y,(R(x,y)→R(y,x))∧∀x∀y∀z,((R(x,y)∧R(y,z))→R(x,z)))→∀x,R(x,x)` Étapes numérotées Étape Formule Justification 1 `∀x,R(x,s(x))`  Hypothèse 2 `∀x∀y,(R(x,y)→R(y,x))`    3 `∀x∀y∀z,((R(x,y)∧R(y,z))→R(x,z))`    4 Fixons une variable arbitraire `x` Pour généralisation ultérieure 5 `R(x,s(x))`  `∀`-élimination sur (1) 6 `R(s(x),x)`  `∀`-élimination sur (2), puis modus ponens avec (5) 7 `(R(x,s(x))∧R(s(x),x))→R(x,x)`  `∀`-élimination sur (3) avec x,s(x),x 8 `R(x,s(x))∧R(s(x),x)`  Conjonction de (5) et (6) 9 `R(x,x)`  Modus ponens sur (7) et (8) 10 `∀x,R(x,x)`  `∀`-introduction sur (9), x arbitraire 11 Conclusion finale Déduction conditionnelle des lignes (1–3) vers (10) ✅ Conclusion La formule :    `(∀x R(x,s(x))∧∀x∀y (R(x,y)→R(y,x))∧∀x∀y∀z ((R(x,y)∧R(y,z))→R(x,z)))→∀x R(x,x)` est démontrable dans le système Hilbertien du premier ordre. Souhaites-tu maintenant que je la formalise complètement avec une numérotation plus rigoureuse (comme une vraie preuve ligne par ligne) ou qu’on la traduise en notations de type Fitch (sous-forme indentée) ?

 

---- 1 mai 2025 ----

.