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 de programmation. Son exécution peut prendre en entrée une donnée écrite dans un langage qui peut être le même, pour produit une donnée en sortie. Le langage de programmation, pour être pertinent, doit pouvoir définir une machine ayant la puissance d'une machine de Turing. C'est à dire qu'avec avec assez de temps et de mémoire elle puisse mener à bien tous les calculs possibles (faisables par une machine de turing). A quoi peut ressembler un tel langage ? Un des plus simples d'entre eux est le Brainfuck, décrit dans Informatique et logique
Pour traiter de la logique, nous allons utiliser un autre langage de programmation, un langage adapté utilisant la fonction d'unification de termes, qui à l'avantage d'avoir une complexité linéaire.
On construira différent systèmes de production Turing-complet, et chaque système de production définira une logique.
Le but étant de définir une logique, nous allons choisire un type de 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 !
Le langage s'enrichit de variable `X,Y,Z,...` muettes. Elles sont dites muettes car on peut les renommer sans que cela ne change le sens du terme. Elle vont nous permettre de définir les ensembles génériques, les applications génériques et les fonctions génériques.
L'ensemble générique de termes se définit grâce à la procédure d'unification de termes.
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(X,v)"*"f(Y,Y) = f(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. Ainsi elles peuvent être librement renommées. 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 ou la séquence de termes.
La sémantique d'un terme tel que `f(X,v)` est alors l'ensemble de tous les termes unifiables à lui. Cela confirme pourquoi, ici, le sens que l'on donne à un terme avec variable ne tient pas compte du nom des variables. Les ensembles définissables par un terme sont dit générique.
Par exemple, le terme `X` désigne l'ensemble de tous les termes.
On étend cette procédure d'unification aux `n`-uplet de termes. Un `n`-uplet de termes, pouvant partager de mêmes variables, désigne un ensemble générique de dimension `n`.
La sémentique d'un `n`-uplets de termes est l'ensemble de tous les `n`-uplets de termes unifiables à lui.
Par exemple, le couple `(X,Y)` désigne l'ensemble de tous les couples de termes.
L'ensemble vide est noté `Ø`.
Un terme désigne une application de `L^k→L` où `k` est le nombre de variables contenues dans le terme. 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 :
`X,Y|->f(s(X),Y)`
Un `n`-uplet de termes désignent une application de `L^k→L^n` où `k` est le nombre de variables contenues dans le `n`-uplet de termes. Par exemple le couple de termes `( f(s(X),Y), g(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 :
`X,Y|->( f(s(X),Y), g(X,Y) )`
Les fonctions génériques généralisent les appliation précédentes en remplaçant la liste de variables libres de l'entête par un terme. Elles procédent d'abord par une unification des entrées, définissant ainsi leur domaine de définition. Par exemple, considérons la fonction `varphi` d'arité 2 :
`varphi : f(X,v),s(X) |-> g(X,Z)`
Appliquée au couple de termes `(f(u,v),s(u))`, elle produit `g(u,Z)` qui est un terme avec variable, c'est à dire un ensemble générique. Les fonctions génériques prennent un `n`-uplet de termes (qui avec variables représente un ensemble générique de `n`-uplets de termes) pour produire un terme (qui avec variables représente un ensemble générique de `n`-uplets de termes). Nous avons par exemples :
Voici un exemple de fonction d'arité nulle :`varphi(f(u,v),s(u)) = g(u,Z)`
`varphi(A,B) = g(X,Z)`
`varphi(A,s(u)) = g(u,Z)`
`varphi(f(A,A),s(A)) = g(v,Z)`
`varphi(f(A,u),B) = Ø`
`|-> g(u,v)`
Cette fonction produit le terme `g(u,v)`
Exemple de fonction générique produisanr un couple de termes (qui avec variables représente un ensemble générique de couple de termes) :
`f(X,Y),s(X) |-> (g(Y,X),s(Y))`
Un terme est un arbre, une composition finie et non récurcive d'opérateurs tel que par exemple `f(g(u,s(v)),f(v,y))`. On peut concevoir un arbre partageant des sous-arbres, et des termes récurcifs formant un graphe fini. On utilise des labels composés d'une variable et du signe égal mis en préfixe d'un terme pour indiqué que celui-ci est partagé sous la référence de la variable mentionnée. Par exemple le terme `f(X=f(u,v),X)` partage le sous-terme `f(u,v)`. Autre exemple, le terme récurcif `X=s(X)`.
La définition des ensembles génériques, des applications générique, et des fonctions génériques, s'applique également à l'extention rationnelle du langage.
Notez que le domaine de définition des fonctions génériques s'agrandissent dans l'extention rationnelle du langage.
On aborde la théorie de la démonstration de façon constructive. Il existe donc un système de production qui énumère toutes les tautologies par un procédé calculable. Et cela définit ce que l'on entend par tautologie.
Le système de production est un ensemble de règles de production. Une règle de production et une fonction générique qui doit s'appliquer qu'aux termes déjà produits. Exemple :
`|-- f(u,X)`
`|-- g(v,w)`
`f(X,Y), g(Y,Z) |-- f(X,Z)`
Les règles d'arité zéro permette de définir la classe zéro `T_0` des tautologies qui contient ici `{f(u,X),g(v,w)}`. Les autres règles appliquées aux termes de la classe `T_1` définissent la classe un des tautologie `{f(u,w}}`. Les autres règles appliquées aux termes de la classe un définissent la classe deux des tautologies `{f(u,w}}`
Les démonstrations étant calculables, elles découles d'un tel système de production Turing-complet. Pour chaque logique, il existe donc un tel système de production qui contient de façon exhaustive toutes les règles de raisonnement dans cette logique.
La logique propositionnelle classique correspond au calcul booléen.
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. Ce sont des opérateurs binaires de syntaxe centrée c'est à dire au lieu d'écrite `"∧"(x,y)` on note `(x"∧"y)` mais cela correspond exactement au même terme. 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 une théorie d'égalité qui y définie une relation d'équivalence :
`sfP/T = {0,1}`
On étend le langage 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. Il est donc possible d'introduire des nouvelles proposition qui ne sont pas booléennes, et d'introduire des principes non-classiques dans cette logique classique.
Si on suppose que `a,b,c` sont booléens, alors, étant 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 qui énumère toutes les démonstrations possibles, qui produit toutes les propositions tautologiques au niveau syntaxique, 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, ou encore d'autres logiques plus exotiques.
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.