Suivant |
Le problème de l'arrêt décrit par Allan TURING constitue une manière simple de démontrer le premier théorème d'incomplétude de Kurt GÖDEL, grace à une analogie entre démonstration mathématique et exécution d'un programme informatique.
L'exécution d'un programme informatique produit un résultat. La preuve qu'il produit bien ce résultat est donnée par l'exécution formelle et mécanique du programme. C'est pour cette raison que l'on peut affirmer que « La programmation précède la logique ».
Or, qu'est-ce qu'un programme ? Il est écrit dans un langage `L`. C'est un mot appartenant à `L`, et son exécution peut prendre en entrée un mot qui joue le rôle de données d'entrée, pour produit un mot qui joue le rôle de résultat (une données de sortie). Et il n'est pas nécessaire de différencier donnée et programme. Le langage des données peut être le même que le langage de programmation.
Le langage de programmation, pour être pertinent, doit avoir la puissance d'une machine de Turing. Autrement dit, il doit pouvoir exprimer avec assez de temps et de mémoire les mêmes calculs que n'importe quel langage de programmation généraliste. A quoi peut ressembler un tel langage ? Un des plus simples d'entre eux est le Brainfuck.
La machine à une mémoire interne qui est un ruban indéfini composé de cases contenant un chiffre (un entier sur 3 bits, compris entre 0 et 7) initialisé à 0. Un pointeur indique en permanence la case courante. L'entrés standart est une file dans laquelle sont mise les données d'entrée. La sortie standart est une file dans laquelle sont envoyés les données résultats. Les données d'entrée ou de résultat sont des entiers compris entre 0 et 7. Notez qu'il n'y a pas de différence entre une donnée et une instruction. Le brainfuck comprend juste 8 instructions :
Il est important de distinguer le programme et le processus. Le programme n'est qu'un mot du langage `L= [0"-"7]"*"`, tandis que le processus comprend une mémoire interne (le ruban), une entrée standart (une file), une sortie standart (une file) et un pointeur pointant la case courante du ruban. Le processus démarre à la première instruction du programme et s'arrète lorsqu'il n'y a plus d'instruction à exécuter.
Le processus lit la file d'entrée. Si la lecture est incomplète, le restant de la donnée d'entré est perdu. Si la lecture continue au delà de la donnée d'entrée, il n'y a que des zéros qui sont lus.
Il n'y a pas de distinction entre programme et donnée, et la seule granulation présente est l'instruction qui est ici un entier compris entre `0` et `7`. Il n'y a pas d'erreur de syntaxe, tous mot de `[0"-"7]"*"` est un programme bien écrit.
Tout d'abord, on perfectionne la sémantique sans changer le langage, afin de permettre l'application des programmes à une suite de données. Pour cela il nous faut trouver un séparateur de donnée qui n'a aucun effet en terme de programmation tel que le mot `"><"` Qui correspond à l'instruction déplaçant le curseur à droite d'une case puis déplaçant le curseur à gauche d'une case.
On peut retirer ce mot `"><"` de tout programme sans que cela ne change le résultat du programme. En revanche les données sont modifiés. On impose donc un langage de donnée, dans lequel chaque donnée ne doit pas contenir le sous-mot `"><"` qui joue le rôle de séparateur.
Donc ce séparateur permet d'écrit toute suite de programme possible. Les données comme les programmes ne doivent plus contenir ce mot `"><"`qui est réservé pour servir de séparateur de donnée. On remarque alors qu'une séquence de programme forme un programme par concaténation, les mots servant de séparateur `"><"` n'ayant aucun effet sur le résultat du programme. On peut donc donner un sens dans le meta-langage à l'expression `(a,b)(x,y)` qui est la concaténation des programmes `a,b` que l'on applique à `x,y` où `x` et `y` sont deux programmes ou données quelconques.
Existe-t-il un programme `H` qui prend deux entrées et qui se comporte comme suit :
Allan Turing démontre par l'absurde qu'un tel programme n'existe pas, comme suit :
Supposons qu'un tel programme `H` existe. On considère le programme `D` suivant :
`D(P) :`
`"Si "H(P,P)"=="1" alors lancer une boucle sans fin"`
`"Retourner" 1`
Le calcul de `H(D,D)` révèle alors une contradiction :
On définit un nouveau langage de programmation de conception idéalement simple étendant naturellement les fonctionnalités évoquées pour le problème de l'arrêt d'une manière plus abstraite, c'est à dire au moins suffisament riche pour exprimer cette contradiction, mais libéré des contraintes de bas protocole. Nous allons à la fois révéler la constitution du processus associé au programme, et décrire les mécanismes de déclaration de variable en suivant les principes de la logique du premier ordre.
On part de l'élément, le type le plus générale, unique, propre à la logique du premier ordre.
Ce langage comprend la faculter d'appliquer un élément à un élément, ou à un couple d'éléments. On peut prolonger cette faculté et admettre qu'un élément peut s'appliquer à `n` éléments. Exemple : `X(Y,Z,T)`, l'élément `X` s'applique au triplet d'éléments `Y,Z,T`. Le résultat étant aussi un élément, il peut s'appliquer à son tour à une liste d'autres éléments, `X(Y,Z,T)(A,B)`. Cela engendre le langage alpha multi-aire.
L'élément `X` peut être exécuté comme un programme sur l'entrée vide, et cela se note `X()`. Ainsi l'élément `X` est le programme `X` tandis que l'élément `X()` est le résultat du programme `X` appliqué à aucun argument c'est à dire à une file d'entrée vide.
Lorsqu'il y a un appel d'application, celle-ci est évaluée. Pour définir le langage, il faut pouvoir manipuler de telles expressions sans les évaluer. On conçoit donc une première phase de l'interpréteur qui n'évalue pas les appels d'application, et permet de manipuler les termes du langage alpha multi-aire.
---- 31 mai 2026 ----
Ce langage comprend la donnée `0` et la donnée `1`, soit deux éléments. Si on tient à garder cette ambivalence que tout élément est un programme, alors, conceptuellement parlant, le plus simple et le moins desinformationel, est de considérer ces constantes comme des programmes produisant en sortie ces mêmes constantes, c'est à dire produisant elle-même.
`0=0()=0(X)=0()()`
`1=1()=1(X)=1()()`
Ce langage comprend l'opération de concaténation de programme, noté par la virgule à qui on donne ce deuxième rôle. La concaténation de programmes n'est pas le pipeline ou composition de programmes. Elle utilise la même file d'entrée et de sortie. Ainsi, une séquence de constantes peut être interprété comme une concaténation de programme, et nous constatons qu'elle retourne la séquence de constantes dans le même ordre :
`(0,1,0,0,1)() = 0,1,0,0,1`
L'expression `(A,B)(X)` commence par exécuter `A`, avec `X` dans la file d'entrée, puis exécute `B` avec ce qui reste dans la file d'entrée et en utilisant toujours la même file de sortie.
La donnée vide ou programme vide se note par une séquence vide `()`. Et l'exécution de `()(X)` retourne `()`. Parcontre, l'insertion d'une séquence vide dans une séquence n'a aucun effet. `(X,(),Y)` est identiqe à `(X,Y)`. Les séquences sont des listes applaties. `(X,(Y,Z))` est identique à `(X,Y,Z)`.Autrement-dit, la concaténation est associative et a comme élément neutre la séquence vide.
La variables `L_1` contient le premier argument, la variable `L_2` comprend le second argument, etc.. Si l'argument n'existe pas, la variable contiendra la séquence vide.
Ce langage comprend l'instruction conditionnelle qui, si l'élément `X' est égale à `1` alors on retourne l'élément `Y`, sinon on retourne la séquence vide. Cela se fait par l'exécution du programme `C(X,Y)`.
Ce langage comprend l'instruction "répéter tant que". Cela consiste à répéter un programme `Y` tant que `X` est égale à `1` en utilisant la même file d'entrée et la même file de sortie. Cela se fait par l'exécution du programme `"ට"(X,Y)`.
Le calcul de `"ට"(X,Y)` commence par évaluer `X`, et si `X` est égale à `1` alors il évalue `Y` et recommence, et si `X` est égale à `0` alors il retourne le résultat de la dernière execution de Y
Une boucle sans fin ne faisant rien se programme comme suit `"ට"()`
Considérons le programme `D` suivant : C(H(L_1,L_1),ට),F(1)
Jusqu'à présent les lettres `A,B,X,Y,Z,T` représentent des données particulières qui peuvent donc être interprété aussi bien comme des données que comme des programmes. Elles se comportent comme des variables globales déclarées dans le langage de base. Un langage de programmation moderne permet de déclarer de nouvelles variables dont la portées est restreinte à une partie. Si la variable est de même nom qu'une variables déjà existante alors elle la masque sur tout l'espace de sa portée. La déclaration de la variable `X` se fait par le programme `EE(X,Y)`. Cela crée une nouvelle variable `X` de portée couvrant le programme `Y`.
Le programme `EE` se distingue des autres propgrammes par le fait qu'il n'évalue pas son premier argument qui doit être une variable.
L'affectation de la variable `X` par la valeur `1` se fait par l'exécution du programme `A(X,1)`.
Le programme `A` se distingue des autres propgrammes par le fait qu'il n'évalue pas son premier argument qui doit être une variable.
La composition de programmes correspond au pipeline, noté par le symbole Unix "`"|"`". La file de sortie sert alors de file d'entrée du programme suivant. Exemple : `X|Y|Z`. La composition est associative.
Ce langage comprend la fonction de test d'égalité qui compare ses deux arguments et retourne `1` s'il sont égaux ou `0` sinon. Cela se fait par l'exécution du programme `Q(X,Y)`
Ce langage comprend l'instruction qui termine le programme en cours, en retournant dans la file de sortie la donnée `X`. Cela se fait par l'exécution du programme `F(X)`
Avec cette base de langage, si nous supposons un programme `H` tel que H(X,Y)=1 si X(Y) s'arrête. et H(x,y)=0 si X(Y)=oo c'est à dire ne s'arrête jamais. Nous programmons le programme D comme suit :
`D(P) :(`H(P,P)"=="1 => "ට"X(),"da" `1)`
En résumer, quelque soit 3 programmes `X,Y,Z` nous avons le jeux d'instructions suivantes :
Programme qui retourne `0` Programme qui retourne `1` Programme `X` qui utilise comme entrée `Y` Programme `X` qui utilise comme entrée `Y` et `Z` Programme `X` qui répète indéfiniment le sous-programme `X` Si l'exécution du programme `X` est égale à l'exécution du programme `Y` alors exécuter le sous-programme `Z` retourne ce que retourne le sous-programme `X`
La structure générale met en avant deux opérations. L'une est l'application d'un programme sur une donnée d'entrée. L'autre est la concaténation de deux programmes . On définit donc un méta-langage :
Magma
Langage alpha
Tout d'abord, on perfectionne la sémantique sans changer le langage, afin de permettre l'application des programmes à une suite de données. Pour cela il nous faut trouver un séparateur de donnée qui n'a aucun effet en terme de programmation tel que le mot `"><"` Qui correspond à l'instruction déplaçant le curseur à droite d'une case puis déplaçant le curseur à gauche d'une case.
On peut retirer ce mot `"><"` de tout programme sans que cela ne change le résultat du programme. En revanche les données sont modifiés puisque
Donc ce séparateur permet d'écrit toute suite de programme possible. Les données comme les programmes ne doivent plus contenir ce mot `"><"`qui est réservé pour servir de séparateur de donnée. On remarque alors qu'une suite de porgramme forme un programme par concaténation, les mots servant de séparateur `"><"` n'ayant aucun effet sur le résultat du programme. On peut donc donner un sens dans le meta-langage à l'expression `(a,b)(x,y)` qui est la concaténation des programmes `a,b` que l'on applique à `x,y` où `x` et `y` sont deux programmes quelconques.
On généralise ainsi l'application d'un programme sur une liste de données d'entrée. L'application d'un programme `x` sur une liste `(a,b)` est notée `x"*"(a,b)` ou plus classiquement `x(a,b)`, où `x,a,b,c` sont des mots du même langage `L` ne contenant pas le mot `"><"`.
ll y a deux notations, l'écriture classique qu'est celle d'une loi magmatique `"*"`, et d'une loi associative libre qu'est la concaténation virgule, et l'écriture dynamique qu'est celle du langage alpha multi-aire :
Magma
Langage alpha(a,b)(x)(y)
La définition d'un programme peut se faire à l'aide du meta-opérateur `|->`. Par exemple :
A = (X|->X(X))
A partir de ces seuls propriétés, Alan Turing résoud le problème de l'arrêt.
Le but étant de définir une logique, nous allons choisire un langage adapté pour cela. On choisit un langage algébrique c'est à dire engendré par une liste d'opérateurs d'arité fixé dits générateurs tel que par exemple :
`L ="<"u,v,w,s("."),f(".,."),g(".,.")">"`
Les mots de ce langage son appelés des termes. Un terme est une composition close d'opérateurs générateurs. Voici quelques exemples de termes du langage `L`:
`u, s(u), s(s(u)), f(v,g(v,w))`
Le premier stade de la logique est la logique propositionnelle. C'est pourquoi les termes de notre langage désigneront des propositions. Mais la définition s'arrête là, les termes du langage n'ont comme propriété que celle d'être des identifiants. Et donc ce ne sont pas des booléens !
Et on ajoute des variables `X,Y,Z,...` muettes. Elles sont dites muettes car on peut les renomer sans que cela ne change le sens du terme
Un terme avec variable désigne une application de `L^n→L`. Par exemple le terme `f(s(X),Y)` désigne l'application suivante où les variables d'entrée `X,Y` sont énumérées dans l'ordre de leur première apparition dans le terme.
Le terme avec variables : `f(s(X),Y)`
L'azpplication correspondante : `X,Y|->f(s(X),Y)`
L'unification de deux termes, notée avec l'opération `"*"`, consiste à affecter aux variables les termes les plus généraux afin que les deux termes coïncident, et de retourner le terme unifié. Exemple :
`f(f(X,v),Y)"*"f(Z,f(Z,v)) = f(f(X,v),f(f(X,v),v))`
On utilise cette opération qu'avec des variables muettes, ou autrement dit qui n'ont pas de signification à l'extérieur de l'unification en cours. Elles peuvent être renommées, et il existe une forme normale qui consiste à nommer les variables `x_1,x_2,x_3,...` dans l'ordre de leur première apparition dans le terme.
La sémantique d'un terme tel que `f(f(X,v),Y)` est l'ensemble de tous les termes unifiables à lui. Cela confirle pourquoi, ici, le sens que l'on donne à un terme avec variable ne tient pas compte du nom des variables.
Lorsque l'on introduira les règles de production, la production d'un terme avec variable signifiera que tout les termes qui lui sont unifiables sont également productibles.
Les fonctions généralisent les application vues précédement, en procédant d'abord par une unification des entrées. Par exemple considérons la fonction `varphi` suivante :
`varphi : f(f(X,v),Y),s(Y) |-> g(X,f(Y,Z))`
On note le résultat `Ø` lorsque la fonction est appliquée en dehors de son domaine de définition. Nous avons par exemples :
Voici un exemple de fonction d'arité nulle :`varphi(A,B) = g(X,f(Y,Z))`
`varphi(f(A,B),s(A)) = g(f(X,v),f(f(X,v),Z))`
`varphi(f(A,u),B) = Ø`
`|-> g(u,v)`
Cette fonction produit le terme `g(u,v)`
Un système de production est un ensemble de telles fonctions `{varphi_1(.,.), varphi_2(.), varphi_3(.,.,.), ,...}` que l'on applique qu'à des propositions déjà produite pour en produire une. L'arbre de production est alors un terme du langage `"<"varphi_1(.,.), varphi_2, varphi_3(.),...">"`
L'algorithme de recherche pour découvrir le chemin de production d'un terme `lambda`, apparaît naturellement : L'état initial comprend un ensemble `E` ne comprenant que le terme `lambda` à résoudre. Pour chaque règle de prodution, on regarde si la production `P` est unifiable avec `lambda`. Puis, si c'est le cas, on crée un état fils en ajoutant dans l'ensemble `E` les hypothèses nécessaires affirmés par la règle avec les variables affectée par l'unification. Lors de l'ajout d'un terme dans l'ensemble frontière, on teste son unification avec chacun d'eux, et si elle réussit on ne le rajoute pas mais on remplace le terme déjà présent par le résutlat de l'unification. Si le niveau `n"+"1` est atteint, on retropédale on revient au noeud père et on essaye une autre règle de production.
Pour rendre complet l'algorithme de rechechre, il faut parcourire l'arbre en profondeur d'abord jusqu'au niveau maximum `n` puis recommencer jusqu'au niveau `n"+"1` et ainsi de suite.
Notre programme est défini par un ensemble de règles de production. lorsqu'on l'applique à un terme, soit il ne s'arrète jamais de calculer, ou soit il retourne l'arbre de production de terme de plus petite profondeur.
Un terme est un arbre, une composition fini et non récurcive d'opérateurs tel que par exemple `f(g(u,s(v)),f(v,y))`. On peut concevoir des termes récurcifs formant un graphe fini, par exemple le terme `X=s(X)`. Autre exemple, le terme `f(X=g(X,u),s(X))`.
Notez que le système de production agrandit sa production dans l'extension rationnelle.
La logique propositionnelle classique donne à toute proposition sans variable la valeur logique vrai ou faux, et utilise comme connecteurs, les opérations booléennes. La valeur logique vrai est notée `1`, la valeur logique faux est notée `0`. Les connecteurs booléens les plus utilisés sont `"¬", "∧","∨","→","↔"` et correspondent à des opérations booléennes. Chaque connecteur booléen est défini par sa table de vérité :
`"¬"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`
Une proposition sans variable est une formule du langage `sfP="<"0,1,"¬","∧","∨","→","↔>"`. C'est un calcul qu'il suffit d'effectuer pour connaitre sa valeur logique. Exemple :
`"¬"((0"→"0)"∧"(1"→"0))"↔"(0"→"0)`
Si on effectue toutes les opérations booléennes, on obtient la valeur logique de la proposition. Ainsi chaque proposition sans variable se réduit en une unique valeur booléenne.
Le langage est défini par la grammaire suivante :
`sfP = {0,1, "¬"sfC,(sfC"∧" sfC),(sfC"∨" sfC),(sfC"→" sfC),(sfC"↔" sfC)}`
Les tables de vérité qui permettent d'effectuer les opérations booléennes, se regroupent en une théorie :
T = {`"¬"0"="1`, `"¬"1"="0`, `0"∧"0"="0`, `0"∧"1"="0`, `1"∧"0"="0`, `1"∧"1"="1`, `0"∨"0"="0`, `0"∨"1"="1`, `1"∨"0"="1`, `1"∨"1"="1`, `0"→"0"="1`, `0"→"1"="1`, `1"→"0"="0`, `1"→"1"="1`, `0"↔"0"="1`, `0"↔"1"="0`, `1"↔"0"="0`, `1"↔"1"="1`}
Le langage et le procédé de calcul regroupé dans la théorie forme une structure. La structure se note sous forme d'un quotient du langage algébrique par la théorie d'égalité :
`sfP/T`
On étend le langange propositionnel en ajoutant 3 variables élémentaires `a,b,c`. Une proposition devient une formule du langage `sfP` que l'on note à l'aide des crochets entourant les éléments et connecteurs générateurs :
`sfP="<"0,1,"¬", "∧","∨","→","↔", a,b,c">"`.
Le langage s'exprime aussi sous forme d'une grammaire (une sorte d'inclusion récurcive d'ensembles) :
`sfP = {"¬"sfP,(sfP"∧" sfP),(sfP"∨" sfP),(sfP"→" sfP),(sfP"↔" sfP),0,1,a,b,c}`
Le langage est dit une extension du langage par ajout de nouveaux éléments `a,b,c` et que l'on note :
`sfP[a,b,c]`
Notez qu'à ce stade, rien n'indique que les éléments `a,b,c`, sont des variables booléennes.
Etant donné une proposition par exemple : `p =(a"→"(b"→"c))"→"(b"→"(a"→"c))`. La proposition est dite tautologique si quelques soient les valeurs booléennes des variables, elle vaut toujours `1`. La proposition est dite antilogique si quelques soient les valeurs des variables, elle vaut toujours `0`. Et elle est dite indécidable s'il existe des valeurs des variables pour lesquelles `p` vaut `1`, et il existe des valeurs des variables pour lesquelles `p` vaut `0`.
Pour savoir par exemple si la proposition `a"→"(b"→"a)` est tautologique c'est à dire toujours vrai quelques soient les valeurs des variables `a` et `b`, on calcule tous les cas possibles grâce aux tables de vérité et on vérifie que la proposition vaut toujours `1` dans tous les cas.
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 les quantificateurs existentiels et universels, alors le nombre d'éléments existants et le nombre d'inconnus booléens existants devient infini. L'usage des tables de vérité des connecteurs n'est plus suffisant 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 propositionnelles, à des formules dans un langage augmenté qui peut être celui 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 sans variable peut s'écrire qu'avec deux seuls connecteurs booléens que sont le faux `"0"` et le connecteur d'implication `"→"`. En effet, il est facile de constater que les connecteurs booléens peuvent tous être définis avec seulement le faux `"0"` 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 simple, défini par la grammaire suivante :
`sfP = {0,(sfP"→" sfP)}`
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 soit la valeur zéro ou soit le nom d'une variable élémentaire.
Considérons une proposition quelconque avec des inconnues `a,b,c,...`. La proposition étant considérée en dehors de tout contexte, les variables n'ont pas de signification propre et peuvent être renomer sans que cela ne change la valeur logique de la proposition. On définit une forme normal en renommant les variables dans l'ordre de leur première apparition dans la proposition. Ainsi `(b"→"a)"→"b` possède comme forme normal `x_1"→"(x_2"→"x_1)`.
Le système de Hilbert propose 4 règles de production de propositions, pemettant de produire exactement toutes les propositions tautologiques au sens classique.
`"R1"` : `|-- a"→"(b"→"a)` `"R2"` : `|-- (a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))`
`"R3"` : `|-- ((a"→⊥")"→"(b"→⊥")) "→"(b"→"a)`
`"MD"` : `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 du langage `sfP`.
La priorité syntaxique des connecteurs est la suivante, de la plus forte à la plus faible :
`"virgule"` `"⊢"`
La quatrième règle MD est appelé le « modus ponens ».
On définit la négation juste comme une réécriture :
`"¬"x := x"→"0`
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 la valeur zéro. Ainsi chaque fois que sera écrit `"¬"x` il faudra lire `x"→"0`.
Dans le langage `"<⊥,→,>"`, les propositions utilisent des variables `a,b,c,...` qui n'ont pas de signification particulière
Dans le langage `"<⊥,→,>"` le système de démonstration de Hilbert est décrit par les 4 règles de déduction suivante :
`"R1"` : `|-- a"→"(b"→"a)`
`"R2"` : `|-- (a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))`
`"R3"` : `|-- ((a"→⊥")"→"(b"→⊥")) "→"(b"→"a)`
`"MD"` : `a, a"→"b |-- b`
Voici comment fonctionnent de telles règles : Les variables `a,b,c` contiennent chacune une proposition inconnue. Les propositions énumérées à gauches du symbole `"⊢"` doivent avoir déjà été produite pour pouvoir appliquer la règle. 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.
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.
| `"R1"` : `|-- a"→"(b"→"a)`
`"R2"` : `|-- (a"→"(b"→"c))"→"((a"→"b)"→"(a"→"c))` `"R3"` : `|-- ((a"→⊥")"→"(b"→⊥")) "→"(b"→"a)` `"MD"` : `a, a"→"b |-- b` |
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, et cela se fait avec une complexité linéaire :
`a"→"(b"→"a)`
`(c"→"(d"→"e))"→"((c"→"d)"→"(c"→"e))`
`("¬"f"→¬"g) "→"(g"→"f)`
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é :
On définit la classe `n` des tautologies, celles produites par le modus ponens appliqué une seul fois à deux tautologies de classe inférieur à n. Pour qu'une proposition appartinennent à la classe `n`, il y a trois possibilité :
On voit qu'il est possible d'étudier de tels systèmes de production de façon empirique, en programmant leur énumérateur selon cette stratégie par degrés.
---- 30 avril 2026 ----
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és de leurs axiomes (les règles de raisonnement spécifiques à eux) pour ainsi produire une extension de la logique qui n'est plus booléenne dès qu'un tel connecteur non-booléen est présent.