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. Ces inclusions récursives forment une grammaire, qui construit des emboitements. Les parenthèses sont donc nécessaires autours de chaque composition. Mais la plus part d'entre-elles sont remplacées dans l'écrit par des règles de priorité syntaxique.
Le système de Hilbert propose un shéma d'axiomes pemettant de construire toutes les tautologies.
`|-- 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 :
---- 4 décembre 2025 ----
`"¬", "→", "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 déduction naturel propose une liste d'axiomes basé sur l'introduction et l'élimination de chaque connecteur du langage :
`(a|--b) |-- a"→"b` `a, a"→"b |-- b`
`a"→"b |-- "¬"b"→¬"a`
`a, "¬"a |-- b`# 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`. À tout endroit d'une preuve ou d'une sous preuve il est possible de commencer une sous sous preuve commençant par une supposition, et ainsi de suite.
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 ----