Une approche constructive large permet de redéfinir la logique d'une manière plus générale incorporant les logiques non-classiques et d'autres logiques 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 programmer une machine ayant la puissance de calcul d'une machine de Turing. C'est à dire qu'avec assez de temps et de mémoire elle doit pouvoir 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é, un langage algébrique simple. Où les éléments générateurs sont des propositions atomiques, et où les opéarateurs générateurs sont des connecteurs logiques. Et nous utiliserons la fonction d'unification de termes, un procédé qui a l'avantage d'être de complexité linéaire.
On pose comme premier principe que la logique définit un nombre fini de valeurs logiques, et que chaque proposition peut posséder zéro ou une ou plusieurs de ces valeurs logiques. Autrement dit, une valeur logique désigne un ensemble de propositions (l'ensemble des propositions possédant cette valeur logique).
On pose comme second principe que la logique est calculable, c'est à dire que chaque valeur logique désigne un ensemble énumérable. C'est à dire que pour chaque valeur logique, l'ensemble des propositions possédant cette valeur logique est énumérable.
Il découle de ce principe que les propositions qui n'ont pas de valeurs logiques forment généralement un ensemble non-énumérable appelé l'ensemble des propositions indéterminées
On ajoute comme troisième principe que le procédé d'énumération de ces ensembles doit être donné par le système de production de la logique.
A partir de ces trois principes on peut construire différent systèmes de production, 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.
La construction consiste à définir pour chaque identifiant, une ou plusieurs valeurs logiques ou bien l'absence de valeur logique. Et le procédé qui énumère les propositions avec leur valeur logique, est par principe calculable, c'est à dire qu'il existe et qu'il est d'une certaine façon contenu dans le système de production de la logique.
La sémantique du langage se décrit à l'aide de la notion d'univers qui regroupe l'ensemble des inconnues logiques. Chaque proposition constiue une inconnue logique. L'univers est l'ensemble des termes du langage. Un monde, qui est une instanciation de l'univers, donne une valeur logique aux termes du langage mais pas à tous car la logique est non-exhaustive. Il restera dans le cas générale un ensemble indénombrabe de proposition sans valeur logique.
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 n'ont donc pas de référence à l'extérieur du terme ou du n-uplet de termes considéré. Autrement dit elles ne correspondent à aucune nouvelle inconnue logique dans l'univers.
Elle vont nous permettre de définir les ensembles génériques, les applications génériques et les fonctions génériques.
Un terme avec variable muette définit un ensemble générique de termes. C'est l'ensemble des termes qui lui sont unifiables. Par exemple, le terme `X` désigne l'ensemble de tous les 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 ainsi définissables par un terme sont dit générique.
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.
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émantique 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 avec variable muette désigne aussi 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(Y),Y), g(X,Y) )` désigne l'application suivante où les variables d'entrée `Y,X` sont énumérées dans l'ordre de leur première apparition dans le `n`-uplet de termes :
`Y,X|->( f(s(Y),Y), g(X,Y) )`
Les fonctions génériques généralisent les application précédentes en remplaçant la liste de variables libres de l'entête par une liste de termes. 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)`
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é 0sous 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 part du principe que le système de production de la logique énumère pour chaque valeur logique toutes les propositions possédant cette valeur logique. Et donc que les valeurs logique correspondent à des ensembles énumérables de propositions.
Le langage (l'ensemble des propositions) forme une structure libre. Les valeurs logiques désignent des sous-ensembles énumérables de propositions. On remarque que les combinaisons d'unions et d'intersections de valeurs logiques sont également énumérable, et peuvent donc constituer des valeurs logiques.
Toute combinaison d'unions et d'intersections de valeurs logique peut servire de définition de nouvelles valeurs logiques. En revanche dans le cas générale, le complément d'une valeur logique n'étant pas énumérable, il ne peut servir à définir une nouvelle valeur logique.
On définit un type de système de production très général, appelé grammaire-schème qui sont des ensembles de fonctions génériques où chaque proposition argument doit avoir une valeur logique prédéfinie, et ou le résultat possède une valeur logique prédéfinie. Voici un exemple de telle fonction, avec 3 valeurs logiques `"A,B,C"` :
`f(X,Y) "∈" "A", g(Y,Z)"∈""B" |-- f(X,Z) "∈" "C"`
Reste à déterminer la valeur logique de la règle elle-même, qui reste encore un point a éclaircire, et auquel on ne répond pas pour l'instant, la règle de production ne faisant pas partie du langage des propositions.
Les valeurs logiques prédéfinies utilisées dans les règles pourraient être des combinaisons d'unions et d'intersections de valeurs logiques. Dans ce cas on redéfinit des valeurs logiques de telle sorte qu'elles apparaissent toujours isolées dans les règles du système de production.
Un premier travail consiste à concevoir l'algorithme de production d'une grammaire-schème.
La logique propositionnelle classique correspond au calcul booléen.
La logique propositionnelle classique donne à toute proposition sans variable une valeur logique vrai ou faux, résultat du calcul de la proposition. Elle utilise alors comme connecteur, les opérations booléennes c'est à dire des opérateurs opérant sur `{0,1}`. 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 peut ajouter des variables muettes pour définir des ensembles génériques de propositions, des applications génériques, et des fonctions génériques. Mais si ces variables ne sont plus locales et qu'elles sont ajoutées dans l'univers comme des nouvelles constantes inconnues, alors on parlera d'extension élémentaire. Ces nouvelles variables constitue de nouvelles propositions.
On étend le langage propositionnel en ajoutant 3 variables élémentaires `a,b,c`. On note le langage étendu à l'aide des crochets entourant les éléments et connecteurs générateurs :
`sfL="<"0,1,"¬", "∧","∨","→","↔", a,b,c">"`
Le langage s'exprime aussi sous forme d'une grammaire (une sorte d'inclusion récurcive d'ensembles) :
`sfL = {"¬"sfL,(sfL"∧" sfL),(sfL"∨" sfL),(sfL"→" sfL),(sfL"↔" sfL),0,1,a,b,c}`
que l'on peut aussi présenter sous forme de grammaire-schème :
`X^sfL |-> ("¬"X)^sfL` Si `X` est dans `sfL` alors `"¬"X` est dans `sfL ` `X^sfL, Y^sfL |-> (X"∧" Y)^sfL` Si `X` et `Y` sont dans `sfL` alors `X"∧" Y` est dans `sfL` `X^sfL, Y^sfL |-> (X"∨" Y)^sfL` Si `X` et `Y` sont dans `sfL` alors `X"∨" Y` est dans `sfL` `X^sfL, Y^sfL |-> (X"→" Y)^sfL` Si `X` et `Y` sont dans `sfL` alors `X"→"Y` est dans `sfL` `X^sfL, Y^sfL |-> (X"↔" Y)^sfL` Si `X` et `Y` sont dans `sfL` alors `X"↔"Y` est dans `sfL` `|->0^sfL` `0` est dans `sfL` `|->1^sfL` `1` est dans `sfL` `|->a^sfL` `a` est dans `sfL` `|->b^sfL` `b` est dans `sfL` `|->c^sfL` `c` est dans `sfL`
Le langage est dit une extension du langage par ajout de nouveaux éléments `a,b,c` et que l'on note :
`sfL = 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.
Dans le langage étendu `sfP[a,b,c]`, les variables `a,b,c` ne sont pas muettes car l'extension du langage s'accompagne de l'extension de l'univers.
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 indeterminée 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 booléenne 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.
Si les éléments et opérateurs ne sont pas booléens. Le nombre d'inconnus existants peut devenir infini. L'usage des tables de vérité pour calculer la valeur logique d'une formule, peut de plus pouvoir être mis en oeuvre. 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à de la logique classique, à des logiques non standard ou encore d'autres logiques encore 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 décrit au prochain chapitre. 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.
Les logiques ternaires comprenent trois valeurs logiques possibles. Si on considère une logique ternaire où chaque proposition sans variable possède une valeur logique qui est le résultat du calcul de la proposition, comme c'est le cas pour la logique binaire, alors les connecteurs de cette logique sont simplement les opérateurs opérants sur les triléens `{0,1,2}`. On les appelle les connecteurs triléens. Chaque connecteur triléen est défini par sa table de vérité. On optient la définition de la logique triléenne classique.
Mais il est tout à fait possible de définir des logiques exotiques où la valeur logique d'une proposition sans variable n'est pas toujours obtenu par le résultat du calcul de la seule proposition.