Les connecteurs booléens peuvent tous être définis avec seulement le connecteur d'implication `"→"` et le connecteur de négation `"¬"` :
Pour réduire le nombre de parenthèses nécessaires, on attribue une priorité syntaxique plus forte pour la négation.
On désigne la proposition tautologique par le symbole `"⊤"` qui ressemble à la première lettre de Tautologie, et qui évoque le ciel, la plus haute valeur logique, le vrai. Tandis que sa négation est représentée par le symbole `"⊥"` qui évoque le sol, la plus basse valeur logique, le faux.
Grammaire :
`sfV ← {x_1,x_2,x_3,...}`
`sfP ← {sfV,"¬"sfP, sfP"→" sfP}`
Le symbole `"←"` définit un ensemble par une inclusion pouvant être réccurcive, et comprenant des opérations qui s'emboitent. Les parenthèses sont donc nécessaires autours de chaque composition. Mais la plus part d'entre-elles sont supprimées par des règles de priorité syntaxique. Ces inclusions récursives d'ensembles forment une grammaire.
La grammaire constitue un énumérateur de toutes les propsoitions. Demandons à ChatGPT de programmer un tel énumérateur.
| Les connecteurs booléens peuvent tous être définis avec seulement le connecteur binaire d'implication `"→"` et le connecteur unaire de négation `"¬"`.
On considère les variables booléennes `x_1,x_2,x_3,....` Les propositions sont les compositions closes de connecteurs et de variables. Peut-tu programmer un énumérateur de toutes les propositions (indépendamment de leur valeur logique) ? |
Reflexion durant 20s
Oui. L’idée la plus simple (et “correcte” au sens : chaque proposition apparaîtra un jour) est d’énumérer par taille (par exemple : nombre de connecteurs) en parcours en largeur. On construit toutes les formules ayant exactement c connecteurs, à partir de celles qui en ont moins :
Comme il y a une infinité de variables `x1, x2, ...,` on les “injecte” progressivement : par exemple, on introduit `x_{c+1}` à la taille `c`. Ainsi, chaque variable finit par apparaître. Voici un énumérateur Python infini (générateur) : ---- premier essai ---- |
Pour la taille `c"="0`, le programme énumère :
Pour la taille `c"="1`, le programme énumère :
|
| Tu as raison : avec ma convention j’introduis `x_{c+1}` à la taille `c`, `x_2` n’est pas considéré comme une formule de taille `0` au moment où on construit la taille `1`, donc on ne peut pas fabriquer `¬(x_2)` ni les implications qui l’utilisent.
La bonne façon (classique) de gérer l’infinité des variables est de faire du dovetailing (énumération en diagonale) : Étape `s = 1,2,3,...` On fixe un ensemble fini de variables `V_s "=" {x_1, ..., x_s}` On énumère toutes les formules de taille `c "≤" s` construites sur `V_s` Et on fait ça pour `s` croissant : ainsi toute formule finie (qui n’utilise qu’un nombre fini de variables et un nombre fini de connecteurs) apparaîtra à une étape finie. Voici un générateur Python qui fait exactement ça, et qui inclut bien à `c"="1` : `¬(x_2), (x_2→x_1), (x_1→x_2), (x_2→x_2)` (quand `s "≥" 2`). Télécharger enumerateur.py |
Pour expérimenter le programme python, il faut installer python3 comme indiqué ici : python
Le système de Hilbert propose 4 règles de productions pemettant de construire toutes les tautologies. On présente le système de Hilbert sous la forme d'une sorte de grammaire perfectionnée :
`|-- a"→"(b"→"a)` `|-- (a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))`
`|-- (¬a"→"¬b) "→"(b"→"a)`
`a, a"→"b |-- b`
Le symbole `"⊢"` , de priorité syntaxique la plus faible, définit une règle de déduction assujettie à la véracité des hypothèses énumérées à sa gauche.
La priorité syntaxique des connecteurs est la suivante, de la plus forte à la plus faible :
`"¬", "→", "virgule", "⊢"`
Notez que les nouvelles variables libres placées à droite du symbole `"⊢"` et qui n'ont pas d'occurrences à gauche, peuvent prendre comme valeur globale toutes les propositions qu'elles soient vrais ou fausses.
La dernière règle, appelée le modus ponens, joue un rôle particulier.
---- 3 mars 2026 ----
La déduction naturelle propose également 4 règles pemettant de construire toutes les tautologies. Ces règles sont basées sur l'introduction et l'élimination des connecteurs du langage. On présente le système de déduction naturelle sous la forme d'une sorte de grammaire encore plus perfectionnée :
`(a|--b) |-- a"→"b` `a, a"→"b |-- b`
`a"→ ⊥" |-- "¬"a`
`a, "¬"a" |-- "⊥"`
# Introduction de l'implication. # Élimination de l'implication.
# Introduction de la négation.
# Élimination de la négation.
L'introduction de l'implication `(a|--b) |-- a"→"b` a comme prémisse, une sous-preuve `a|--b` qui commence par une supposition `a`. Ce qui rend la déduction naturelle plus complexe que le système de déduction d'Hilbert. À tout endroit d'une preuve ou d'une sous-preuve il est possible de commencer une sous-sous-preuve commençant par une supposition dans le but d'établire une sous-sous-preuve, et ainsi de suite.
À titre d'exemple, voyant à quoi ressemble la preuve formelle de la règle de la contraposé :
`a"→"b |-- "¬"b"→¬"a`
Preuve :
| Supposons `a"→"b` | `{a"→"b}` | |
| Supponsons `a` | `{a, a"→"b}` | |
| R2 : `a, a"→"b |-- b` | `{a, b, a"→"b}` | `{a|--b}` |
| R4 : `b, "¬"b" |-- "⊥"` | `{ "⊥",a, b, a"→"b}` `{a|--"⊥",a|--b}` | `{ "⊥",a, b, a"→"b}` `{a|--"⊥",a|--b}` |
| R1 : `a|--"⊥" |-- a"→⊥"` | ||
---- 11 janvier 2026 ----
Supposons `"¬"b`
Supponsons `a`
R2 : `a, a"→"b |-- b`
R4 : `b, "¬"b" |-- "⊥"`
R1 : `a"→ ⊥" |-- "¬"a`
R1 : `a"→ ⊥" |-- "¬"a`