Un fondement mathématique, pour être incontestable à notre époque, doit reposer sur un mécanisme parfait... au sens de la mécanique classique. Les mathématiques sont un jeu de construction, un jeu de légo, où chaque pièce s'encastre exactement dans un édifice servant de démonstration. Rien ne relève du mystère, tout est trivial..., c'est l'aspect exacte de la science mathématique. Le démonstrateur n'est finalement qu'une machine, une machine idéale, composée de rouages parfaitement emboités et sans aucun jeu. Ces machines sont décrites à l'aide d'un langage formel.
Le raisonnement, à notre ère, pour être incontestable doit pouvoir s'effectuer mécaniquement, comme un programme informatique ou une machine idéale en mécanique classique.
Nous proposons une approche globale du raisonnement mathématique dans laquelle il n'y a pas de différence de genre entre hypothèses et règles de déduction. Une théorie est un système de déduction. Chaque règle de déduction constitue un choix, une hypothèse. Et c'est l'ensemble de ces choix qui déterminera la sémantique, c'est à dire le sens réel des énoncés, ce qu'ils peuvent modéliser.
En mécanique classique, le bit est une mémoire possédant deux états possibles, exclusifs et exhaustifs. Il est représenté par une case contenant soit `0` soit `1`. Le bit représente le quanta d'information minimum qui possède une structuration de données la plus simple et, en dessous du quel, la structuration change nécessairement de forme et de nature. On résume cela en disant que le bit contient un booléen. Toute donnée structurée de n'importe quelle nature peut se décomposer en un nombre fini de bit. C'est pourquoi toute équation de n'importe quelle nature peut se décomposer en une équation bouléenne. Et l'étude des équations booléennes correspond à l'étude du calcul propositionnel.
Le calcul propositionnel est identique au calcul des équations booléennes. Les propositions élémentaires sont des inconnus booléens `X_1,X_2,X_3,...`, et les propositions sont les équations booléennes.
Voici 4 méthodes pour déterminer si une proposition est une tautologie, une antilogie, ou est indécidable :
Cette méthode consiste à procéder à tous les testes possibles en attribuant aux inconnus booléens `X_1,X_2,X_3,...` les valeurs booléennes dans l'ordre selon l'endianess big-endian, exemple pour trois inconnus : `(000,001,010,011,100,101,110,111)`. S'il y a au moins un résultat égal à `0` et un résultat égal à `1` alors la proposition est indécidable. Si les résultats sont toujours égaux à `0` alors la proposition est une antilogie. Si les résultats sont toujours égaux à `1` alors la proposition est une tautologie.
Cette méthode comprend une variante dite « méthode Shadock » qui consiste à procèder à un trés grand nombre de tests en attribuant aux inconnues `X_1,X_2,X_3,...` des valeurs booléennes au hasard. Si il y a au moins un résultat égal à `0` et un résultat égal à `1` alors la proposition est indécidable de façon certaine. Si les résultats sont toujours égaux à `0` alors la proposition est une antilogie selon un indice de confiance. Si les résultats sont toujours égaux à `1` alors la proposition est une tautologie selon un indice de confiance.
L'indice de confiance pertinent est le rapport entre le nombre d'essais effectués et le nombre d'essais distincts possibles qui est `2^n` où `n` est le nombre d'inconnus booléens présents.
On transcrit la proposition sous forme d'un polynôme dans le corps suivant `(0,1,"⇎","et")` ou bien le corps suivant `(1,0,"⇔","ou")`, qui sont des corps de caractéristique 2 que l'on renomme en `(0,1,"+","∗")`. La proposition se transcrit en un unique polynôme, une forme normale développée en enlevant les puissances doubles `x^2 = x` et en enlevant les monômes doubles `2x = x"+"x = 0`, puisque nous sommes dans un corps de caractèristique 2. La proposition est tautologique si elle est égale au polynôme `1`, elle est antilogique si elle est égale au polynôme `0`, et elle est indécidable si elle est égale à un polynôme autre que `0` ou `1`.
Cette théorie utilise les connecteurs logiques `{¬, "⇒"}` qui sont suffisants pour engendrer tous les connecteurs logiques. Et elle utilise des inconnnus que l'on note `a,b,c,...` et qui jouent ici non pas le rôle de variable booléenne mais un rôle uniquement symbolique puisque la résolution s'opère uniquement de façon syntaxique. Les connecteurs n'opèrent pas de calcul booléen, ils ne sont que symboliques.
Puis on utilise des variables supplémentaires dites libres `A,B,C,...` et le connecteur de déduction `⊢` pour écrire les règles de déduction de cette théorie.
On accumule dans un sac toutes les propositions que l'on démontre. Les règles de déduction prennent des propositions présentes dans le sac et opère un calcul pour produire le cas échéant une nouvelle proposition que l'on rajoute dans le sac. Et il y a 4 règles de déductions :
`(A, A"⇒"B)⊢ B`
`⊢ A "⇒" (B "⇒" A)`
`⊢ (A "⇒" (B "⇒" C)) "⇒" ((A "⇒" B) "⇒" (A "⇒" C))`
`⊢ ("¬"A "⇒" "¬"B) "⇒" (B "⇒" A)`
La première règle s'appelle le modus ponens. Elle prend en entrée deux propositions présentes dans le sac, et si l'unification avec l'entête réussit, elle produit une nouvelle proposition que l'on rajoute dans le sac. Les 3 autres règles ont une liste vide comme entête et engendrent des propositions où `A,B,C` parcourent toutes les propositions du langage.
Ce moteur produit exactement l'ensemble de toutes les propositions tautologiques. Pour détecter les propositions indécidables, il faut un autre algorithme.
Si on commence l'algorithme avec un sac contenant une proposition initiale `varphi`, on produit alors exactement l'ensemble de toutes les déductions possibles de `varphi`.
Cette théorie utilise les seuls connecteurs logiques `{¬, "et", "ou" }` et des inconnus `a,b,c,...`. Même remarque que précédement, ces inconnnus jouent ici non pas le rôle de variable booléenne mais un rôle uniquement symbolique puisque la résolution s'opère uniquement de façon syntaxique. Les connecteurs n'opèrent pas de calcul booléens, ils ne sont que symboliques.
On appel littéral, un inconnu préfixé ou non par le connecteur de négation. Les littéraux sont `a,"¬"a,b,"¬"b,c,"¬"c,...`. On appel proposition une composition close de connecteurs et d'inconnus. On appel clause une disjonction de littéraux.
L'étude de la logique propositionnelle, nous montre que toute proposition se ramène à une conjonction de clauses. En effet, prenez par exemples la proposition `(a"⇒"b)"⇒"c`. Cette proposition est équivalente à `(a "ou" c) "et" ("¬"b "ou" c)`. Les règles de déduction du calcul propositionnel se décrivent simplement si on décompose ainsi les propositions en des conjonctions de clauses.
Une clause est un couple d'ensembles finis d'inconnus `(A,B)`, le premier ensemble regroupe les inconnus affirmés dans la clause, et le second ensemble regroupe les inconnus négativés dans la clause. Par exemple :
`A={a,b,c]`
`B={d,e}`
`(A,B) = ({a,b,c},{d,e}) = a" ou "b" ou "c" ou ¬"d" ou ¬"e`
On choisit une proposition `varphi` de départ que l'on décompose en une conjonction de clauses. On considère un sac contenant ces clauses de départ. Chaque clause contenue dans le sac apporte une contrainte. Le sac correspond à une grande conjonction. Puis on accumule dans le sac, toutes les clauses que l'on démontre. Et pour cela on applique 5 règles :
Le moteur s'arrête si la conjonction contient la clause vide et auquel cas la proposition `varphi` est une antilogie, ou si la conjonction devient vide et auquel cas la proposition `varphi` est une tautologie.
Pour détecter les propositions indécidables, il faut un autre algorithme.
Par négation nous obtenons le mécanisme symétrique de résolution des disjonctions d'états :
On appel état une disjonction de littéraux.
L'étude de la logique propositionnelle, nous montre que toute proposition se ramène à une disjonction d'états. Les règles de déduction du calcul propositionnel se décrivent simplement si on décompose les propositions en disjonctions d'états.
Un état est un couple d'ensembles finis d'inconnus `(A,B)`, le premier ensemble regroupe les inconnus affirmés dans l'état, et le second ensemble regroupe les inconnus négativés dans l'état. Par exemple :
`A={a,b,c]`
`B={d,e}`
`(A,B) =({a,b,c},{d,e}) = a" et "b" et "c" et ¬"d" et ¬"e`
On choisit une proposition `varphi` de départ que l'on décompose en une disjonction d'états. On considère un sac contenant ces états de départ. Chaque état contenu dans le sac apporte une alternative possible. Le sac correspond à une grande disjonction. Puis on accumule dans le sac tous les états que l'on produit. Et pour cela on applique 5 règles de production :
Le moteur s'arrête si la disjonction contient l'état vide et auquel cas la proposition `varphi` est une tautologie, ou si la disjonction devient vide et auquel cas la proposition `varphi` est une antilogie.
Pour détecter les propositions indécidables, il faut un autre algorithme.
Pour pouvoir étendre ce système de déduction à des langages logiques plus riches, on va opter pour une cinquième méthode dite "naturelle" qui introduit et élimine chaque connecteur logique par une règle de déduction spécifique.
Le système de déduction naturelle utilise les connecteurs logiques `{¬, "⇒", "et", "ou" }` et des inconnus `a,b,c,...`. Même remarque que précédement, ces inconnnus jouent ici non pas le rôle de variable booléenne mais un rôle uniquement symbolique puisque la résolution s'opère uniquement de façon syntaxique. Les connecteurs n'opèrent pas de calcul booléens, ils ne sont que symboliques. Par commodité on ajoute au langage, l'élément antilogique `"⊥"` qui représente la contradiction et le faux. Autrement dit le système de déduction naturelle utilise les connecteurs logiques `{"⊥", ¬, "⇒", "et", "ou" }` et des inconnus `a,b,c,...`.
Une proposition est une composition close de connecteurs logiques et d'inconnus. L'ensemble des propositions est appelé le langage propositionnel.
Les règles de déduction sont construites à l'aide du langage propositionnel augmenté du connecteur multi-aire de déduction `"⊢"` et de variables libres `A,B,C,...`. Cela forme un nouveau langage plus riche appelé le langage propositionnel étendu et qui permet d'écrire des règles de déduction.
Puis on considère le procéder d'unification qui permet d'unifier une variable libre à n'importe quelle proposition (du langage propositionnel étendu) et pouvant contenir de telles variables libres. Remarquez que ce procédé d'unification permet de définir des propositions récurcives que l'on exclut dans un premier temps.
La règle de déduction possèdent une entête qui est une liste de propositions (du langage propositionnel étendu) et un corps qui est une proposition (du langage propositionnel étendu). Par exemple, considérons la règle suivante :
`(A"⇒"B, A" et "C) |-- B" et "C`
Cette règle s'applique par exemple au couple de propositions suivantes `(a"⇒"b, a" et "¬b)`. Elle procéde une unification entre son entête et le couple de propositions en question. Si l'unification réussie ce qui est le cas ici, les variables libres étant affectées comme suit : `A"="a,B"="b,C"=¬"b`, la règle produit alors son corps dans lequel les variables libres affectées sont remplacées par ce qu'elles contiennent `b" et ¬"b`, et les eventuelles variables libres non affectées c'est à dire qui n'apparaissent que dans le corps de la règle, peuvent prendre comme valeurs toutes les propositions du langage.
Ce type de règle de déduction est pertinent pour plusieurs raisons. D'abord il s'inspire d'un principe trés général d'apprentissage par similitude. Et surtout, il s'appuit sur un mécanisme d'unification qui, lorsqu'il est bien programmé, s'avère de complexité linéaire.
Notez bien que ces régles de déduction ne font pas partie du langage propositionnel mais du langage propositionnel étendu.
La définition du connecteur de déduction `"⊢"` différe de celle de l'implication `"⇒"`. La proposition `A"⊢"B` signifie que l'on peut déduire `B` de `A` par un procédé mécanique qui est celui de la démonstration tel que défini par la règle elle-même, alors que la proposition `A"⇒"B`, sans la règle de déduction dite du modus ponens `(A, A"⇒"B)⊢B`, ne permet pas de déduire `B` de `A`. Cette distinction est inutile en logique propositionnelle, mais elle devient nécessaire si on enrichie le langage en une logique du premier ordre. Car la théorie devenant incomplète, il se peut qu'une proposition `B` ne soit pas démontrable par `A` et que sa négation `"¬"B` non plus, `"¬"(A"⊢"B) "et" "¬"(A"⊢¬"B)`, et en identifiant le connecteur de déduction et le connecteur d'implication, on aboutirait à la contradiction suivante `"¬"(A"⇒"B) "et" "¬"(A"⇒¬"B)`.
Un moyen simple d'étudier ces théories est la façon empirique en programmant un moteur qui applique ces règles de déduction. Un tel moteur comprend un algorithme d'unification et un générateur de propositions. Voir Implémentation des langages d'opérateurs.
---- 9 avril 2014 ----
Les règles de déduction naturelle sont au nombre de 12 :
Règle d'introduction du `"et"` `(A, B)⊢ A "et" B` Règles d'élimination du `"et"` `(A "et" B) ⊢ A`
`(A "et" B)⊢ B`Règles d'introduction du `"ou"` `A⊢(A "ou" B)`
`B⊢(A "ou" B)`Règles d'élimination du `"ou"` `(A "ou" B,A"⇒"C,B"⇒"C)⊢C` Règle d'introduction du `"⇒"` `(A"⊢"B)⊢(A"⇒"B)` Règle d'élimination du `"⇒"`
dite règle du modus ponens`(A, A"⇒"B)⊢B` Règle d'introduction du `"¬"` `(A"⊢⊥")⊢ "¬"A` Règle d'élimination du `"¬"` `(A, "¬"A)⊢ ⊥` Règle "Ex falso" `"⊥" ⊢ A` Règle "Ab absurdo" `("¬"A"⇒⊥")⊢ A`
Mais une difficulté apparait. Certaines prémisses de ces règles ne sont pas des propositions du langage propositionnel mais sont des propositions du langage propositionnel étendu. La règle d'introduction de l'implication ainsi que la règle d'introduction de la négation ont comme prémisses non pas l'existence d'une proposition dans le sac, mais l'existence d'une démonstration.
---- 9 avril 2019 ----
| Règle d'identité | `"⊤"⊢ (A "⊢" A)` |
Puis il faut ajouter les règles relatives au symbole de déduction `"⊢"` ; La règle d'introduction du `"⊢"`, et la règle d'élimination du `"⊢"` qui est déjà présente puisqu'elle correspond à la règle d'introduction du `"⇒"`.
Règle d'introduction du `"⊢"` `(A"⇒"B)⊢(A"⊢"B)`
Règle d'introduction du `"et"` `(H"⊢"A, G"⊢"B) ⊢ (H,G "⊢" (A "et" B))` Règles d'élimination du `"et"` `(A "et" B) ⊢ A`
`(A "et" B)⊢ B`Règles d'introduction du `"ou"` `A⊢(A "ou" B)`
`B⊢(A "ou" B)`Règles d'élimination du `"ou"` `(A "ou" B,A"⇒"C,B"⇒"C)⊢C` Règle d'introduction du `"⇒"` `(A"⊢"B)⊢(A"⇒"B)` Règle d'élimination du `"⇒"`
dite règle du modus ponens`(A, A"⇒"B)⊢B` Règle d'introduction du `"¬"` `(A"⊢⊥")⊢ "¬"A` Règle d'élimination du `"¬"` `(A, "¬"A)⊢ ⊥` Règle "Ex falso" `"⊥" ⊢ A` Règle "Ab absurdo" `("¬"A"⇒⊥")⊢ A`
Mais attention cette dernière règle n'est pas anodine. Elle signifie que si une proposition `B` est conséquence d'une proposition `A` alors il existe une démonstration de `B` à partir de `A`, ce qui, en d'autre terme, affirme la complétude du système de démonstration. Cette complétude existe bien dans le langage propositionnel, c'est pourquoi cette règle est valable
Délors les deux symboles `⊢ , ⇒ ` sont équivalents du fait des deux règles suivantes :
`(A"⇒"B)⊢(A"⊢"B)`
`(A"⊢"B)⊢(A"⇒"B)`
C'est pourquoi en logique classique et dans le langage propositionnel le connecteur d'implication et de déduction sont fusionné en le connecteur `"→"` . Et cela rend inutil la r ègle d'introduction de l'implication. Les règles de déductions naturelle sont alors :
Règle d'introduction du `"et"` `(A, B)→ A "et" B` Règles d'élimination du `"et"` `(A "et" B) → A`
`(A "et" B) → B`Règles d'introduction du `"ou"` `A→(A "ou" B)`
`B→(A "ou" B)`Règles d'élimination du `"ou"` `(A "ou" B,A"→"C,B"→"C)→C` Règle d'élimination du `"⇒"`
dite règle du modus ponens`(A, A"→"B)→B` Règle d'introduction du `"¬"` `(A"→⊥")→ "¬"A` Règle d'élimination du `"¬"` `(A, "¬"A)→ ⊥` Règle "Ex falso" `"⊥" → A` Règle "Ab absurdo" `("¬"A"→⊥")→ A`
L'ensemble de ces 13 règles constitue un moteur qui va produire toutes les tautologies dans le langage propositionnel étendu.
Tout est langage. Dans une démarche minimaliste où l'on ne veut poser aucune hypothèse, où l'on ne veut dépendre d'aucune prémisse, le premier choix qu'il convient de faire est de définir un langage. Et ce choix va limiter notre pouvoir d'expression tout en nous en donnant un. On choisit un langage d'opérateurs, et on choisit des opérateurs d'arité fixe, parce que l'étude des opérateurs d'arité variable montre qu'ils peuvent toujours être remplacés de façon équivalente par deux opérateurs binaires.
Un language d'opérateurs est défini par sa présentation qui est un ensemble énumérable d'opérateurs. Par exemple la présentation `L= {a,b,f"(.)",g"(.,.)"}` désigne deux opérateurs zéro-aire `a` et `b` qui constituent des éléments, un opérateur unaire `f` et un opérateur binaire `g`. Les opérateurs `{a,b,f"(.)",g"(.,.)"}` sont dit générateurs car ils engendrent le langage par composition close.
Un terme est une composition close d'opérateurs appartenant à `L`. L'ensemble des termes du langage forme le domaine de Herbrand que l'on note `"<"L">"` ou directement `"<"a,b,f"(.)",g"(.,.)>"` :
`"<"L">" = {a, f(a), f(f(a)), f(b), f(g(b,a)), g(a,b),...}`
C'est l'ensemble des éléments que l'on peut construire, ou désigner, avec le langage `L`.
Le « langage `L` » désigne l'ensemble `"<"L">"` c'est à dire le domaine de Herbrand, et réciproquement « la présentation du langage `<L>` » désigne l'ensemble `L`. La présentation du langage est l'ensemble des opérateurs générateurs du langage. Ces opérateurs sont dits générateurs parcequ'ils engendrent le langage `L`.
Par contre les opérateurs définis par exemples comme suit : `x|->g(x,x)`, `(x,y)|->g(y,x)`, `x|->f(f(x))` n'appartienent pas à la présentation de `L`, et donc ne sont pas des opérateurs générateurs. Néanmoins ils se définissent dans ce langage en question augmenté du méta-connecteur `vecx|->` qui précise l'ordre des variables muettes. Autrement dit, ils sont définissables selon le niveau 3 (composition générale) dans le langage d'opérateurs en question. L'ensemble des opérateurs ainsi définissable se note `"≪"L"≫"`.
On remarque que les opérateurs générateurs d'arité `n` restreints au domaine de Herbrand sont des applications injectives distinctes appartenant à `"<"L">"^n"↪""<"L">"`, et que les opérateurs générateurs d'arité `0` sont des éléments distincts appartenant à `"<"L">"`.
Le but d'un langage est de désigner autre chose que lui-même. Un terme désigne un élement. Le terme est le signifiant. L'élément est le signifié. Dans une démarche constructive, cette séparation se fait dans un premier temps, à l'identique, de telle sorte que deux termes distincts désignent deux éléments distincts. On parlera d'une désignation injective. L'ensemble des termes est regroupé dans le langage. L'ensemble des éléments est regroupé dans la structure qui est le domaine de Herbrand et, qui est dite libre du fait de cette désignation injective c'est à dire telle que deux termes distincts désignent nécessairement deux éléments distincts.
Ainsi le langage d'opérateurs `L` définie une structure libre, appelée aussi le domaine de Herbrand, noté `"<"L">"`, qui comprend toutes les compositions closes possibles d'opérateurs générateurs, et que nous appellons termes ou éléments. Par exemple le terme `g(a,f(a))` désigne un élément. Et deux termes distincts désignent obligatoirement deux éléments distincts, principe d'une désignation injective des éléments qui coïncide avec le fait de ne perdre aucune information dans le procédé désignatif.
On remarquera alors, que le langage d'opérateurs n'apporte aucune information sur la situation des éléments qu'il désigne. Il ne fait que leur donner un nom, et il définit par ailleurs chaque opérateur générateur comme une injection dans l'ensemble des éléments désignables, ou dits constructibles, par le langage. Par exemple si l'opérateur `f"(.)"` fait partie de la présentation du langage, alors quelque soit les éléments `x` et `y` désignables par ce langage, nous avons la propriété suivante `x"≠"y => f(x)"≠"f(y)`. Remarquez que cette formulation ne fait pas encore partie de notre langage formel puisque les symboles `"="` et `"≠"` n'y sont pas encore définis. C'est aussi pourquoi à cette étape, le langage d'opérateurs ne peut définir qu'une structure libre.
On accordera le rôle qui consiste à apporter une information sur la situation des éléments, à une autre sorte d'opérateur appelé prédicat. Le prédicat prend en argument un n-uplet d'éléments et retourne comme résultat non pas un élément mais un booléen, qui constitue une information sur ce n-uplet d'éléments et que nous appellons prédication. Le prédicat n-aire est donc une fonction caractéristique. Il partitionne en deux, l'ensemble des n-uplets d'éléments désignables. il définit un sous-ensemble au sens classique, de l'ensemble des n-uplets d'éléments désignables.
Un langage prédicatif comprend un langage d'opérateurs `L` que l'on munie d'un ensemble énumérable de prédicats `ccP`. Conventionnellement, les opérateurs générateurs sont notés en premier en minuscule et la liste est entourée de crochet `"< >"`, puis les prédicats sont notés en second en majuscules et placés après en étant entourée de braquette `{ }`. Par exemple, le langage prédicatif `"<"a,b,f"(.)>", {K, E"(.)",R"(.,.)"}` que l'on désigne aussi par `"<"L">",ccP`, désigne deux opérateurs générateurs d'arité zéro `a` et `b` qui constituent deux éléments distincts, un opérateur générateur unaire `f` qui appliqué à un élément quelconque `x` produit l'élément désigné par `f(x)`, un prédicat d'arité zéro `K` qui constitue un paramètre boolean, un prédicat unaire `E` qui appliqué à un élément quelconque `x` produit un booléen, autrement dit, `E` représente un ensemble d'éléments désignables que l'on note avec la même lettre que celle du prédicat, `E sube "<"L">"`, et enfin un prédicat binaire `R` qui constitue une relation, et qui appliqué à un couple d'éléments quelconques `(x,y)` produit la prédication `R(x,y)`, autrement dit, `R` représente un ensemble de couples d'éléments désignables que l'on note avec la même lettre que celle du prédicat, `R sube "<"L">"^2`.
Le langage d'opérateurs regroupe tous les termes qui sont par définition des compositions closes d'opérateurs générateurs du langage, et forme le domaine de Herbrand. Par exemples : `a, f(a), f(f(b))`.
Le langage prédicatif regroupe toutes les prédications qui sont obtenues par composition close d'un prédicat et des termes du langage d'opérateurs. Chaque prédication correspond à une adresse mémoire contenant un booléen. Par exemples : `K, E(a),R(a,f(b))`
On a ainsi fait le choix qui accorde la plus grande liberté possible au langage, tout en séparant opérateurs générateurs et prédicats. Les opérateurs générateurs nomment les éléments, et donc construisent la structure libre associée. Les prédicats sont les seules composantes du langage à contenir de l'information, une information booléenne sur les n-uplets d'éléments, en indiquant s'il appartiennent où non à un ensemble, l'ensemble portant le même nom que le prédicat. Les prédicats construisent au dessus de la structure libre, l'univers. C'est un réseau infini de cases mémoires, une matrice infinie où chaque prédicat zéro aire, chaque prédicat unaire complété par chaque élément de la structure libre, chaque prédicat binaire complété par chaque couple d'éléments de la structure libre..., chaque prédicat n-aire complété par chaque n-uplets d'éléments de la structure libre..., appelé aussi adresse mémoire, y possèdent une case mémoire distincte contenant une valeur booléenne pouvant être définie librement. Dans l'exemple `"<"a,b,f"(.)>", {K, E"(.)",R"(.,.)"}`, cela revient à la libre définition d'une valeur booléenne `K`, d'un ensemble `E` d'éléments désignables, `E sube "<"L">"`, et d'un ensemble `R` de couples d'éléments désignables, `R sube "<"L">"^2`.
La prédication apporte une information booléenne sur son n-uplet d'éléments qui lui sert d'argument, et détermine ainsi une caractéristique du monde. Le monde est une structure qui est enrichie de cette information pour chaque prédication.
Chaque prédication est un inconnu booléen. Par exemple la prédication `R(a,f(f(a)))` désigne un inconnu booléen. Et deux inconnus booléens sont distincts, c'est à dire constituent deux mémoires booléennes d'adresses distinctes, si les prédications qui les désignent sont d'expression distinctes. C'est encore le principe d'une désignation injective des adresses mémoires qui coïncide avec le fait de ne perdre aucune information dans le procédé désignatif.
On remarque qu'un prédicats d'arité `0` est une variable booléenne. On remarque qu'un prédicat d'arité `n` est une application de `"<"L">"^n"→"{0,1} `. Un prédicat est donc une fonction caractéristique. Un prédicat d'arité `n` définit donc un ensemble de n-uplet d'éléments désignables, autrement dit, un sous-ensemble du domaine de Herbrand, et on désigne cet ensemble par la même lettre que le prédicat. Par exemple :
`R(a,b) <=> (a,b)"∈"R`
On ajoute le connecteur logique de négation `¬` dans notre langage formel pour pouvoir écrire que la prédication `R(a,b)` est égale à `0` en notant simplement `"¬"R(a,b)`, et que la prédication `R(a,b)` est égale à `1` en notant simplement `R(a,b)`. Avec cette convention d'écriture, les uns sont appellés littéraux négatifs puisque préfixés par le connecteur de négation `¬`, et les autres sont appelés littéraux affirmatifs.
`"¬"R(a,b) <=> (a,b)"∉"R`
Chaque prédication est une case mémoire contenant un booléen. L'ensemble de toutes ces cases mémoires constituent l'univers. Un monde est une instanciation de cet univers, c'est à dire dans lequel chaque case mémoire est fixée à une valeur `0` ou `1`. L'univers est l'ensemble des mondes possibles. Il y a donc deux façons de percevoir ce qu'est l'univers. C'est une liste des cases mémoires booléennes qui permet de définir complétement un monde, ou bien c'est l'ensemble des mondes possibles.
Là où il faut être prudent, c'est que ces mondes sont constitués d'une infinité énumérable de cases mémoires booléennes et donc sont suceptibles de contenir une quantité d'information infinie ce qu'aucun objet physique réel n'est capable de faire. Et donc, il y a deux sortes de monde :
Dans ce dernier cas, il faut admettre que ces mondes sont immanents puisque non-constructibles. Ils sont donc préalablement définis par une infinité de choix arbitraires que nous ne pourrions évidement pas créer nous-même.
La syntaxe décrit le signifiant, tandis que la sémantique décrit le signifié. Chaque terme détermine un élément du monde. Chaque prédication détermine une caractéristique du monde. Quelle est cette caractéristique ? qu'est ce que désigne une prédication ? Ce sont les appartenance aux ensembles prédéfinis vus précédement. Dans l'exemple, c'est le paramètre booléen `K`, les ensembles `E` et `R`. Mais il est possible de répondre à cette question d'une façon plus générale, sans y répondre vraiment, en se plaçant à une échelle d'ordre supérieur, simplement par une définition, en répondant à la question « Qu'elle est sa sémantique ? ». La sémantique d'une prédication est l'ensemble des mondes qui la satisfait.
Le monde `M` est dit « satisfaire une prédication `R(a,b)` », ce qui ce note `M"⊨"R(a,b)`, si et seulement si la prédication `R(a,b)=1`, et qui par convention se note simplement `R(a,b)`, correspond bien à l'information mémorisée par `M` à l'adresse `R(a,b)`.
La signification de la prédication `R(a,b)` est que le couple `(a,b)` appartient à l'ensemble `R`. La sémantique de la prédication `R(a,b)` est donné par l'ensemble des mondes la satisfaisant :
`R(a,b) <=> (a,b)"∈"R`
`R(a,b) ≡ {M "/" M"⊨"R(a,b)}`
Comme les booléens se composent à l'aide des connecteurs booléens, les littéraux se composent avec ces mêmes connecteurs, appelés pour l'occasion connecteurs logiques, pour produire des propositions qui, comme les littéraux, ont une valeur booléenne déterminée par ces derniers dans chaque monde. Une proposition est une composition close de connecteurs et de littéraux
Le langage des propositions regroupe toutes les propositions qui sont obtenues par la composition close de connecteurs logique et de littéraux. Par exemple : `R(a,f(b))=>R(b,a)`
La relation de satisfaisabilité `"⊨"` qui s'applique aux mondes et aux littéraux, s'étend aux propositions, puis s'étend en fin de course aux ensemble de mondes, c'est à dire aux sous-ensembles de l'univers. Et dans l'ensemble des ensembles de mondes, c'est à dire dans l'ensemble des sous-ensembles de l'univers, elle correspond à la relation d'inclusion, c'est pourquoi on peut la noter aussi par le symbole `"⊆"`. Et le symbole `≡`, précédement utilisé, désigne l'égalité sémantique.
Cela permet de définir ce qu'est la conséquence sémantique. Etant donné deux propositions `P, Q`, l'expression `P"⊨"Q`, ou `P"⊆"Q` signifie que `Q` est une conséquence sémantique de `P`, c'est à dire que l'ensemble des mondes satisfaisant `P` est inclus dans l'ensemble des mondes satisfaisant `Q`, autrement dit, que si un monde satisfait `P` alors il satisfait `Q`. Par contre la conséquence syntaxique qui sera décrite plus loin, ne met en oeuvre que des règles formelles de raisonnement que l'on se sera choisies, et ne s'applique que sur la syntaxe des propositions.
Pour récapituler, considérons par exemple le langage prédicatif suivant `"<"a,b,f"(.)>", {K, Q"(.)", R"(.,.)"}`.
Les opérateurs générateurs d'arité `0` sont des éléments distincts appartenant `"<"L">"`. Les opérateurs générateurs d'arité `n` sont des applications injectives distinctes, appartenant à `"<"L">"^n"→""<"L">"`.
`"<"L">"={a, f(a), f(f(a)), f(b), f(g(b,a)), g(a,b),...}`
Les prédicats d'arité `0` sont des inconnus booléens qui sont distingués par leur noms. Les prédicats d'arité `n` sont des applications appartenant à `"<"L">"^n"→"{0,1} ` qui sont distingués par leur noms, et qui correspondent donc à des ensembles de n-uplet désignables que l'on désigne par la même lettre que le prédicat. Exemple quelque soit un élément `x` de `"<"L">"` :
`Q(x) <=> x "∈"Q`
`Q(a), K, R(a,f(a)), "¬"R(a,f(b)), "¬"K, "¬"Q(f(f(a)))`
Le prédicat d'égalité `="(.,.)"` est à part, car il joue un rôle spécial. Etant donné deux termes distincts du langage, c'est à dire deux éléments distincts de la structure libre, par exemple l'élément `f(f(a))` et l'élément `a`, la prédication `f(f(a))"="a` va modifier la construction de la structure en liant ces deux éléments par un lien transitif, symétrique et réflexif qu'est l'égalité. Ce lien d'égalité est une relation d'équivalence. La structure s'obtient en quotientant la structure libre par la relation d'équivalence. Les éléments de la structure sont les classes d'équivalence de la structure libre. Les relations d'équivalences peuvent s'ajouter pour former des relations d'équivalence aux classes d'équivalence plus vastes, c'est pourquoi le même raisonnement s'applique pour une conjonction d'égalités qui établit une relation d'équivalence aux classes d'équivalence plus vastes. Mais cela ne s'applique pas pour une disjonction d'égalités car celle-ci ne permet pas d'établir une relation d'équivalence. Par exemple :
`("<"a,b,f"(.)>")/{f(f(a))"="a "et" f(b)"="a} = {a,b,f(a)}`
Le prédicat d'égalité `"=(.,.)"` appliqué à un couple d'éléments `(x,y)` désignable par le langage, produit la prédication `x"="y` qui a pour signification que les deux éléments `x` et `y` sont égaux. Ce prédicat constitue une relation d'équivalence sur l'ensemble des termes c'est à dire des éléments de la structure libre. Autrement dit, la relation est reflexive, symétrique et transitive. Les termes ne désignent plus de façon injective les éléments. Ce sont les classes d'équivalence qui désignent de façon injective les éléments. Ce prédicat d'égalité entraine des contraintes sur lui-même, à savoir que c'est une relation d'équivalence (reflexive, symétrique et transitive). Quelque soit `x,y,z` des termes du domaine de Herbrand, nous avons :
`x"="x`
` (x"="y)=>(y"="x)`
`(x"="y)" et "(y"="z)=>(x"="z)`
Notez la priorité syntaxique des connecteurs et déclarateurs de la plus faible à la plus élevée ` =, <=>, =>, "et"`.
Le prédicat d'égalité entraine des contraintes d'égalité sur les opérateurs du langage, à savoir que les opérateurs unaires appliqués à `x` doivent produire le même éléments que les opérateurs unaire appliqué à `y` si `x"="y`. Et que les opérateurs binaire appliqués à `(x_1,x_2)` doivent produire le même élément que les opérateurs binaires appliqués à `(y_1,y_2)` si `(x_1,x_2)"="(y_1,y_2)`. Et de même pour les `n`-uplet s'il y a des opérateurs d'arité `n`. Quelque soit les opérateurs générateurs `f"(.)", f"(.,.)",...`, quelque soit `x,y,x_1,y_1,x_2,y_2,...` des termes du domaine de Herbrand, nous avons :
` (x"="y) => (f(x)"="f(y))`
` (x_1"="y_1)" et "(x_2"="y_2) => (f(x_1,x_2)"="f(y_1,y_2))`
` ...`
Le prédicat d'égalité entraine des contraintes sur les autres prédicats du langage, à savoir que les prédications relatives à `x` doivent être identiques aux prédications relatives à `y` si `x"="y`. Et que les prédications relatives à `(x_1,x_2)` doivent être identiques aux prédications relatives à `(y_1,y_2)` si `(x_1,x_2)"="(y_1,y_2)`. Et de même pour les `n`-uplet s'il y a des prédicats d'arité `n`. Quelque soit les prédicats `P"(.)", P"(.,.)",...`, quelque soit `x,y,x_1,y_1,x_2,y_2,...` des termes du domaine de Herbrand, nous avons :
`(x"="y) => (P(x)"="P(y))`
`(x_1"="y_1)" et "(x_2"="y_2) => (P(x_1,x_2)"⇔"P(y_1,y_2))`
`...`
Le symbole `"⇔"` n'appartient pas à notre langage des propositions. Lorsque nous rencontrons une expression de la forme `A"⇔"B`, nous la traduisons par l'une ou l'autre des propositions suivantes :
`(A"⇒"B) "et" (B"⇒"A)`
`(A "et" B) "ou" ("¬"A "et" "¬"B)`
Si on n'envisage aucune extension du langage d'opérateurs, et donc pas d'usage de variable ni de quantificateur, alors le prédicat d'égalité n'introduit aucune autre contrainte.
Considérons par exemple le langage prédicatif suivant : `"<"a,b,f"(.)",g"(.,.)>",{A"(.)",R"(.,.)"}`. L'introduction du prédicat d'égalité va ajouter juste 7 règles d'égalité. Quelque soit les termes `x,y,z,t` nous avons :
`x"="x`
`(x"="y) |-- (y"="x)`
`(x"="y) "et" (y"="z) |-- (x"="z)`
`(x"="y) |-- (f(x)"="f(y))`
`(x"="y) |-- (A(x)"⇔"A(y))`
`(x"="z) "et" (y"="t) |-- (g(x,y)"="g(z,t))`
`(x"="z) "et" (y"="t) |-- (R(x,y)"⇔"R(z,t))`
Ces règles peuvent être écrites comme des propositions en remplaçant le symbole de déduction `|--` par le symbole d'implication `=>`. Cela revient au même car nous avons la règle du modus ponens `(A, A"⇒"B)⊢B`, et la règle d'introduction du `"⊢"` qui s'écrit `(A"⇒"B)⊢(A"⊢"B)`.
---- 17 mars 2019 ----
Une démonstration est un arbre où chaque noeud correspond à une règle de déduction. La tête du noeud contient le corps de la règle c'est à dire sa conclusion. Et les fils du noeud contiennent chacun dans l'ordre une hypothèse de la règle, c'est à dire l'entête de la règle. Chaque règle se comporte comme un opérateur `n`-aire où `n` est le nombre de ses hypothèses. Chaque proposition démontrée se comporte comme un opérateur zero-aire. Ces opérateurs se composent entre eux pour former des arbres, formant d'autres opérateurs, qui constituent de nouvelles règles de déduction. Par exemple considérons les trois règles suivantes :
`(A "et" B) ⊢ A`
`(A "et" B)⊢ B`
`(A, A"⇒"B)⊢B`
Que l'on note sous forme d'opérateur :
`f = (A "et" B) ↦ A` (Opérateur unaire)
`g = (A "et" B) ↦ B` (Opérateur unaire)
`h = (A, A"⇒"B) ↦ B` (Opérateur binaire)
On utilise la composition série des opérateurs `n`-aires qui reporte dans l'entête la concaténation des entêtes des arguments dans l'ordre de leur apparition. Ainsi la composition `h(f,g)` est égale à `(X,Y)↦ h(f(X),g(Y))`. Après unification, cette composition aboutie à l'opérateur suivant :
`h(f,g) = (A "et" B, C "et" (A"⇒"D)) ↦ D`
Qui constitue une nouvelle règle de déduction.
Mais on procède tout de suite à une simplification. Les arguments d'une démonstration, qui peuvent être des propositions avec variables libres, peuvent être utilisés plusieurs fois dans la même démonstration et avec la même instantiation, structurant la démonstration non pas sous forme d'un arbre mais sous forme d'un graphe orienté sans boucle, et qui se définit par une composition générale d'opérateurs. Ainsi à partir de l'exemple précédent, la composition générale suivante :
`X |-> h(f(X),g(X))`
va constituer la règle de déduction suivante :
` (A "et" A"⇒"B) ↦ B`