Qu'est-ce qu'une proposition mathématique ? C'est en voulant répondre à cette question que l'on va décrire les règles du raisonnement, en partant de son aspect purement mécanique. Et à bien y regarder, il s'agit plus précisement d'une 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. Le démonstrateur peut avancer à l'aveugle et appliquer la méthode Shadok qui consiste à tester au hasard. Et dans ce cas, il n'est finalement qu'une machine produisant des démonstrations, une machine idéalisée, composée de rouages parfaitement emboités et sans aucun jeu. Ces machines sont décrites à l'aide d'un langage formel.
Une proposition est écrite dans un langage d'alphabet fini, et doit être de taille finie. Et il existe une machine capable de décider en un temps fini si une chaine de caractères constitue une proposition correctement écrite, c'est à dire satisfaisant la syntaxe du langage en question. Délors, l'ensemble des propositions possibles `L` est énumérable. Il existe une machine qui énumère toutes les propositions possibles du langage `L`. Nous résumons cela par la phrase « On peut énumérer toute les propositions ».
Selon la hierchie de Chomsky, cela définit la catégorie des langages décidables, c'est à dire défini par une grammaire formelle et dont le complémentaire doit être également défini par une grammaire formelle. La hierarchie de Chomsky dévoile des catégories de langages plus simples que sont les langages contextuels, et dévoile des langages encore plus simples que sont les langages algébriques. On se restreint à l'étude de ces derniers.
Chaque langage algébrrique peut se ramener à un langage de composition d'opérateurs d'arités fixes de type fini. On suppose donc que le langage logique `L` est un langage de composition d'opérateurs d'arité fixes et qu'il est engendré par un nombre fini d'opérateurs générateurs.
La proposition est une composition d'opérateurs générateurs, qui en constitue sa syntaxe. Mais elle possède aussi une sémantique. Dans la conception classique, la proposition a pour rôle de décrire une propriété d'un modèle. Le modèle est l'expérience ultime qui donne une valeur de vérité à la proposition. Si la proposition `a` est vrai dans le modèle `M`, nous dirons que le modèle `M` réalise la proposition `a`, ou encore que `M` satisfait la proposition `a` et on notera :
`M |== a`
Le méta-opérateur `|==` teste si la proposition `a` est vrai dans le modèle `M`. La conception classique suppose de plus que le modèle est complet et donc qu'il tranche toutes les propositions en leur assignant une valeur de vérité, vrai ou faux. Autrement dit, la proposition possède une valuation booléenne qui en constitue sa sémantique classique.
Néanmoins rien ne garantit l'existence de tel modèle. C'est pourquoi on défini parfois une seconde conception de modèle appelé monde, qui ne tranche pas la proposition `a` directement, mais qui tranche seulement la question de sa démontrabilité, qui elle, est déterminée par le système de démonstration choisi, et par un ensemble de propositions pouvant être infini, le monde se différentiant de la proposition en ce sens.
Une preuve est un objet de taille finie, vérifiable par des moyens mécaniques rudimentaires, qui comporte une conclusion et des hypothèses. La preuve repose sur l'usage de règles de déduction rudimentaires appliquées en cascades à des hypothèses pour aboutir à une conclusion.
Autrement dit : La preuve est un arbre ou chaque noeud est une proposition qui est déduite de ses fils par une règle de déduction, et où chaque feuille est une hypothèse ou une proposition qui est déduite par une règle de déduction sans hypothèse. Et la racine de l'arbre en est la conclusion.
On augmente le langage `L` afin de pouvoir écrire les preuves. Cela se fait en ajoutant un opérateur capable de créer de tels arbres de propositions de `L`, c'est à dire des arbres où les noeuds et les feuilles sont des propositions de `L` et où les feuilles sont marqués comme hypothèse ou comme déduite sans hypothèse. Mais on ne souhaite pas introduire d'opérateur d'arité variable. On ajoute donc un opérateur unaire `⤚"(.)"`, un opérateur binaire `⤚"(.,.)"`, un opérateur ternaire `⤚"(.,.,.)"`, un opérateur quaternaire `⤚"(.,.,.,.)"` et peut être davantage.... Et on choisit une syntaxe mettant en évidence les conclusions, qui est de la forme `"⤚"b`, `(a⤚b)`, `(a,b⤚c)`, `(a,b,c⤚d)`.
Déjà avec ces `4` opérateurs ajoutés au langage `L`, on peut construire tous les arbres de propositions de `L` où les noeuds ont au plus `3` fils, et où les feuilles sont marqués comme étant une hypothèse ou une proposition déduite sans hypothèse. En cela, la preuve est un objet plus riche qu'une proposition, et comprend les propositions. Elle possède une valeur de vérité dont le calcul est rudimentaire, et qui ne dépend pas du modèle car elle ne dépend que de la syntaxe des opérateurs. Chaque preuve possède une valeur de vérité, qui est vrai si tous ses noeuds et toutes ses feuilles marquées "déduite sans hypothèse" obéïssent aux règles de déduction, et qui est faux, s'il existe un noeud ou une feuille marquées "déduite sans hypothèse" qui n'obéït pas aux règles de déduction. La vérification d'une preuve est rudimentaire, puisque les règles de déduction sont posées comme étant rudimentaires.
L'ajout des opérateurs `"⤚(.)"`, `⤚"(.,.)"`, `⤚"(.,.,.)"`, `⤚"(.,.,.,.)"` au langage logique `L` va engendrer le langage logique étendu que l'on note :
`L["⤚(.)","⤚(.,.)","⤚(.,.,.)","⤚(.,.,.,.)"]`
Par exemple, la proposition étendue `(a,b⤚c)` signifie que `a` et `b` démontre `c` en appliquant exactement une seule fois une règle de déduction. C'est à dire que l'application de la règle de déduction au couples de proposition `(a,b)` va produire la proposition `c`. La proposition étendue `"⤚"a` signifie que `a` se démontre sans hypothèse en appliquant exactement une seule fois une règle de déduction.
Il existe une machine qui énumère toutes les preuves possibles, c'est à dire les arbres de propositions de `L` où les feuilles peuvent être marquées comme étant des hypothèses ou comme étant des propositions déduites sans hypothèse. Nous résumons cela par la phrase « On peut énumérer toutes les preuves ». Et il existe une machine capable de reconnaitre en un temps fini si la preuve est valide ou invalide puisque cette tâche est posée comme rudimentaire. Nous résumons cela par la phrase « On peut énumérer toute les preuves valides ».
La relation binaire de démontrabilité `"⊢"` entre deux propositions, est déterminée mécaniquement par l'ensembles des règles de déduction appelé système de démonstration que nous choisissons arbitrairement. Par exemple si la preuve `(a, (a ⤚ b) ⤚ c) , a ⤚ d` est vérifiée alors nous avons `a|--d`.
À partir d'une proposition servant d'hypothèse, on peut énumérer toutes ses déductions. En effet, le langage logique étendu étant énumérable, on peut énumérer toutes les preuves, ne retenir que celles qui sont valides, et qui ont comme unique hypothèse la proposition en question, et pour chacune d'elle, en prélever sa conclusion. Ainsi on peut énumérer toutes les déductions possibles de la proposition en question. On résume cela en disant que « On peut énumérer toutes les déductions d'une propostion ».
La relation de démontrabilité se définie par son graphe comme un sous-ensemble de `L^2`. Pour les mêmes raisons que précédement le graphe de la relation de démontrabilité `|--` est énumérable.
Nous allons construire petit à petit, et en parallèle, le langage des propositions et les règles de déductions. On ajoute un à un les opérateurs générateurs du langage et une à une les règles de déduction, en s'assurant à chaque fois que ces règles sont toutes nécessaires c'est à dire qu'elles forment une axiomatique.
Une tautologie se définit syntaxiquement ou sémantiquement. Une tautologie syntaxique est une proposition qui se déduit sans hypothèse en appliquant les règles de déduction. Une tautologie sémantique est une proposition vrai dans tous les modèles. Mais par défaut c'est la tautologie syntaxique dont on parlera.
On appelle tautologie une proposition qui peut être démontrée sans hypothèse. Il existe une machine qui énumère toutes les preuves, qui ne retient que celles qui n'on pas d'hypothèse et qui sont valides, et qui en extrait leur conclusion. Et donc, il existe une machine qui énumère toutes les tautologies. L'ensemble des tautologies, qui est inclus dans l'ensemble des propositions, est engendré mécaniquement par le système de démonstration choisi, et constitue donc un ensemble énumérable. On résume cela en disant que « On peut énumérer toutes les tautologies ».
Pour étudier les théories, il faut être en dehors de celles-ci, en dehors de leur propre langage. C'est pourquoi, à l'aide de tous les moyens mathématiques que nous connaissons, on commence par décrire une nouvelle logique naissante, et on s'attache à suivre de manière scrupuleuse toutes les étapes de sa construction.
A ce stade, et si on ne s'occupe pas de la sémantique qui n'intervient pas dans les règles de déduction, même si on utilise un vocabulaire propre à la logique, la matière étudiée n'est pas encore celle de la logique mais plutôt celle des langages. Car il manque des éléments essentiels que sont les valeurs de vérité vrai et faux transcrite en deux propositions canoniques, la tautologie `"⊤"` et l'antilogie `"⊥"`, et surtout il manque la négation, une symétrie qui permet de passer de l'une à l'autre c'est à dire la capacité expressive totale de dire « non ».
Avant que la négation n'existe, avant même l'existence des valeurs de vérité, les preuves existent et sont des constructions. Les règles de déductions existent et sont des règles de construction. Ce qui peut être déduit d'une proposition correspond à ce qui peut être construit à partir de la dite proposition.
Récapitulons nos connaissances : L'ensemble des propositions se note `L`. Le langage étendue introduit les opérateurs de construction de preuve `"⤚(.)"`, `⤚"(.,.)"`, `⤚"(.,.,.)"`, `⤚"(.,.,.,.)"`. La relation binaire de démonstration, se note `"⊢"`. Et cette relation binaire est énumérable.
Nous allons poser certaines exigences sur la relation de démontrabilité qui nous parraissent incontournable, et cela entrainera des contraintes sur les règles de déduction choisies.
On considère que dans un système de démonstration, la relation de démontrabilité doit satisfaire deux propriétés fondamentales que sont la réflexivité et la transitivité, et qui en font ainsi un préordre :
`AA (a,b,c)"∈"L^3,`
`"⊢"` est un préordre `"⊢"` est réflexive `a"⊢"a` `"⊢"` est transitive `a"⊢"b" et " b "⊢"c => a "⊢"c`
La priorité syntaxique des connecteurs est posée de la plus faible à la plus forte comme suit :
`=`, `<=>`, `=>`, `"et"`, `↔`, `|--`
ce qui permet d'omettre un certain nombre de parenthèses sans introduire d'ambiguïté. Le principe de ce choix est de donner une priorité faible à l'égalité afin d'éviter de devoir entourer les termes des équations par des parenthèses, puis de donner une priorité plus forte pour l'inclusion, puis une priorité plus forte pour la conjonction, et une priorité plus forte encore pour les relations étudiées tel que la relation d'équivalence `"↔"` et la relation de démontrabilité `"⊢"`.
Notez que ces deux propriétés sont écrites dans le langage mathématique extérieur à la théorie étudiée, et que seul les variables `a,b,c` désignent des propositions du langage `L`
Si la relation de démontrabilité ne satisfait pas ces deux règles que sont la réflexivité et la transitivité, on parlera alors d'une relation de démontrabilité locale `"⊢"_"local"`, et on construira une relation de démontrabilité qui sera alors qualifiés de globale, à partir de cette relation de démontrabilité locale, simplement en l'enrichissant de ces deux règles.
On remarque alors, que la seconde règle de déduction peut être perçue comme utilisant des propositions du langage `L["⊢(.,.)"]`.
La règle de déduction doit s'appliquer de façon rudimentaire. Et nous avons découvert au chapitre précédent, deux de ces règles. Voyons qu'elles formes ont-elles ? Elles ont une forme d'axiome et nous voulons en faire des règles de construction. La première règle dite de reflexivité nous dit que une proposition quelconque de `L` et capable de démontrer elle-même. Mais il ne faux pas se limiter aux seules proposition de `L`. Cela s'applique également aux extensions de `L` et en particulier à `L["⊢(.,.)","⤚(.)","⤚(.,.)","⤚(.,.,.)","⤚(.,.,.,.)"]`.
Notez bien la distinction entre `(a|--b)` et `(a⤚b)`. L'un dit que `a` démontre `b` à l'aide du système de démonstration choisi, l'autre dit que `a` démontre `b` en appliquant exactement une seule règle de déduction du système de démonstration choisi.
La règle de reflexivité se met sous la forme `a->a` où `a` est une variable muette. La règle est unaire, elle utilise l'algorithme d'unification de termes qui est de complexité linéaire, pour s'appliquer. Elle unifie son entête qui est la variable libre `a` avec une proposition du langage étendu et retourne son corps qui est ce que vaut `a`.
La règle de transitivité se met sous la forme `(a"⊢"b), (b "⊢"c) -> (a "⊢"c)` où `a,b,c` sont des variables muettes. La règle est binaire. Elle unifie son entête qui est `"("(a"⊢"b), (b "⊢"c)")"` avec un couple de propositions du langage étendu. Si l'unification échoue, la règle ne s'applique pas. Si l'unification réussit, la règle retourne son corps qui est l'expression `(a "⊢"c)` dans laquelle `a` et `c` sont remplacés par ce qu'ils vaux.
--- 12 juin 2021 ---
Des règles supplémentaires apparaîssent nécessaires pour éliminer les opérateurs `⤚` qui sont :
`("⤚"a) -> a`
`(a"⤚"b) -> (a"⊢"b)`
`(a,b"⤚"c),(a"⤚"b) -> (a"⊢"c)`
...
------
Rappelons qu'un ordre est par défaut partiel, et de même, un préordre est par défaut partiel. À partir du préordre `"⊢"` on définie son symétrisé `"↔"` qui constitue une relation d'équivalence :
`a"↔"b <=> a "⊢"b" et "b"⊢"a` `a"↮"b <=> a "⊬"b" ou "b"⊬"a`
Considérons une proposition quelconque `a`. L'ensemble des propositions équivalentes à `a` se note `[a]`. L'ensemble des propositions déductibles de `a` se note `"<"a">"`. Et l'ensemble des propositions déduisant `a` se note `"<"a">"^("-"1)` car correspondant à la relation de déduction inverse, appelée relation d'induction. C'est l'ensemble des propositions induites par `a`.
On divise l'ensemble `L` par la relation d'équivalence `"↔"` pour produire la structure `L"/↔"` regroupant l'ensemble des classes d'équivalences :
Notez que l'on réserve l'usage des braquettes `{}` uniquement pour regrouper des éléments distincts, ce qui explique ici le choix de la notation utilisant l'itérateur d'union. On peut également utiliser la notation de sac :
Dans cette structure `L"/↔"`, le préordre `"⊢"` induit un ordre désigné par le même symbole :
dans `L"/↔"``"⊢"` est réflexive `[a]"⊢"[a]` `"⊢"` est antisymétrique `[a]"⊢"[b]" et "[b]"⊢"[a] => ([a]"="[b])` `"⊢"` est transitive `[a]"⊢"[b]" et "[b]"⊢"[c] => [a]"⊢"[c]`
Remarquez qu'un préordre inversé est encore un préordre et donc que la relation inverse, appelée relation d'induction, `⊣`, est encore une relation de pré-ordre, et que ces deux relations de pré-ordre `"⊢", "⊣"` induisent la même relation d'équivalence `"↔"`, et ont les mêmes classes d'équivalences, et induisent un même ordre mais inversé dans la structure `ccL"/↔"`.
A ce stade qualifié de prélogique où la négation n'est pas encore définie, on peut quand-même définir les antilogies et les tautologies, et donc d'une certaine manière le faux et le vrai à équivalence près.
Une proposition qui n'est ni une tautologie ni une antilogie est appellé un indécidable. L'ensemble des propositions `L` se partitionne en trois parties :
antilogie
pour `"⊢"`
tautologie
pour `"⊢"`
indécidable
pour `"⊢"`
On utilise aussi les adjectifs correspondant, une proposition antilogique est une antilogie, une proposition tautologique est une tautologie, une proposition indécidable est un indécidable.
On peut toujours ajouter, dans le langage des propostitions, deux propositions atomiques, le vrai `"⟙"`, et le faux `"⟘"`, en ajoutant les deux contraintes suivantes sur la relation de déduction.
Et on remarquera que si la relation de déduction n'est pas définie récurcivement par des propriétés globales sur elle-même, alors ces deux contraintes n'ont aucune influence sur la relation de déduction restreinte en enlevant ces deux propositions. Il s'agit alors juste d'une commodité d'écriture, pour désigner facilement la classe des tautologies `["⟙"]`, et la classe des antilogies `["⟘"]`.
Un moyen mémothechnique : L'antilogie démontre tout, donc est placée avant tout le monde dans l'ordre de déduction, donc constitue un minimum total représenté par le symbole du bas `"⟘"`. Tandis que la tautologie est démontrer par tout le monde, donc est placée après tous le monde dans l'ordre de déduction, donc constitue un maximum total représenté par le symbole du haut `"⟙"` qui est également similaire à la lettre T de Tautologie.
L'ensemble des propositions se note `"<"⟘">"= L"` puisque qu'elles sont toutes démontrées par l'antilogie, et l'ensemble des propositions démontrables sans hypothèse se note `"<"⟙">"`, et est appelé l'ensemble des tautologies. Et nous avons bien évidemment `⟘⊢⟙`. Ces deux ensembles sont énumérables puisque la relation `"⊢"` est énumérable.
On définie la notion de cohérence et d'incohérence comme suit :
Le système de démonstration est cohérent `⟙⊬⟘` Le système de démonstration est incohérent `⟙⊢⟘`
Et dans un système incohérent, toute les propositions sont équivalentes.
On constate que le complémentaire des tautologies comprend les antilogies, et que le complémentaires des antilogies comprend les tautologies :
Donc à l'aide de ces deux propostions `⟙, ⟘` et d'une proposition quelconque `a`, on caractérise 6 sous-ensembles de propositions possibles :
`a` démontrable `a` tautologique `a` absurde `a` antilogique `a` décidable `a` tautologique ou antilogique `a` indémontrable `a` antilogie ou indécidable `a` cohérent `a` tautologie ou indécidable `a` indécidable `a` indécidable
Et si nous avons une proposition `a` qui démontre une proposition `b` alors nous avons ces suites ordonnées :
`"<"⟘">"^("-"1) sube "<"a">"^("-"1) sube "<"b">"^("-"1) sube "<"⟙">"^("-"1)`
De la même façon que l'on a défini l'antilogie et la tautologie, on peut définir la relation de déduction par une propriété globale sur la relation de déduction, conséquence de sa reflexivité et de sa transitivité, comme suit : `a` déduit `b` si et seulement si toutes les déductions de `b` sont des déductions de `a`. Et par symétrie temporelle, nous avons de même : `a` déduit `b` si et seulement si toutes les inductions de `a` sont des inductions de `b` :
Etant donné un ensemble de propositions `E` inclus dans `L`, nous dirons que `a` déduit dans `E` la proposition `b` , ce qui se note `a"⊢"_Eb`, si et seulement si la règle précédente ne s'applique que pour les propositions appartenant à `E`.
On définit ainsi `"⊢"_E`, la relation de déduction restreinte à un sous-ensemble de propositions `E sube L`. comme suit : La proposition `a` déduit dans `E` la proposition `b` si et seulement si toutes les déductions de `b` appartenant à `E` sont des déductions de `a`. Et par symétrie temporelle, nous avons de même : La proposition `a` déduit dans `E` la proposition `b` si et seulement si toutes les inductions dans `E` de `a` sont des inductions de `b` :
`a"⊢"_E b` |
`("<"b">"nnE)⊆"<"a">"`
|
`AAx"∈" E, b"⊢"x => a "⊢"x` |
`("<"a">"^("-"1)nnE) ⊆"<"b">"^("-"1)` |
`AAx"∈" E, x"⊢"a => x"⊢"b` |
`a"⊬"_E b` |
`("<"b">"nnE)⊈"<"a">"` |
`EEx"∈"E, b"⊢"x" et "a "⊬"x` |
`("<"a">"^("-"1)nnE) ⊈"<"b">"^("-"1)` |
`EEx"∈" E, x "⊢"a" et "x"⊬"b` |
Le sous-ensemble de propositions `E` se partitionne en trois parties :
`E`-tautologie
pour `"⊢"_E`
`E`-antilogie
pour `"⊢"_E`
`E`-indécidable
pour `"⊢"_E`
On remarque qu'une tautologie dans `L` est une tautologie dans toutes les restrictions de `L`, parcontre l'inverse n'est pas vrai. De même on remarque qu'une antilogie dans `L` est une antilogie dans toutes les restrictions de `L`, parcontre l'inverse n'est pas vrai.
L'inverse d'une restriction et une extension. En regardant ce qu'est une restriction on révèle d'une certaine façon ce qu'est une extension.
On commence par le langage propositionnel le plus rudimentaire ne contenant que des propositions atomiques. Soit `A` un ensemble fini d'atomes. Nous avons par exemple `A"="{a,b,c,d,e,f}`. Et on considère qu'il existe déjà une relation quelconque définit sur `A`, dite relation de déduction locale `"⊢"_"local"`. L'ensemble des propositions est l'ensemble des atomes auquel on ajoute l'antilogie `"⟘"` et la tautologie `"⟙"`, et on complète la relation locale afin que `AA x "∈" L, "⟘⊢"x "et" x"⊢⟙"`
`L=Auu{⟙, ⟘}`
Notez que rien n'est préciser concernant la sémantique de ces propositions atomiques, c'est à dire leur signification, les mondes qu'elles décrivent. En particulier, ces propositions atomiques ne doivent pas être considérées comme des variables booléennes.
On définit une relation de déduction `"⊢"` à partir de la relation `"⊢"_"local"` en ajoutant les propriétés de reflexivité et de transitivité.
Délors, le langage des démonstrations, que l'on note `D`, va pouvoir se définir à partir de cette relation de déduction locale et des deux règles globales imposées que sont la reflexivité et la transitivité. Une démonstration est une suite de propositions de `L` telle que chaque proposition déduit localement son successeur, et où l'hypothèse est la première proposition, et où la conclusion est la derniere proposition.
`D = {(a_i)_(i in{0,1,2...,n}) "/" EEn"∈"NN, AA i "∈"{0,1,2,...,n}, a_i "∈" A "et" (i"<"n=>a_i "⊢"_"local"a_(i+1))}`
L'algorithme de recherche d'une démonstration de `b` à partir de `a` correspond à l'algorithme de recherche d'un chemin de `a` vers `b` dans le graphe `"⊢"_"local"`.
Nous voulons maintenant introduire des connecteurs logiques sans introduire la négation, cela se peut en introduisant les connecteurs `"∧", "∨","⇔"`.
On introduit la conjonction en prélogique comme suit : On ajoute le connecteur binaire de conjonction `"∧"` au langage des propositions. `L` devient l'ensemble des compositions closes d'atomes appartenant à `A` et du connecteur de conjonction `"∧"` , ce qui se note comme suit :
`L = "<" A, "∧>"`
Deux cas sont alors à étudier. Un premier cas simple où la règle de déduction est atomique et provient d'une relation de déduction locale quelconque définie sur `A`. C'est à dire tel que le pouvoir de déduction d'un atome n'est pas changé par la conjonction d'autres atomes. On parlera de conjonction atomique. Et le second cas, qui est le cas général où la règle de déduction provient d'une relation de déduction locale quelconque définie sur `L`. Cela changera l'algorithme de recherche, mais cela ne changera pas le langage des démonstrations.
La conjonction par définition obéit à la règle suivante : Etant donné trois propositions quelconques `P,Q,R` appartenant à `L`, La proposition `P` déduit la proposition `Q"∧"R` si et seulement si `P` déduit `Q` et `P` déduit `R`. Ce qui s'écrit comme suit :
`AA(P,Q,R)"∈"L^3, P"⊢"(Q"∧"R) <=> (P"⊢"Q "et" P"⊢"R)`
Cette règle d'équivalence se traduit en trois règles d'implication :
Ce qui s'écrit comme suit :
`AA(P,Q,R)"∈"L^3,`
`(P"⊢"Q "et" P"⊢"R) => P"⊢"(Q"∧"R)` règle `r_1`
`P"⊢"(Q"∧"R)=>(P"⊢"Q)` règle `r_2`
`P"⊢"(Q"∧"R)=>(P"⊢"R)` règle `r_3`
Notez que le connecteur `"et"` fait parti du méta-langage tandis que le connecteur `"∧"` fait partie du langage des propositions.
Ces trois règles d'implication suffisent pour définir complètement la conjonction et le système de démonstration qui va avec. Cela correspond dans la déduction naturelle à la règle d'introduction de la conjontion `"∧"` et au deux règles d'élimination de la conjonction `"∧"`.
Consiérons l'exemple atomique suivant où `a"⊢"_"local"b` et `c"⊢"_"local"d`. On veut écrire une démonstration de `((a"∧"e)"∧"c)⊢((d"∧"b)"∧"e)` :
L'hypothèse est :
`((a"∧"e)"∧"c)`
En appliquant la réflexivité à partir de l'hypothèse on obient :
`((a"∧"e)"∧"c) "⊢" ((a"∧"e)"∧"c)`
En appliquant la règle n°3 à `((a"∧"e)"∧"c) "⊢" ((a"∧"e)"∧"c)` on obtient :
`((a"∧"e)"∧"c) "⊢" c`
En appliquant la transitivité à `(a"∧"e)"∧"c) "⊢" c` et `c"⊢"_"local"d` on obtient :
`((a"∧"e)"∧"c) "⊢" d`
En appliquant la règle n°2 à `((a"∧"e)"∧"c) "⊢" ((a"∧"e)"∧"c)` on obtient :
`((a"∧"e)"∧"c) "⊢" (a"∧"e)`
En appliquant la règle n°2 à `(a"∧"e)"∧"c) "⊢" (a"∧"e)` on obtient :
`((a"∧"e)"∧"c) "⊢" a`
En appliquant la transitivité à `(a"∧"e)"∧"c) "⊢" a` et `a"⊢"_"local"b` on obtient :
`((a"∧"e)"∧"c) "⊢" b`
En appliquant la règle n°1 à `(a"∧"e)"∧"c) "⊢" d` et `(a"∧"e)"∧"c) "⊢" b` on obtient :
`((a"∧"e)"∧"c) "⊢" (d"∧"b)`
En appliquant la règle n°3 à `(a"∧"e)"∧"c) "⊢" (a"∧"e)` on obtient :
`((a"∧"e)"∧"c) "⊢" e`
En appliquant la règle n°1 à `((a"∧"e)"∧"c) "⊢" (d"∧"b)` et `((a"∧"e)"∧"c) "⊢" e` on obtient :
`((a"∧"e)"∧"c) "⊢" ((d"∧"b)"∧"e)`
En appliquant le modus ponens à `((a"∧"e)"∧"c)` et `((a"∧"e)"∧"c) "⊢" ((d"∧"b)"∧"e)` on obtient la conclusion :
`((d"∧"b)"∧"e)`
La réflexivité semble n'être utilisée qu'en première opération sur l'hypothèse pour produire un lien de déduction. Et le modus ponens semble n'être utilisée qu'en dernière opération sur l'hypothèse et un lien de déduction pour produire la conclusion.
Puis, chaque étape du raisonnement correspond à l'application d'une règle sur un ou deux liens de déduction préalablement démontrés et produisant un lien de déduction démontré. Les règles sont `{t"(.,.)", r_1"(.,.)", r_2"(.)", r_3"(.)"}` avec les définitions suivantes utilisant des variables universelles `A,B,C` appartenant à `L`, et pouvant ainsi s'appliquer par unification :
`t(A"⊢"B,B"⊢"C) = A"⊢"C`
`r_1(A"⊢"B, A"⊢"C) = A"⊢"(B"∧"C)`
`r_2(A"⊢"(B"∧"C)) = A"⊢"B`
`r_3(A"⊢"(B"∧"C)) = A"⊢"C`
La démonstration se met alors sous forme d'un arbre où chaque noeuds est une règle qui produit un lien de déduction et les fils sont des liens de déduction produits par ces noeuds ou apportés par les feuilles. Et les feuilles sont des liens de production propres au système de démonstration ou sont le lien de déduction réflexif de l'hypothèse.
Le connecteur de conjonction est associatif et commutatif de telle sorte qu'une proposition de `L` correspond à un sous-ensemble de `A` désignant la conjonction de ses éléments.
`L = ccP(A)`
Dés lors, le problème se simplifie considérablement. Etant donné une hypothèse représenté par un sous-ensemble `X` sube `A`, On calcul l'ensemble `Y` des atomes atteingnable en partant de `X` et en empruntant les arcs de la relation `"⊢"_"local"` un nombre fini de fois.
`Y = X uu "⊢"_"local"(X) uu "⊢"_"local"^2(X) uu "⊢"_"local"^3(X) uu ....`
L'ensemble des déductions de `X` est :
`"<"X">" = ccP(Y)`
Dans le cas générale, il faut considérer une relation de déduction locale définie de `ccP(A)` sur `A`. On calcul l'ensemble `Y` des atomes atteingnable en partant de `X` et `ccP(X)` et en empruntant les arcs de la relation `"⊢"_"local"` un nombre fini de fois.
`Y_0=X`
`Y_1={x "/" EE E sube Y_0, E "⊢"_"local"x}`
`Y_2={x "/" EE E sube Y_0uuY_1"/" E nn Y_1 ≠ Ø, E "⊢"_"local"x}`
`Y_3={x "/" EE E sube Y_0uuY_1uuY_2"/"E nn Y_2≠ Ø, E "⊢"_"local"x}`
....`Y = Y_0 uu Y_1 uu Y_2 uu Y_3 uu ....`
L'ensemble des déductions de `X` est :
`"<"X">" = ccP(Y)`
On introduit la disjonction en prélogique comme suit : On ajoute le connecteur binaire de disjonction `"∨"` au langage des propositions. `L` devient l'ensemble des compositions closes d'atomes appartenant à `A` et des connecteurs de conjonction `"∧"` et de disjonction `"∨"`, ce qui se note comme suit :
`L = "<" A, "∧", "∨>"`
La disjonction par définition obéit aux règles suivantes :
Etant donné 6 propositions quelconques `P,Q,R,A,B,C` appartenant à `L`.
Si `P` déduit `A"∨"B` et si `Q"∧"A` déduit `C` et si `R"∧"B` déduit `C`, alors `P"∧"Q"∧"R` déduit`C`.
Si `P` déduit `Q` alors `P` déduit `Q"∨"R`
Si `P` déduit `Q` alors `P` déduit `R"∨"Q`
---- 2 janvier 2020 ----