Suivant |
On considère un langage algébrique défini par une liste d'éléments générateurs et d'opérateurs générateurs. Considèrons par exemple le langage algébrique de présenation suivante :
` "<"a,b,c,f("."),g(".,.")">"`
Chaque terme de ce langage constitue une proposition dont la sémantique n'est pas précisée à ce stade. Les éléments générateurs sont des propositions fondamentales non précisées, et les opérateurs générateurs sont des connecteurs logiques non précisés à ce stade. Cela définit une notion de connecteur logique beaucoup plus générale. On considère des variables muettes :
`X,Y,Z,....`
Ces variables représentent donc des propositions quelconque ou inconnue mais appartenant au langage ainsi définit. Aussi elles ne constituent pas une extension du langage, et sont pour cette raison qualifiées de varaible muettes. On considèrons des valeurs logiques :
`"A","B","C"`
Les propositions peuvent posséder zero, une ou plusieurs valeur logique. L'ensemble des propositions possédant la valeur logique `"A"` se note `A`. La logique étant calculable ces ensembles sont énumérables. Par contre l'ensemble des propositions ne possédant pas de valeur logique est en générale non-énumérable. On peut toujours subdiviser les valeurs logiques et les recomposer afin d'obtenir des ensembles de propositions n'ayant qu'une seul valeurs logique et donc disjoints. C'est pourquoi on restreint la définition des logiques, en considérant que chaque proposition ne peut posséder au plus qu'une valeur logique.
Une grammaire schème est un ensemble de règles de production où les arguments sont des couples composées d'une proposition avec variable et d'une valeur logique, et ou le résultat est un couple composé d'une proposition avec variable et d'une valeur logique. Exemple :
`g(X,Y)^"A", g(Y,f(X))^"B" |-- g(X,X)^"C"`
La définition littérale de cette règle est :
Si une proposition `alpha` de valeur logique `"A"` et une proposition `beta` de valeur logique `"B"` existent telles que l'unification de `(alpha,beta)` avec `(g(X,Y),g(Y,f(X))` aboutit, alors la règle produit la proposition `g(X,X)` de valeur logique `"C"` où on a remplacé `X` par sa valeur obtenue lors de l'unification. Autrement dit : `alpha "∈" A "et" beta "∈" B => (alpha,beta)"*"(g(X,Y),g(Y,f(X)) "∈" C`
Considérons les valeur logiques `"A","B","C","D",...`. On initialise à vide les ensembles de propositions de chaque valeur logique que l'on note pareillement que la valeur logique mais penché : `A,B,C,D,...`
`A:={ }`
`B:={ }`
`C:={ }`
`D:={ }`
On initialise à vide les ensembles des nouvelles propositions de chaque valeur logique que l'on note pareillement mais avec une côte : `A',B',C',D',...`
`A':={ }`
`B':={ }`
`C':={ }`
`D':={ }`
Pour chaque règle de dimension zéro, c'est à dire de la forme `|--alpha^"A"` faire :
`A' = A' + {alpha}`
Puis on répète indéfiniment les instrructions suivantes :
`A'':={ }`
`B'':={ }`
`C'':={ }`
`D'':={ }`
A chaque itération on énumère les couples composées d'une proposition et d'une valeur logique, `alpha^A`, qui peuvent être produit à partir de l'itération précédente en utilisant juste une règle. L'algorithme est donc en mesure de donner pour chaque couple `alpha^A`, une démonstration en profondeur d'arbre de règles appliquées la plus courte.
Une optimisation consiste à classer chaque ensemble de propositions en autant de partie qu'il y a de sorte de terme à unifier dans les règles.
Le système de Hilbert propose 4 règles de production de propositions, pemettant de produire exactement toutes les propositions tautologiques au sens classique, dans langage logique réduit à `"<"⊥,"→>"`
`"R1"` : `|-- X "→"(Y"→"X)` `"R2"` : `|-- (X"→"(Y"→"Z))"→"((X"→"Y)"→"(X"→"Z))`
`"R3"` : `|-- ((X"→⊥")"→"(Y"→⊥")) "→"(Y"→"X)`
`"MD"` : `X, X"→"Y |-- Y`
Voyons comment s'écrit l'algorithme d'énumération des productions (qui seront donc des tautologies en logique classique). Il y a deux valeurs de vérité notées {0,1} mais