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.
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.
Pour parfaire la définition, il convient de programmer l'énumérateur correspondant à cette grammaire.
On considère les variables `x_1,x_2,x_3,...` qui seront utilisées dans le langage propositionnel. On considère `F` l'énumérateur de toutes les formules (vrai ou fausse) utilisant ces noms de variables. On considère `F^n` l'énumérateur de tous les `n`-uplets de formules. On considère `G` l'énumérateur de formules suivant :
`G = {`
`(a,b)"≪"F^2`
`a"→"(b"→"a) "≫"`
`(a,b,c)"≪"F^3`
`(a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))"≫"`
`(a,b)"≪"F^2`
`(¬a"→"¬b) "→"(b"→"a)"≫"`
}
`G` énumère toutes les tautologies produtes par les 3 seuls axiomes.
On considère un ensemble `E` initialiement vide qui va accumuler toutes les tautologies produites. A chaque fois que l'on ajoute une ou plusieurs formules dans `E` on regrade tout ce que l'on peut de nouveau produire en appliquant le modus pones avec au moins une de ces nouvelles formules, et on réajoute toutes ces nouvelles produtions pour regarder à nouveau tout ce que l'on peut de nouveau produire en appliquant le modus pones avec au moins une de ces nouvelles formules ajoutées, et ainsi de suite jusqu'à ce qu'il n'y ait plus de formule à ajouter. On consière `H` l'énumérateur des tautologies suivant :
`H = {A|`
`E"="{}`
`{`
`B"="A`
`A"="{}`
`AAy "∈" B, {`
`a"=libre"`
`b"=libre"`
`"si" (y,y)"≈"(a, a"→"b) & b"∉"E & b"∉"A "entonces" b"⇾"A`
`}`
`AAx "∈" E, AAy "∈" B, {`
`a"=libre"`
`b"=libre"`
`"si" (x,y)"≈"(a, a"→"b) & b"∉"E & b"∉"A "entonces" b"⇾"A`
`a"=libre"`
`b"=libre"`
`"si "(y,x)"≈"(a, a"→"b) & b"∉"E & b"∉"A "entonces" b"⇾"A`
`}`
`"si" A"="{} "entonces" {`
`"tanta que" G"∈"E "entonces" G"++"`
`A"⇽"G`
`}`
`}`
`}`
`H` accumule dans `H"."E` toutes les tautologies du langage `"<→,¬, x_1,x_2,x_3,...>"`
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`
On privilègie la génération de formules courtes mettant en oeuvre des variables de petits indices. La formulle est une arborecence composée de noeuds et de feuilles. Les feuilles sont labellisées par les inconnus `x_n` ou leur négation `"¬"x_n`. Les noeuds sont labellisés par `"→"` ou par `"¬→"`.
Lorsque l'on doit générer une feuille c'est à dire choisir un inconnu, son indice, et si il est affirmé ou négativé. On fixe un paramètre d'écart type `sigma`. La procédure `sf"gauss"(sigma)` retourne un réel selon la loi normal centrée en zéro et d'écart type `sigma`. Et en prend l'arrondi entier du carré, `n=sf"gauss"(sigma)`. Cela nous donne l'indice au hasard en ayant introduit le moins d'arbitraire possible.
Puis l'arborescence doit également être générée au hasard. On utilise une probabilité `µ` d'apparition d'un noeud qui devra être très faible et que l'on utilisera sur chaque bourgeons pour déterminer s'il se tranforme en une feuille ou un noeud.
Le programme commence par tester si le bourgeon produit une feuille ou un noeud selon la probabilité `µ`. Si c'est une feuille, elle la détermine au hasard et aussi avec son éventuelle négation. Si c'est un noeud, elle construit le noeud et deux nouveaux bourgeons, et détermine au hasard son éventuelle négation. Et elle réitère le calcul des bourgeons par des appels récursifs.
On reprend l'exemple précédent de génération de formule au hasard. Voyons comment nous pourrions écrire un tel programme. Nous entrons alors dans la science de l'algorithmisation. Il ne s'agit pas de programmer l'implémentation mais juste de prototyper son pilotage, une pré-déclaration des procédures qui effectueront des modifications physiques sur les formules.
Une formule sera désignée par une variable informatique, et nous pourrons sur cette formule procéder à des modifications physiques. Il nous faut donc une première opération qui créer une formule vide appelé un bourgeon :
`x = sf"nue"()`
Puis pour transformer le bourgeon en feuille désignant la `n`ième inconnue avec son éventuelle négation selon le booléen `b`, on modifit physiquement la formule pointée par `x` à l'aide d'une procédure, on définit la méthode suivante :
`x"."sf"fin"(b,n)`
Pour transformer le bourgeon en un noeud labellisé `"→"` ou avec sa négation `"¬→"` selon le booléen `b`, on modifit physiquement la formule pointée par `x` à l'aide d'une procédure, et on récupère les pointeurs `x_1, x_2` désignant les 2 nouveaux bourgeons de la formule. On définit la méthode suivante :
`x_1, x_2 = x"."sf"tenedor"(b,n)`
Pour transformer le bourgeon en une formule aléatoire, nous lui appliquerons la méthode globale que nous sommes entrain de programmer :
`x"."sf"generar"()`
La formule est mémorisée sous forme d'arborescence en mémoire de façon à pouvoir être modifiée physiquement. Un pointeur `x` peut pointer la racine de la formule ou une sous-formule de celle-ci. Comme l'arborescence peut être partagée, il faut faire attention à ce que la modification physique modifie bien la seuls sous-formule ce que l'on souhaite mofifier, et ne modifie pas d'autres sous-formules. dans certain cas, nous devrons faire une copie intégrale de la formule pour préalablement défaire les partages de sous-formules.
On distingue le cas ou le pointeur `x` pointe un noeud ou une feuille, et le cas ou il pointe un bourgeon. Le bourgeon n'est pas une composante d'une formule complète. Le bourgeon doit se transformer soit en une feuille ou soit en un noeud. La formule est complète lorsque qu'elle n'a plus de bourgeon. On conçoit donc 2 types de méthodes, celles qui s'appliquent à un bourgeon et celles qui s'appliquent à une feuille ou à un noeud.
Les méthodes de constructions de la formule étant pilotées, la programmation devient simple :
`sf"generar"= {x "|"`
`a = sf"prob"(µ)`
`color(#705)"si" a "{"`
`b = sf"prob"(0.5)`
`y, z = x"."sf"tenedor"(b,n)`
`y"."sf"generar"()`
`z"."sf"generar"()`
`} color(#705)"entonces" {`
`n = sf"gauss"(sigma)`
`b = sf"prob"(0.5)`
`x"."sf"fin"(b,n)`
`}`
`}`
Pour générer une formule au hasard selon une loi `(µ,sigma)` préalablement posées comme variables globales, nous écrirons :
`x = sf"nue"()`
`x"."sf"generar"()`
Remarquez comment est déclarée une fonction. C'est une variable que l'on rend égale à un bloc commençant par énumérer les variables d'entrées. Exemple `f{x,y,z "|" color(#705)"devolver" x"*"y"+"z}`
Remarquez comment certaines fonctions telle que par exemple `f(x,y,z)` sont utilisées comme des méthodes, simplement en prenant le premier argument comme représentant de l'objet sur lequel est appliquée la méthode. Cela suppose que `f` est déclarée parmi les méthodes de la classe de `x` afin que `x.f(y,z) = f(x,y,z)`. Il est possible de déclarer une méthode sur la classe la plus générale des objets, la rendant ainsi applicable pour tous les objets.
On commence par prototyper les procédures de construction de formules. La fonction `sf"imp"(a,b)` crée la formule `a→b` en remplaçant les pointeurs `a` et `b` par leur valeur qui sont des formules, et retourne un pointeur sur sa racine.
`x=sf"imp"(a,b)`
Lorsque `x` désigne un noeud ou une feuille, la méthode `sf"neg"()` modifie la formule en ajoutant une négation ou en l'enlevant.
`x"."sf"neg"()`
Il y a 4 générateurs à programmer, `sf"h1",sf"h2",sf"h3",sf"h4"`.
`sf"h1"={ "|"`
`a = sf"nue"()`
`a"."sf"generar"()`
`b = sf"nue"()`
`b"."sf"generar"()`
`color(#705)"devolver" sf"imp"(a,sf"imp"(b,a))`
`}``sf"h2"={ "|"`
`a = sf"nue"()`
`a"."sf"generar"()`
`b = sf"nue"()`
`b"."sf"generar"()`
`c = sf"nue"()`
`c"."sf"generar"()`
`color(#705)"devolver" sf"imp"(sf"imp"(a,sf"imp"(b,c)),sf"imp"(sf"imp"(a,b),sf"imp"(a,c)) )`
`}``sf"h3"={ "|"`
`a = sf"nue"()`
`a"."sf"generar"()`
`b = sf"nue"()`
`b"."sf"generar"()`
`color(#705)"devolver" sf"imp"(sf"imp"(a"."sf"neg"(),b"."sf"neg"()),sf"imp"(b,a))`
`}`
Le quatrième générateur appelé le « Modus Ponens » est plus particulier, car il s'applique à l'ensemble des tautologies déjà produites. Pour appliquer cette règle `a, a"→"b |-- b` de façon efficace, on doit mémoriser les tautologies par ordre alphabétique du premier fils.
Sans se préoccuper de la méthode de recherche optimale, on propose juste un prototype, une procédure qui recheche au hasard dans un ensemble de formules `E`, une formule qui possède un fils égale à la formule `a` :
`x=sf"investigar"(E,a)`
Puis on utilise une procédure pour atteindre le deuxièlme fils d'une formule, et une autre pour en faire une copie.
`a=x"."sf"op1"()`
`b=x"."sf"op2"()`
`y=sf"copia"(x)`
# Retourne un pointeur sur le premier fils
# Retourne un pointeur sur le deux ième fils
# Crée une copie de x`sf"h4"={E,a "|"`
`x=sf"investigar"(E,a)`
`color(#705)"si" x "==" sf"Nada" {color(#705)"devolver" sf"Nada"}`
`color(#705)"devolver" sf"copia"(x"."sf"op2"())`
`}`
Le générateur de tautologies de Hilbert fonctionne par accumulation de résultats pour en produire d'autres. Aussi il est utilisé pour augmenter un ensemble `E` de tautologies par un nombre `N` conséquent de nouvelles tautologies accessibles à partir de la génération de formules au hasard de loi `(µ, sigma)` et avec la proportion `tau` de recherche de modus-ponens par rapport aux créations par les 3 autres shémas.
`sf"hilbert" = {E, µ, sigma, tau, N "|"`
`E"."sf"add"(sf"h1"())`
`s=1`
`m=1`
`color(#705)"repetir" N color(#705)"veces" {`
` color(#705)"si" m"/"s < tau {`
`E"."sf"add"(sf"h4"(sf"aleatoria"(E)))`
`m=m+1`
`} color(#705)"entonces" {`
`E"."sf"add"(sf"h1"())`
`E"."sf"add"(sf"h2"())`
`E"."sf"add"(sf"h3"())`
`s=s+3`
`}`
`}`
`}`
`E"."sf"add"()`
`x=sf"aleatoria"(E)`
# Modifit `E` en y ajoutant la formule `x` si elle n'est pas déjà présente.
# Retourne une formule `x` au hasard appartenant à `E`.
Arrivé à ce stade, il devient opportun maintenant de choisir une implémentation pour pouvoir tester le programme.
---- 29 novembre 2025 ----
On regroupe les tautologies au renomage près des variables distinctes. Avec cette équivalence, les trois premières règles de production de la grammaire correspondent aux 3 axiomes :
`a"→"(b"→"a)`
`(a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))`
`(¬a"→"¬b) "→"(b"→"a)`
On ne s'intéresse qu'anx tautotlogies au renomage près des variables distinctes. On initialise l'ensemble `F` à vide, et on ajoute dedans que des tautologies
que peut-on conclure de l'unification de deux tautologies ?