La logique formelle

 

1) Introduction

Qu'est-ce qu'une théorie 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 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 du langage formel.

1.1) Qu'est-ce qu'une théorie ?

Une théorie est une proposition et réciproquement une proposition est une théorie. Ce sont deux mots synonymes. Une théorie est écrite dans un langage d'alphabet fini appelé langage des propositions et doit être de taille finie.

On suppose que le langage des propositions utilise un alphabet fini, et on suppose qu'il existe un programme d'arrêt sûr capable de décider si une chaine de caractères constitue une proposition correctement écrite, c'est à dire dont la syntaxe obéït au langage des propositions.

Délors, l'ensemble des propositions possibles est énumérable. Il existe un programme qui énumère toutes les propositions possibles. Nous résumons cela par la phrase « On peut énumérer toute les propositions  ».

1.2) Qu'est-ce qu'une démonstration ?

C'est un objet plus riche qu'une proposition, et qui contient des propositions. Elle est écrite dans un langage plus riche que le langage des propositions, et que nous appellons langage des démonstrations. Et nous dirons qu'elle est engendrée par le système de démonstration.

On suppose que le langage des démonstrations utilise un alphabet fini, et on suppose qu'il existe un programme d'arrêt sûr capable de décider si une chaine de caractères constitue une démonstration correctement écrite, c'est à dire dont la syntaxe obéït au langage des démonstrations, ou dit autrement, qui est bien engendrée par le système de démonstration. En effet, une démonstration est une preuve et donc doit être de taille finie, et doit être vérifiable mécaniquement par un programme dont l'arrêt est sûr, et elle doit comporter une proposition de départ appelée hypothèse, et une proposition de fin appelée conclusion.

Délors, l'ensemble des démonstrations possibles est énumérable. Il existe un programme qui énumère toutes les démonstrations possibles. Nous résumons cela par la phrase « On peut énumérer toutes les démonstrations ».

Pour étudier les théories, il faut être en dehors de celles-ci, en dehors de leur langage propre. Pour cela on utilise un autre langage que celui des théories étudiées et de leur système de démonstration, un langage mathématique non contraint appelé meta-langage. Ainsi y a-t-il trois niveaux de langage, le langage des propositions inclus dans le langage des démonstrations et le langage mathématique qui les décrit appelé méta-langage.

Le symbole de départ que nous utiliserons, et qui constitura un méta-connecteur, est la relation binaire de déduction `"⊢"` entre deux propositions. Cette relation est déterminée mécaniquement par le système de démonstration choisi.

À partir d'une proposition servant d'hypothèse, on peut énumérer toutes ses déductions. Le langage des démonstrations étant énumérables, on énumére toutes les démonstrations. On ne retient que celles qui ont comme hypothèse la proposition en question. Et pour chacune d'elle on prélève sa conclusion. On énumère ainsi 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 ».

Par contre, le paradoxe de Godel-Turing démontre que dans le cas général on ne peut pas énumérer le complémentaire, c'est à dire les propositions qui ne peuvent pas être déduites. Ainsi la relation binaire de déduction `"⊢"` constitue un demi-prédicat, qui donne une demi-réponse. Le calcul de `P"⊢"Q` répond oui en un temps fini si Q se déduit de P. Mais ne donne jamais de réponse si Q ne se deduit pas de P, et il faut donc se placer à la fin des temps pour être sûr qu'il s'agit d'une non réponse et que cela correspond donc bien à une réponse négative.

Nous allons construire petit à petit, et en parallèle, le langage des propositions et le langage des démonstrations, dévoilant ainsi le système de démonstration, en ajoutant un à un les composants du langage des propositions et une à une les règles de construction des propositions, en ajoutant un à un les composants du langage des démonstrations et une à une les règles de construction des démonstrations, en s'assurant à chaque fois que ces règles sont toutes nécessaires c'est à dire qu'elles forment une axiomatique, et qu'elles sont suffisantes pour une sémantique que nous pourrons ainsi définir, c'est à dire qu'elles démontrent toutes les propositions validées par la sémantique.

1.3) Qu'est-ce qu'une tautologie ?

On appelle tautologie une proposition qui peut être démontrée sans hypothèse. Il existe une machine qui énumère toutes les démonstrations. Et l'absence d'hypothèse correspond à l'hypothèse tautologique, que nous représentons par le symbole `"⊤"`. Cela représente donc la proposition vide, ce qu'il reste d'une proposition lorsque l'on a tout enlevé, l'hypothèse présente avant toute hypothèse possible. Il existe alors une machine qui énumère toutes les tautologies. Le langage des tautologies, inclus dans le langage des propositions, est ainsi engendré mécaniquement par le système de démonstration et constitue également un ensemble énumérable. On résume cela en disant que « On peut énumérer toutes les tautologies ».

L'élémentarisme se fonde à partir du fait essentiel que quelque soit le langage des propositions choisi et quelque soit le langage des démonstrations choisi, du moment qu'ils sont tous deux énumérables, l'ensemble des tautologies est énumérable. Et qu'il doit donc y avoir une sémantique dénombrable rendant superfétatoires les sémantiques non dénombrables et les infinis autres que l'infini potentiel noté aleph, `aleph`.

2) Prélogique

A ce stade, 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, la tautologie `"⊤"` et l'antilogie `"⊥"`, et surtout il manque ce qu'est 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 démonstrations existent et sont des objets plus généraux appelés des constructions. Ce qui peut être déduit d'une proposition correspond à ce qui peut être construit à partir de la dite proposition par le même procédé, c'est à dire en construisant une démonstration ayant la proposition comme hypothèse et en ne retenant que sa conclusion.

Récapitulons nos connaissances : L'ensemble des propositions se note `L`. La proposition tautologique se note `"⊤"`. Donc `"⊤" "∈" L`. La relation binaire de déduction se note `"⊢"`. Nous avons donc `"⊢" "∈" ccP(L^2)`. Cette relation binaire est énumérable, c'est à dire qu'il existe une bijection totalement calculable `f` de `NN->"⊢"`

2.1) La relation de déduction est un préordre

On considère que dans un système de démonstration, la relation de déduction doit satisfaire deux règles que sont la réflexivité et la transitivité :

 `"⊢"` est un préordre      `"⊢"` est réflexive      `AA a"∈"L, a"⊢"a`
 `"⊢"` est transitive   `AA (a,b,c)"∈"L^3, a"⊢"b" et " b "⊢"c => a "⊢"c` 

Notez que la priorité syntaxique des connecteurs est ordonnée comme suit, de la plus faible à la plus forte, `=`, `<=>`, `=>`, `"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éduction `"⊢"`.

Si la relation de déduction ne satisfait pas ces deux règles que sont la réflexivité et la transitivité, on parlera alors d'une relation de déduction locale `"⊢"_"local"`, et on construira une relation de déduction globale à partir de cette relation de déduction locale en l'enrichissant de ces deux règles.

Ces deux règles exigées, que sont la reflexivité et la transitivité, font que la relation de déduction est un pré-ordre.

2.2) Classe d'équivalence et relation d'ordre

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`.

 `"<"a">" = {x"∈" L "/" a"⊢"x}` 

 `"<"a">"^("-"1) = {x"∈" L "/" x"⊢"a}` 

 `[a]= {x"∈" L "/" a"⊢"x" et "x"⊢"a} = "<"a">" nn "<"a">"^("-"1)` 

On divise l'ensemble `L` par la relation d'équivalence `"↔"` pour produire la structure `L"/↔"` regroupant l'ensemble des classes d'équivalences :

 `L"/↔" = uuu_(a in L){[a]}` 

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 :

 `L"/↔" = "⟅" [a] "/"EEa "∈" L "⟆"` 

Dans cette structure `L"/↔"`, le préordre `"⊢"` induit un ordre désigné par le même symbole :

 `"⊢"` est un ordre
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"/↔"`.

2.3) Définition des antilogies et tautologies

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 :

`a` est une
antilogie
`a` est un minimum total
pour `"⊢"`
`AA x "∈" L, a"⊢"x`
`a` est une
tautologie
`a` est un maximum total
pour `"⊢"`
`AA x "∈" L, x"⊢"a`
`a` est un
indécidable
`a` n'est pas un bout total
pour `"⊢"`
 `(EE x "∈" L, x"⊬"a)" et "(EE x "∈" L, a"⊬"x)` 

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.

 `AA x "∈" L, ⟙"⊢"x` 
 `AA x "∈" L, ⟘"⊢"a` 

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 :

 `["⟘"] sube "∁"["⟙"]` 
 `["⟙"] sube "∁"["⟘"]` 

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`
 `a` tautologique
`a"∈"["⟙"]`
 `a` absurde
`a"⊢"⟘`
 `a` antilogique
`a"∈"["⟘"]`
 `a` décidable
 `⟙"⊢"a" ou "a"⊢"⟘` 
 `a` tautologique ou antilogique 
`a"∈"(["⟙"]uu["⟘"])`
 `a` indémontrable 
`⟙"⊬"a`
 `a` antilogie ou indécidable
`a"∈∁"["⟙"]`
 `a` cohérent
`a"⊬"⟘`
 `a` tautologie ou indécidable
`a"∈∁"["⟘"]`
 `a` indécidable
 `⟙"⊬"a" et "a"⊬"⟘` 
 `a` indécidable
 `a"∈"("∁"["⟙"]uu"∁"["⟘"])` 

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)` 
`⟘⊢a⊢b⊢⟙`
`⟙⊣b⊣a⊣⟘`
`"<"⟙">" sube "<"b">" sube "<"a">" sube "<"⟘">"`

2.4) Les restrictions du système de démonstration

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` :

`a"⊢"b`
`"<"b">⊆<"a">"`
`AAx"∈" L, b"⊢"x => a "⊢"x`
`"<"a">"^("-"1) "⊆<"b">"^("-"1)`
 `AAx"∈" L, x"⊢"a => x"⊢"b`
`a"⊬"b` 
`"<"b">⊈<"a">"`
`EEx"∈" L, b"⊢"x" et "a "⊬"x`
`"<"a">"^("-"1) "⊈<"b">"^("-"1)`
`EEx"∈" L, x "⊢"a" et "x"⊬"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 :

`a` est une 
`E`
-tautologie
`a` est un minimum total
pour `"⊢"_E`
`AA x "∈" E, x"⊢"a`
`a` est une 
`E`
-antilogie
`a` est un maximum total
pour `"⊢"_E`
`AA x "∈" E, a"⊢"x`
`a` est un 
`E`
-indécidable
`a` n'est pas un bout total
pour `"⊢"_E`
`(EE x"∈" E, x"⊬"a)" et "(EE x"∈"E, a"⊬"x)`

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.

2.5) Introduction des propositions atomiques

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 `"∧", "∨","⇔"`.

2.6) Introduction de la conjonction `"∧"`

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 :

  1. Si `P` déduit `Q`, et si `P` déduit `R`, alors `P` déduit la proposition `Q"∧"R`.
  2. Si `P` déduit `Q"∧"R` alors `P` déduit `Q`
  3. Si `P` déduit `Q"∧"R` alors `P` déduit `R`.

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)`

2.6) Introduction de la disjonction `"∨"`

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 ----

 

 


Dominique Mabboux-Stromberg