La logique propositionnelle classique donne à toute proposition une valeur logique vrai ou faux, et utilise comme connecteurs, les opérations booléennes. On désigne le vrai, la valeur booléenne `1`, par le symbole `"⊤"` qui ressemble à la première lettre de « Tautologie », et qui évoque le ciel, la plus haute valeur logique. Tandis que sa négation, le faux, la valeur booléenne `0`, est représentée par le symbole de l'antilogie `"⊥"` qui évoque le sol, la plus basse valeur logique.
Les connecteurs les plus utiliseées sont `"¬", "∧","∨","→","↔"`. Chaque connecteur étant une opération booléenne, il est dit booléens, et il est défini par sa table de vérité :
booléenne
`"¬"1=0`
`0"∧"1=0`
`1"∧"0=0`
`1"∧"1=1`
`0"∨"1=1`
`1"∨"0=1`
`1"∨"1=1`
`0"→"1=1`
`1"→"0=0`
`1"→"1=1`
`0"↔"1=0`
`1"↔"0=0`
`1"↔"1=1`
Lorsque l'on étend la logique propositionnelle en la logique du premier ordre, en introduisant des éléments, des fonctions, des prédicats, des variables élémentaire et le quantificateur existentiel, le nombre d'éléments existants et le nombre d'inconnus booléens existants devient infini. La table de vérité ne peut plus être utilisée pour calculer la valeur logique d'une formule. C'est pourquoi, les logiciens proposent une autre façon de calculer la valeur logique d'une proposition. Ils proposent un procédé récurcif de production de toutes les propositions tautologiques, un procédé qui peut s'appliquer au delà des seuls formules propostionnelles, pour être appliqué aux formules de la logique du premier ordre.
Le premier système de production des propositions tautologiques proposé, appellé aussi système de démonstration ou système de déduction, est celui de Hilbert. Il commence par simplifier le problème en démontrant que toutes propositions peut s'écrire qu'avec deux seuls connecteurs booléens que sont l'antilogie `"⊥"` et le connecteur d'implication `"→"`. En effet, il est facile de constater que les connecteurs booléens peuvent tous être définis avec seulement l'antilogie `"⊥"` et le connecteur d'implication `"→"` :
La vérification de ces équivalences se fait en utilisant les tables de vérité, c'est à dire en calculant les valeurs booléennes pour chaque configuration de paramètres booléens. Le langage initial de la logique propositionnelle choisi par Hilbert est donc très simplifié, défini par la grammaire suivante :
`sfV = {"⊥", x_1,x_2,x_3,...}`
`sfP = {sfV, (sfP"→" sfP)}`
La grammaire se définit par une sorte d'inclusion récurcive d'ensembles. La grammaires construit des emboitements de la forme `(x"→"y)`. Ainsi, chaque proposition est un arbre binaire où chaque noeud correspond à une implication et où chaque feuille porte comme étiquette le nom d'une variable ou le symbole de l'antilogie.
Le système de Hilbert propose 4 règles de production de propositions, pemettant de produire exactement toutes les propositions tautologiques.
`"R1"` : `|-- a"→"(b"→"a)` `"R2"` : `|-- (a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))`
`"R3"` : `|-- ((a"→⊥")"→"(b"→⊥")) "→"(b"→"a)`
`"R4"` : `a, a"→"b |-- b`
Le symbole `"⊢"` , de priorité syntaxique la plus faible, définit une règle de production assujettie à la production des hypothèses énumérées à sa gauche, et où les nouvelles variables libres placées à droite du symbole `"⊢"` et qui n'ont pas d'occurrences à gauche, peuvent prendre comme valeur toutes les propositions qu'elles soient vrais ou fausses.
La priorité syntaxique des connecteurs est la suivante, de la plus forte à la plus faible :
`"virgule"` `"⊢"`
La quatrième règle `R4` est appelé le « modus ponens » que l'on désigne parfois par le nom `"MD"`.
On définit la négation juste comme une réécriture :
`"¬"x := x"→⊥"`
Le troisième axiome peut alors se réécrire :
`"R3"` : `|-- ("¬"a"→¬"b) "→"(b"→"a)`
Mais il est judicieux de ne pas introduire ce connecteur, afin que les propositions soit toujours de cette forme particulièrement simple d'arbre binaire où les feuilles ont comme étiquette soit le nom d'une variable ou soit le symbole de l'antilogie. Ainsi chaque fois que sera écrit `"¬"x` il faudra lire `x"→⊥"`.
Pour démontrer qu'un tel système produit bien toutes les propositions vrai selon le calcul booléens et uniquement celles-ci, on recourt à la récurrence. Etant donnée deux propositions `p, q` tel que le système produit soit `p` ou bien soit `"¬"p`, et aussi `q` ou bien `"¬"q`, alors nous démontrerons que le système produit `p"→"q` ou bien `"¬"(p"→"q)` selon le cas logique définit par l'hypothèse. Le langage propositionnelle `sfP` étant définit par ce seul procédé de construction comme l'indique sa grammaire, `sfP = {sfV, (sfP"→" sfP)}` et `sfV = {"⊥", x_1,x_2,x_3,...}`, nous aurons démontré ainsi que pour toute proposition, le système de Hilbert produit forcement, soit la proposition, ou soit sa négation.
Cela consiste concrètement à montrer que le système de Hilbert engendre les `4` règles de déductions suivantes :
`p,"¬"q |-- "¬"(p"→"q)`
`"¬"p,q |--p"→"q`
`"¬"p,"¬"q |-- p"→"q`
Puis, pour prouver que le sytsème de Hilbert produit seulement les propositions tautologiques, il suffit de vérifier en utilisant la table de vérité de l'implication que chaque règle `"R1"`, `"R2"`, `"R3"`, `"R4"` appliqué à des prémisses de valeur booléenne `1`, produisent des propositions de valeur booléenne `1`.
La démonstration est triviale :
`"R1"` : `|-- q"→"(p"→"q)`
`"R4"` : `q, q"→"(p"→"q) |-- p"→"q`
La démonstration est la même :
`"R1"` : `|-- q"→"(p"→"q)`
`"R4"` : `q, q"→"(p"→"q) |-- p"→"q`
Posons la question à ChatGPT 5.3 :
Peut-tu démontrer `p"→"q` en utilisant seulement `"R1", "R2", "R3", "R4"` et la connaissance de `p,"¬"q` ? |
|||||||||||||||
Oui. Et on peut même le faire très simplement : la connaissance de `"¬"q` n’est pas nécessaire ; `"¬"p` suffit. Preuve condensée
|
La démonstration est beaucoup plus complexe...., mais ChatGPT 5.3 est peut-être capable de la trouver, et il constitue un excellent professeur capable de s'adapter aux choix de notations qu'on lui propose :
| Le système de démonstration à la Hilbert comprend `4` règles de production de propositions, permettant de produire exactement toutes les propositions tautologiques. `"R1"` : `⊢ a"→"(b"→"a)` `"R2"` : `⊢(a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))` `"R3"` : `⊢("¬"a"→¬"b) "→"(b"→"a)` `"R4"` : `a, a"→"b ⊢ b` Le symbole `"⊢"`, de priorité syntaxique la plus faible, définit une règle de production assujettie à la production des hypothèses énumérées à sa gauche, et où les nouvelles variables libres placées à droite du symbole `"⊢"` et qui n'ont pas d'occurrences à gauche, peuvent prendre comme valeur toutes les propositions qu'elles soient vrais ou fausses. La priorité syntaxique des connecteurs est la suivante, de la plus forte à la plus faible : `"¬ | → | , | ⊢"`. |
Oui. Avec tes conventions, on peut reformuler cela proprement comme un système de production de formules démontrables de la logique propositionnelle classique.
1. Les objets manipulésOn part d’un langage propositionnel formé à partir :
Les formules sont engendrées récursivement par :
Avec ta convention de priorité :
donc par exemple
se lit bien comme
2. Sens du symbole `"⊢"`Dans ce cadre, `"⊢"` ne fait pas partie des formules du langage objet ; c’est un symbole métathéorique qui décrit une règle de production.
Autrement dit, une démonstration est une suite finie de formules où chaque ligne est obtenue :
3. Les trois schémas d’axiomesLes règles `"R1","R2","R3"` sont mieux vues comme des schémas d’axiomes :
Pour toutes formules `a,b` on peut produire directement `a→(b→a)`. Exemple : en prenant `a"="x_1, b"=¬"x_2`, on obtient `⊢x_1"→"("¬"x_2"→"x_1)`.
Pour toutes formules `a,b,c`, on peut produire directement cette formule. C’est le schéma qui formalise la composition des implications.
Pour toutes formules `a,b`, on peut produire directement cette formule. C’est une forme de contraposée classique. C’est ce schéma qui donne au système son caractère classique. La règle d'inférence `"R4"`
Elle signifie : si `a` a déjà été produit, et si `a"→"b` a déjà été produit, alors on peut produire `b`. C’est l’unique vraie règle de déduction du système. Exemple :
alors par `"R4"`, on obtient `⊢x_2"→"x_1` 5. Variables libres dans les schémasQuand tu écris `a,b,c` dans `"R1","R2","R3"`, ce ne sont pas des variables propositionnelles du langage objet, mais des métavariables. Elles parcourent toutes les formules du langage. Donc `"R1"` ne produit pas une seule formule, mais une infinité de formules, une pour chaque choix de `a` et `b`. Par exemple, toutes les formules suivantes sont des instances de `"R1"` : `⊢ x_1"→"(x_2"→"x_1)`
`⊢ "¬"x_3"→"((x_1"→"x_4)"→¬"x_3")` `⊢ (x_1"→¬"x_2)"→"(("¬"x_4"→"x_5)"→"(x_1"→¬"x_2))"` 6. Ce que produit exactement le systèmeLe système engendre l’ensemble des théorèmes de la logique propositionnelle classique exprimée avec `"¬"` et `"→"`. Autrement dit :
On dit que le système est :
7. Différence entre “proposition” et “proposition démontrable”Il faut distinguer :
Par exemple :
Donc les 4 règles ne produisent pas toutes les propositions du langage, mais toutes les propositions démontrables, c’est-à-dire exactement les tautologies. 8. Définition possible d’une démonstration hilbertienneUne démonstration d’une formule `p` est une suite finie de formules
telle que pour chaque `i`, la formule `f_i` est :
Et si `f_n"="p`, alors on écrit :
(Notez que dans cette expression, `p` n'est pas une variable libre et doit être ramplacé par la tautologie démontrée c'est à dire la formule désignée par `f_n`.) 9. Exemple classique : démontrer `⊢ a "→"a`Cette formule n’est pas un axiome immédiat, mais elle est démontrable. On peut la dériver ainsi :
|
| En sachant les deux propositions, `p`, `"¬"q`, démontre avec ce système de Hilbert la proposition `¬(p"→"q)` | ||||||||||||||||||||||||
| Reflexion durant 2m 32s Oui. On peut le faire proprement dans ton système de Hilbert, en utilisant un lemme dérivé classique. A partir des hypothèse `p`, `"¬"q`, démontrer `¬(p"→"q)`. Lemme dérivé utiliséDans ce système, on peut dériver le schéma de contraposition :
En particulier, en remplaçant `x` par `(p"→"q)` et `y` par `q`, on obtient :
Je l’utiliserai à la ligne 6. DémonstrationOn raisonne sous les hypothèses `p` et `"¬"q`. Étape 1 : obtenir `(p"→"q)"→"q`
Donc, par le théorème de déduction, de `3–4` on conclut :
Etape 2 : utiliser la contraposition
C'est une instance du lemme dérivé
avec `x"="(p"→"q)` et `y"="q`.
Conclusion on a bien démontré `p`, `"¬"q ⊢ ¬(p"→"q)` Version condensée
|
Le théorème de déduction pourrait être défini par la méta-formule suivante :
Le théorème de déduction ne figure pas parmi les règles de production du système de Hilbert. Peut-tu produire le résultat en utilisant seulement `"R1","R2","R3","R4"` et la connaissance de `p,"¬"q` ? |
|||||||||||||||||||||||||||
| Reflexion durant 5m 30s
Oui. Sans utiliser le théorème de déduction comme règle, on peut obtenir le résultat à partir de p,¬q par une suite finie d’applications de R4, à condition d’utiliser deux théorèmes déjà démontrables dans ce système de Hilbert :
Ces deux formules sont des théorèmes du système engendré par `"R1", "R2", "R3", "R4`. Je ne me sers pas ici du théorème de déduction. Démonstration de `"¬"(p"→"q)` à partir de `p,"¬"q`On part des deux connaissances :
On utilise d'abord `"L1"` avec `a":="p` et `b":="q`
Puis `"R4"` avec `2` et `3` :
On réutilise `"L1"`, cette fois avec `a":="(p"→"q)` et `b":="p` :
Cette version ne sert pas directement. La bonne instanciation pour passer de `(p"→"q)"→¬"p` à `"¬"(p"→"q)` est :
qui est encore `"L1"`, avec `a":="(p"→"q)` et `b":=""¬"p`. Par `"R4"` avec `4` et `5` :
On utilise maintenant `"L2"` avec `a":="p` :
Par `"R4"` avec `1` et `7` :
Enfin, par `"R4"` avec `5` et `8` :
Conclusion : on a bien démontré : `p,"¬"q⊢"¬"(p"→"q)` Forme condensée
|
Mais les démonstrations de `"L1"`, `"L2"`, ne sont pas faites et s'avèrent compliquées pour ChatGPT. Il va errer indéfiniment si on ne le guide pas en le faisant procéder par étapes, ou sans lui indiquer d'autres indices.... Les réponses sont similaires avec KIMI. On va lui demander de chercher sur Internet..., et là..., il trouve tout de suite en passant par deux nouveaux lemmes intermédiaires ;
| Cherche sur Internet comment Hilbert démontre
:
`⊢ x"→ ¬¬"x` Puis, transcrit les démonstrations dans notre système de notation. |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Démontrer le lemme de l'identité L1 : `⊢ a "→"a`
Démontrer le lemme de transitivité L2 : `(x"→"y),(y"→"z)⊢x"→"z`
C’est exactement le lemme de transitivité de l’implication dans ce système de Hilbert. DEMONSTRATION DE `⊢ "¬¬"x"→"x`
DEMONSTRATION DE `⊢ x "→¬¬"x`
|
`|-- a"→"(b"→"a)` `|-- (a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))` `|-- ("¬"a"→¬"b) "→"(b"→"a)` `a, a"→"b |-- b`
Les autres connecteurs sont définis comme suit :
`"¬"(b"→¬"a)`
`"¬"b"→"a`
Les alternatives "ou bien" n'ont pas besoin d'être mentionnées car elles sont équivalentes dans le système de Hilbert.
Ayant ainsi définit formellement les règles de déduction exacte et complète concernant le monde fini booléen. On peut alors étendre la logique en introduisant de nouveaux connecteurs non-booléens accompagné de leurs axiomes (des règles de raisonnement spécifique à eux) pour ainsi produire une extension de la logique qui n'est plus booléenne dès qu'un tel connecteur est présent.
---- 28 avril 2024 ----
Pour déterminer si une proposition `P` peut-être produite par les trois premières règles, il suffit de procéder à l'unification parallèle disjonctive de `P` avec les trois tautologies suivantes :
`a"→"(b"→"a)`
`(c"→"(d"→"e))"→"((c"→"d)"→"(c"→"e))`
`("¬"f"→¬"g) "→"(g"→"f)`
Et cela se faite avec une complexité linéaire. On définit ainsi la classe zéro des tautologies. Reste alors l'utilisation du modus ponens `"MP"`. On détermine ainsi la première classe de tautologies, celles produites par le modus ponens appliqué une seul fois à deux tautologies de classe zéro. Pour qu'une proposition appartinennent à la première classe, il ya trois possibilité :
Elle s'unifit à `b"→"a` et `b` est une proposition de classe zéro ou bien `("¬"b"→¬"a) est une proposition de classe zéro
Elle s'unifit à `(c"→"d)"→"(c"→"e) ` et `c"→"(d"→"e)` est une proposition de classe zéro.
Elle s'unifit à `(g"→"f)` et est une proposition de classe zéro.