Suivant |
Une approche constructive minutieuse permet de redéfinir la logique d'une manière plus générale, d'incorporer les logiques non-classiques, de définir les logiques d'ordre supérieurs et d'autres encore plus exotiques.
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 (un rôle de 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 arrive à la fin des instructions du programme à exécuter.
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 :
Magma
Langage alpha
Il n'y a pas de distinction entre programme et donnée, et la seul 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 les calculs et toutes les structures de données peuvent être programmés en Brainfuck.
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 composé d'opérateurs d'arité fixé tel `L ="<"u,v,w,s("."),f(".,."),g(".,.")">"` et on ajoute des variables `X,Y,Z,...` élémentaires muettes.
Un terme sans variable du language `L` est une composition complète d'opérateurs tel que par exemple `f(f(u,v),u)`. Un terme avec variable élémentaire désigne une application de `L^n→L`. Par exemple le terme `f(f(X,v),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.
`X,Y|->f(f(X,v),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(Y,f(Z,v)) = f(f(X,v),f(X,v))`
On utilise cette opération qu'avec des variables muettes, ou autrement dit qui n'ont pas de signification à l'exterieur 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 telque `f(f(X,v),Y)` est l'ensemble de tous les termes unifiables à lui. C'est 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.