On se propose de construire petit à petit les règles de raisonnement nécessaires pour construire une mathématique, en procédant empiriquement, par tâtonnement succeccif, où l'axiomatique en construction va garantir la totale mécanicité du raisonnement. On reprend donc la discussion sur la génèse mais d'un point de vue beaucoup moins prétentieux, un point de vue juste pratique et empirique. On utilise pour cela des structures qui ne sont pas du premier ordre mais qui restent constructives où tous les éléments sont énumérés par des programmes informatiques.
On développe un programme qui explore toutes les constructions possibles de démonstration. On ajoute un à un les connecteurs du langage, et un à un les axiomes auxquel ils doivent se conformer. On décrit le langage utilisé par les axiomes, par les règles de déduction, et par les programmes informatiques auxquelles elles correspondent et qui transforment les prémisses en conclusions. On construit une sémantique interne qui permet de donner un sens au formule et on vérifie que la vérité syntaxique coïncide avec la vérité sémantique.
On crée l'élément `1` qui désignera la valeur logique vrai. Puis on crée l'élément `0` qui désignera la valeur logique faux. Puis on crée le connecteur unaire `"¬(.)"`, et les connecteurs binaires `"∧(.,.)", "∨(.,.)", "⇒(.,.)", "⇔(.,.)", "+(.,.)"` de syntaxe centrée. Le langage des propositions `sfL` est l'ensemble des compositions closes finies de ces connecteurs, appelées termes. On définit le langage `sfL` comme une clôture par compositions closes finies de connecteurs, que l'on présente entouré de crochet :
`sfL = "<"1,0,"¬(.)", "∧(.,.)", "∨(.,.)", "⇒(.,.)", "⇔(.,.)", "+(.,.)>"`
Les connecteurs `"¬", "∧", "∨","⇒","⇔","+"` sont appellés les connecteur générateurs du langage `sfL` car faisant partie de sa présentation. Par ailleurs, ces connecteurs sont libres parce que non-préalablement-définis, ou plus précisement parce que leur définition sont :
`1 = (|->1)`
`0 = (|->0)`
`"¬" = (x|-> "¬"x)`
`"∧" = ((x,y)|-> x"∧"y)`
`"∨" = ((x,y)|-> x"∨"y)`
`"⇒" = ((x,y)|-> x"⇒"y)`
`"⇔" = ((x,y)|-> x"⇔"y)`
`"+" = ((x,y)|-> x"+"y)`
Où le symbole fonctionnelle `"↦"` joue le rôle d'un connecteur soit unaire ou binaire ou ternaire, de construction de termes. Ainsi les connecteurs `1`, `0`, `"¬"`, `"∧"`, `"∨"`, `"⇒"`, `"⇔"`, `"+"` jouent deux rôles, un rôle passif de composant d'un terme et un rôle actif de fabrication de terme. Remarquez comment on a augmenté le langage formelle pour exprimer cela :
Puis
Le langage des propositions `sfL` est aussi définissable par une grammaire. C'est le langage engendré par la grammaire suivante :
`sfL"→"{1,0,"¬"sfL, (sfL"∧"sfL), (sfL"∨"sfL), (sfL"⇒"sfL), (sfL"⇔"sfL), (sfL"+"sfL)}`
On ajoute au langage des termes le symbole `sfL` comme connecteur nullaire. Délors apparait deux sortes de terme, les termes dit terminaux ne comprenant pas de symbole `sfL`, et les termes dit non-terminaux comprenant des symboles `sfL`. Ainsi, le symbole `sfL` joue deux rôles, c'est l'ensemble de tout les termes terminaux du langage, et c'est aussi un connecteur nullaire non-terminal et qui d'après la grammaire peut être remplacé par l'un des termes présents dans l'ensemble à droite du symbole `"→"`. Le langage des termes est élargi en ajoutant des connecteurs nullaires non-terminaux, et après cela, chaque terme joue deux rôles. Par exemple, le terme `(sfL"∧"sfL)` désigne l'ensemble des compositions qu'il est possible de faire à l'aide du connecteur binaire `"∧"` et de deux termes terminaux quelconques de `sfL`, et il désigne aussi un terme non-terminal. Nous avons :
`sfL = {1}"∪"{0}"∪"{¬sfL}"∪"(sfL"∧"sfL)"∪"(sfL"∨"sfL)"∪"(sfL"⇒"sfL)"∪"(sfL"⇔"sfL)"∪"(sfL"+"sfL)`
Remarquez comment on a augmenté le langage formelle pour exprimer cela :
Puis
On ajoute un troisième rôle au symbole `sfL`, celui de représenter l'ensemble des termes (terminaux et non-terminaux). Et c'est le contexte qui déterminera quel rôe est joué.
Le langage des termes terminaux est `sfL`. Le langage des termes (non-terminaux ou terminaux) s'obtient par extension élémentaire en ajoutant le connecteur nullaire non-terminal qui porte le nom du langage `sfL`. Cette extension se note `sfL[sfL]`. chaque terme de `sfL[sfL]` possède un deuxième rôle qui est sa sémantique et qui correspond à un ensemble (l'ensemble des termes terminaux).
Par exemple, le terme `(sfL"∧"sfL)` possède comme sémantique l'ensemble des compositions d'un connecteur binaire `"∧"` avec deux termes terminaux quelconques de `sfL`. Et le terme terminal `(0"∧"1)` possède comme sémantique l'ensemble singleton contenant `(0"∧"1)`.
On crée `n` nouveaux éléments `a,b,c,...` qui désigneront des valeurs logiques inconnues. On les ajoute dans le langage sous forme d'une extension élémentaire :
`sfL = "<"a,b,c,1,0,"¬(.)", "∧(.,.)", "∨(.,.)", "⇒(.,.)", "⇔(.,.)", "+(.,.)>"`
`sfL"→"{a,b,c,1,0,"¬"sfL, (sfL"∧"sfL), (sfL"∨"sfL), (sfL"⇒"sfL), (sfL"⇔"sfL), (sfL"+"sfL)}}`
On peut les regrouper dans un ensemble `sfC`. On permet d'ajouter dans l'énumération entre crochet `"<"...">"` des ensembles qui seront remplacés par leur contenu :
`sfL = "<"sfC,1,0,"¬(.)", "∧(.,.)", "∨(.,.)", "⇒(.,.)", "⇔(.,.)", "+(.,.)>"`
`sfC = {a,b,c}``sfL"→"{sfC,1,0,"¬"sfL, (sfL"∧"sfL), (sfL"∨"sfL), (sfL"⇒"sfL), (sfL"⇔"sfL), (sfL"+"sfL)}}`
`sfC"→"{a,b,c}`
Afin de limiter l'usage des parenthèses, on munie les connecteurs d'une priorité syntaxique de la plus élevée à la plus faible comme suit :
Et on adopte un sens syntaxique de composition de mêmes opérateurs binaires de gauche à droite. Ainsi, nous avons :
`"¬"a"⇒"b` signifie `("¬"a)"⇒"b`
`a "∨" b "∧" c "∨" a` signifie `(a "∨" b) "∧" (c "∨" a)`
`a "∧" b "⇒" c "⇔" a` signifie `((a "∧" b)"⇒"c)"⇔" a`
`a"⇒"b"⇒"c"⇒"a` signifie `a"⇒"(b"⇒"(c"⇒"a)) `
`a,b,c` sont appellés les propositions génératrices du langage car faisant partie de sa présentation, et `"¬", "∧", "∨","⇒","⇔","+"` sont appellés les connecteur générateurs du langage car faisant partie de sa présentation.
Une démonstration directe est un arbre de preuve où chaque noeud applique une règle de déduction syntaxique sur des prémisses apportées par ses fils et transmet la conclusion à son noeud parent. La démonstration est directe car elle n'introduit à aucun moment des hypothèses. La règle de déduction est dite syntaxique car elle n'opère qu'une transformation mécanique déterminée sur l'expression des prémisses pour produire l'expression d'une conclusion.
On remarque que pour chaque noeud de l'arbre de preuve, ses fils peuvent être regroupés en un ensemble de prémisses correspondant à leur conjonction. Et la conclusion pourra également s'étendre en un ensemble de conclusions sous forme de conjonction ou être simplement partagé entre plusieurs noeuds parents. Délors, l'arbre de preuve devient un graphe de preuve orienté sans cycle où les règles de déduction sont des programmes qui appliqués à un ensemble d'expressions de prémisses `P`, produisent un ensemble d'expressions de conclusions `C`.
Les règles de déduction sont écrites dans un second langage qui est un langage de programmation. L'approche empirique va contester la distinction de nature entre les règles de déduction et les propositions, affirmant qu'une règle de déduction doit pouvoir être considérée comme une proposition. L'approche empirique va ainsi agrandire le langage des propositions pour y inclure le langage des règles de déduction. Et cela se fera en fusionnant certain de ses opérateurs. Apparaîtront alors d'autre règles de déduction s'appliquant aux règles de déduction, exprimées dans un troisième langage de programmation. Et ce processus va se répéter. Car à chaque fois que l'on agrandit le langage des propositons pour y incorporer les règles de déduction, apparaissent de nouvelles règles de déduction exprimée dans un nouveau langage de programmation.
Une déduction est une production faite par un programme informatique. Cette conception ouvre le paradigme programmatif où les axiomes sont des règles de production et sont regroupées avec les propositions admises dans un ensemble appelé l'ensemble des propositions connues ou publiées. Puis cet ensemble va s'agrandire en fonction du temps traduisant une effectivité consommée en appliquant les règles de production qu'il contient selon un ordre canonique propre aux langages, et exhaustifs c'est-à-dire de telle sorte que toute proposition produisable se produise en un temps fini. Cette dernière condition sera garantie par une implémentation spécifique du raisonnement. Délors, toute théorie est un programme qui énumères toutes ses déductions.
Le raisonnement est dit hypothético-décuctif lorsqu'il est accompagné d'hypothèses librement choisies. Une démonstration formelle est alors un arbre de preuve qui comprend des sous-arbres avec à chaque fois des hypothèses librement choisies formant un contexte différent et où le noeud racine du sous-arbre transmet comme résultat, l'implication entre les hypothèses utilisées dans le sous-arbre et sa conclusion.
On homogénise un tel arbre de preuve en utilisant des séquents. Un ensemble de propositions `P` sousmisent à un ensemble d'hypothèses `H` se note `H"⇒"P` est s'appelle un séquent. L'homogénéisation s'opère en remplaçant chaque règle de déduction qui est un programme `phi` transformant un ensemble d'expressions `P` en un autre ensemble d'expression `C`, en un programme `varphi` transformant souvent le séquent `H"⇒"P` en le séquent `H"⇒"C` où `H` est un ensemble de propositions librement choisies servant d'hypothèses. Délors le sous-arbre va s'insérer dans l'arbre de preuve et pouvant rappeler simplement de façon ascendante les hypothèses dans les cas où la règles de déduction ne les perturbe pas.
A la fin du raisonnement, dans la dernière conclusion, aucune hypothèse ne doit rester présente. L'hypothèse ne sert que d'élément catalyseur. Elle permet de déclencher de nouvelle méthode de raisonnement telle le raisonnement par l'absurde, et permet d'accroître considérablement la puissance de déduction par rapport au simple raisonnement directe.
L'étude des structures mathématiques a mis en évidence le principe du raisonnement d'équivalence : Si dans une structure, les éléments `x` et `y` sont équivalents selon une relation d'équivalence respectant les opérateurs de la structure, alors quelque soit un morphisme `f` de cet structure, les images `f(x)` et `f(y)` sont équivalentes. C'est cette propriété qui permet de définir la structure quotient.
Appliqué à notre logique, une proposition est équivalente à une autre si l'une déduit l'autre et que l'autre déduit l'une.
On accorde un sens premier aux structures mathématiques énumérables, car un programme informatique, de par sa nature s'applique à des éléments d'une telle structure. Et comme nous construisons le raisonnement par un programme informatique, ces structures fond nécessairement partis des fondements du raisonnement.
---- 8 juin 2022 ----
Puisque nous voulons revenir à un traitement purement informatique du raisonnement, on en propose une implémentation. Et comme nous voulons procéder par étape, on part du langage vide `"<>"` dans lequel il n'y a pas de négation. Nous somme donc dans une pré-logique, une logique sans négation où les déductions s'apparentent à de simples productions. Notez que les trois principes de raisonnement précédement décrits sont pré-logiques puisqu'ils ne font pas intervenir de négation.
On crée `n` nouveaux éléments `a,b,c,...` qui désigneront des propositions pré-logiques puisqu'il n'y a pas encore de négation. Ce sont des connecteurs nullaires libres, c'est à dire initialement distincts par absence d'information, mais pouvant par la suite se révélés être équivalents. Et qu'entend-on nous par être équivalent ? Deux propositions pré-logiques sont équivalentes si de l'une on déduit l'autre et si de l'autre on déduit l'une. Ce constat ouvrira l'accès au type de raisonnement d'équivalence.
On ajoute par exemple cinq connecteurs nullaires libres `a,b,c,d,e`. Chacun d'eux représente une proposition qui au cours du monologue émis par une théorie qui énumère toutes ses déductions possibles, est soit connue c'est-à-dire publiée, ou bien est momentanément ou de façon permanente inconnue c'est-à-dire non-publiée. Le langage des propositions devient :
`sfL = "{"a, b, c, d, e}"`
Il ne comprend que `5` propositions. Une théorie est par définition un ensemble de propositions, interprété en tant que conjonction. Il y a donc `2^5` théories, étant sous-entendus que l'on dénombre leur expression dans le langage `ccP(sfL)`.
On munie le langage d'un système de démonstration. Et la théorie devient un programme qui énumère tous ses déductions possibles.
On va concevoir ce programme en utilisant une technique de programmation basée sur une gestion des évènements.
Etant donné une variable `x`. Etant donné une propositions génératrice c'est à dire une constante appartenant à `{a,b,c,d,e}`. On affecte cette proposition génératrice à `x`. Par la suite, à l'exécution du programme, chaque occurence de la variable `x` dans le programme désignera son contenu. Puis, on publie `x`.
On part d'un ensemble `E` de propositions publiées initialement vide. On crée la procédure de publication d'une proposition `x` dont l'appel est notée par l'instruction :
`x"≫"`
Cette instruction va rergarder si `x` appartient déjà à l'ensemble `E`, puis s'il n'y appartient pas, alors elle va ajouter `x` dans `E` et émettre un évènement `x` en direction de tous les autres processus. On crée le lanceur de programme sur évènement extérieur, dont l'appel est notée par l'instruction suivante :
`"≫"x "|" sfP`
où `x` récupère la proposition portée par l'évènement, et où `sfP` est le programme à exécuter sur chaque tel évènement, et qui se présente comme une succession d'instructions séparées par des point-virgules. Cette instruction crée un processus qui va écouter tous les évènements en permanence. On définie le programme de chaque proposition. Il contiendra se genre d'instruction qui lance un processus qui ne s'arrête jamais, qu'on laisse tournée en arrière plan tel un service. Le programme de la théorie se résume à lancer le programme de chacune de ses propositions. Les premières règles du système de démonstration sont :
Afin de limiter l'usage des parenthèses, on a munit les opérateurs de programmation d'une priorité syntaxique de la plus forte à la plus faible :
`"⇒"` `"≫"` `"∈"`
Ces deux premières règles du système de démonstration correspond au principe d'identité et d'intemporalité des propositions et au principe qu'une théorie est un ensembles de propositions.
Voyez comment nous avons utilisé un langage plus sophistiqué pour automatiser l'implémentation de propositions génératrice, ainsi que pour l'implémentation de nos théories. Ces programmes ce traduissent littéralement comme ceci :
Voici une bref descritption du langage de programmation :
---- 6 juin 2022 ----
La règle de déduction la plus simple consiste en une implication entre deux propositions génératrices. Par exemple `a"⇒"b` signifie que, si `a` est connue alors on publie `b`. On augmente le langage des propositions par extension élémentaire en ajoutant le connecteur `"⇒(.,.)"` afin de pouvoir exprimer cette règle qui constituera aussi une proposition :
`sfL := sfL["⇒(.,.)"]`
`sfL = "<"a,b,c,d,e,"⇒(.,.)>"`
Mais en intégrant la règle comme étant une proposition, on élargie de faite le langage des règles également qui comprendra par exemple la règle `(a"⇒"b)"⇒"(c"⇒"d)`.
L'implémentation de l'implication met en oeuvre le modus ponens :
`AAx"∈"sfL, AAy"∈"sfL,`
`x"⇒"y ≝ x"⇒"y"≫" ";" (x"∈" sfE "|" y"≫") ";" "≫"z | x"="z "|" y"≫"`
Et voyez que nous avons utilisé une règle plus sophistiquée dans un langage plus riche, pour automatiser l'implémentation de toutes nos règles de base. Ce programe ce traduit littéralement comme ceci : Etant donné trois variables `x,y,z`. Etant donné une implication connue. On unifie cette implication avec le terme `x"⇒"y` ce qui va attribuer à `x` et à `y` des valeurs appartenant à `sfL`. Par la suite, chaque occurence des variables `x, y` désignera leur contenu respectif. Puis on publie `x"⇒"y` . Puis si `x` appartient à `E` alors on publie `y`. Puis sur chaque évènement autre que celui émis par la première instruction, on récupére le paramètre de l'évènement `z`, puis si `x"="z` alors on publie `y`.
Description du langage de programmation (suite) :
De la même façon que la règle s'écrit dans un langage formelle, le programme s'écrit dans un langage formel qu'il convient maintenant de définir précisément.
Le programme utilise des constantes minuscules ou chiffrés telles que `a`, `b`, `1`, qui sont des connecteurs nullaires, puis utilise des connecteurs unaires tels que `"¬(.)"`, `f"(.)"`, puis utilise des connecteurs binaires tels que `"∧(.,.)"`, `"⇒(.,.)"`, `g"(.,.)"`, et qui s'assemblent par composition close finie pour former des termes appelé valeur. Le choix qui est fait ici est de considérer les termes comme étant des compositions close de connecteurs plutot que des séquences de caractères sans condition.
Leur déclaration se fait implicitement à leur première apparition en spécifiant leur arité par un suffixe `"(.)"` pour unaire , `"(.,.)"` pour binaire, `"(.,.,.)"` pour ternaire, etc., ou par absence de suffixe pour l'arité nullaire.
Le programme utilise des variables minuscules `x,y,z`. Chaque variable contient une valeur qui est un terme, ou bien la valeur `"nil"` si elle n'a pas été initialisée et dans ce cas la variable est dite libre. Il n'y a pas de distinction entre une variable libre et une constante, ou un connecteur nullaire, Elles se déclarent donc de la même façon.
On utilise l'opérateur binaire `:=` pour affecter une valeur à une variable. Le premier membre est la variable et le second membre est la valeur. Par la suite, chaque occurence de la variable si elle n'est pas placée comme premier membre de l'opérateur `:=`, désignera son contenu ou elle-même si son contenu est nil, et devra être ainsi remplacée par ce qu'elle désigne lorsque l'on exécutera l'instruction. Ce procédé s'appelle l'évaluation.
Les variables peuvent être utilisées dans la construction des termes. Ils se comportent comme des connecteurs nullaires tant qu'ils sont libres. S'ils ne sont plus libres, la différence apparait lors de l'exécution de l'instruction où les variables placées ailleurs que dans le premier membre de l'opérateur `:=`, sont remplacées par leur contenu. Si on ne souhaite pas que le terme soit évalué, on l'entoure de simples quotes.
Pour sécuriser la programation, on permet de déclarer constant des variables `a,b,c` par l'instruction `"const" a,b,c`, ce qui génère un avertissement lorque une affectation de ces variables se produits. On réinitialiser des variables `x,y,z` par l'instruction `"clear" x,y,z` ou en affectant `"nil"` aux variables `x":="nil` `";"` `y":="nil"` `";"` `z":="nil`. Mais on peut aussi les redéclarer, ce qui les masques par de nouvelles variables dans ce nouveau contexte `"new" x,y,z`.
Le programme utilise des variables ensembles en majuscule `T,R,S`. Chaque variable contient un ensemble de termes, ou bien l'ensemble vide si elle n'a pas été initialisée. On utilise l'opérateur binaire d'affectation `:=` pour affecter un ensemble à une variable ensemble. Le premier membre est la variable ensemble et le second membre est un ensemble de termes. De même par la suite, chaque occurence de la variable ensemble si elle n'est pas placée comme premier membre de l'opérateur `:=`, désignera son contenu, et devra être remplacée par son contenu lorsque l'on exécutera l'instruction. Notez que dans un premier temps, ces ensembles ne sont pas considérés comme des termes mais comme des types. Un ensemble est une grammaire rudimentaire, un langage rudimentaire, et constitue donc un type rudimentaire.
Pour pouvoir produire les termes d'un langage spécifique, le programme utilise la grammaire du langage en question. Pour cela, on utilise des types en majuscule `A,B,C` qui représentent à la fois les symboles non-terminaux de la grammaire et l'ensemble des termes obtenus en les prenant comme point d'entrée dans la grammaire.
Les types sont aussi des constantes et peuvent être utilisé dans la construction des termes en tant que connecteur nullaire. Ils sont utilisés ainsi pour définir les grammaires.
Pour pouvoir définire la grammaire, on utilise l'opérateur binaire `"→"` associant un type à un ensemble de termes. Le choix qui est ainsi fait, consiste à ne considérer que les grammaires algébriques.
On les déclare implicitement comme des connecteurs nullaires par leur première apparition et on précise leur domaine à l'aide de l'opérateur de définission de grammaire `"→"`. Par exemple, considérons les instructions suivantes :
`A→{0,1,f(A),g(A,A)}`
Ces deux instructions séparées par un point virgule qui précise l'ordre dans lequel doivent être exécutées les instructions, définissent le type `A` qui représente l'ensemble :
`A = {0,1,f(0),g(1,1),g(f(0),1),f(g(1,f(1))),...}`
Chaque connecteur, s'enrichit implicitement d'une règle de typage lui permettant de déterminer le type de son résultat :
`f in A"→"A`
`g in A"×"A"→"A`
On remarque qu'une boucle for qui s'applique à un ou zéro cas constitue une instruction if-then, c'est pourquoi ces deux instructions vont être confondues. La boucle for dans sa généralité s'exerce pour toutes les valeurs possibles de ses index satisfaisant une condition. Et il y deux sortes de condition, l'égalité entre terme, et l'appartenance d'un terme à un ensemble.
`"new" x,y,z ";" x "∈" T "|" x "=" y"⇒"z "|" "≫"y"⇒"z`
Ces deux instructions séparées un par un point virgule vont publier tous les termes de la forme `x"⇒"y` contenu dans `T`, où `x` et `y` sont remplacés par n'importe quel terme.
La publication d'un terme `x` se fait par l'instruction `x"≫"`, cela transmet dans la file d'attente le terme avec un numéro de lancement de programme (différent pour chaque lancememt de programme). Le gestionnaire d'évènement, relève la tête de la file c'est à dire la publication la plus ancienne pour toujour les traiter de façon chronologique. Puis il émet l'évènement en direction de tous les processus en écoute qui n'ont pas le même numéro de lancement que celui de l'évènement.
Le programme lance une écoute des évènements exterieur à l'aide de l'instruction `"≫"x "|" P`. Cela constitue un processus qui tourne sans arrêt en arrière plan et qui à chaque évènement exterieur, récupère le terme de l'évènement en `x` et exécute le programme `P` qui est une successions d'instructions séparées par des point-virgules.
Notre langage de programmation est un langage contextuel c'est à dire qu'une portion de code n'a pas la même signification selon où il se trouve. La signification dépent du contexte et donc la syntaxe va être fortement incitée à dépendre également du contexte. Le contexte évolue de façon mineur après chaque affectation de variable. Et il évolue de façon majeur après chaque déclaration de variable.
On va représenter ces grammaires contextuelles d'une manière plus pratique que par une grammaire formelle classique, en implémentant l'emboitement des contextes tel qu'il existe dans les langages de programmation.
---- 5 Juin 2022 ----
Le langage de programmation noté `sfP` comprend deux types de variable `sfL` et `ccpsfL`, et se définit par la grammaire suivante :
`sfL"→"{a,b,c,d,e,(sfL"⇒"sfL)}`
`sfV"→"{x,y,z}`
`sfT"→"{R,S,T,sfL}``sfP"→"{(sfC"|"sfP),(sfL"≫"), (sfT"≝"sfP)}`
`sfC"→"{(sfL"="sfL),(sfL"∈"sfT),(sfL"∈"E),("≫"sfV)}``sfP` représente un programme.
`sfC` représente une condition ou un domaine.
`sfL` représente une proposition.
`sfV` représente une variable de programmation de type `sfL`.
`sfT` représente une théorie ou une proposition.
Afin de limiter l'usage des parenthèses, on a munie les opérateurs de programmation d'une priorité syntaxique de la plus élevée à la plus faible comme suit :
`"⇒"` `"≫"` `"∈"`
---- 29 mai 2020 ----
Les prototype des opérateurs de programmation :
`sfL"⇒"sfL` de type `sfL`
`sfL"≫"` de type `sfP`
`sfL"∈"E` de type `sfC`
`sfL"="sfL` de type `sfC`
`sfC"→"sfP` de type `sfP`
`"≫"sfV|sfP` de type `sfP`
`sfP";"sfP` de type `sfP`
`sfT"≝"sfP` de type `sfP`
`sfL"⇒"sfL` `sfL"≫"` `sfL"∈"E`
Une règle plus riche prendra deux arguments au lieu d'un seul, nécéssitant un connecteur d'implication ternaire "⇒(.,.,.)". Par exemple `a,b"⇒"c`, qui signifie que si `a` est connue et que `b` est connue alors on publie `c`. L'ensemble des règles devient :
`sfR = "<"a,b,c,d,e,"⇒(.,.)","⇒(.,.,.)>"`
`AAx"∈"sfL_2, AAy"∈"sfL_2, AAz"∈"sfL_2,`
`((x,y)"⇒"z) ≝ (x"∈" sfE)"→"((y"∈" sfE)"→"(z"≫"))) ";" ("≫"s|(x"="s)"→")`
Une règle plus riche prendra `n` arguments au lieu d'un ou de deux nécéssitant un connecteur d'implication multi-aire `"⇒(...)"`. Cela se fait en définissant, deux connecteurs binaires l'implication `"⇒(.,.)"` et la conjonction `"∧(.,.)"`. Par exemple `(a,b,c)"⇒"e` s'écrira`(a"∧"b"∧"c)"⇒"e` voilà comment la conjonction apparait. L'ensemble des règles devient :
`sfR = "<"a,b,c,d,e,"⇒(.,.)","∧(.,.)>"`
.
que l'on note :
`(X, X"⇒"Y)|->Y`
Le langage des règles `sfR` peut comprendre des connecteurs nullaires `X,Y` qui jouerons le rôle de variable universelle ou dite libres. Il peut comprendre les connecteurs nullaires `a,b,c,d,e,` qui jouerons le rôle de constantes. Il peut comprendre le connecteur binaire d'implication `"⇒(.,.)"` de syntaxe centrée. Et il peut comprendre des connecteurs binaire, `"↦(.,.)"`, ternaire, `"↦(.,.,.)"` quaternaire , `"↦(.,.,.,.)"` de syntaxe (n,1), appelé opérateur de définition de fonction, et qui détermine la transformation opérée par la règle.
`sfR = "<"a,b,c,d,e, X,Y,"⇒(.,.)","↦(.,.)","↦(.,.,.)","↦(.,.,.,.)>"`
L'application de la règle consiste a procéder à l'unification d'un couple de propositions `(U,V) "∈" sfL^2` avec l'entête de la règle `(X, X"⇒"Y)` où `X` et `Y` jouent le rôle de variable libre. Puis si l'unification réussie alors les variables `X` et `Y` sont affecté par l'unification et possèdent une valeur appartenant à `sfL`. Puis la règle retourne sont corps `Y` dans lequel il faut remplacer `Y` par sa valeur.
Ce langage possède une sémantique interne. A chaque proposition de `sfR` est associé un ensemble de propositions de `sfL`. Les propositions `X` et `a` sont toutes deux des connecteurs nullaires et obéïssent à la même syntaxe. Par contre leur sémantique diffèrent. La proposition `X` désignera `(AAx, x)`, soit l'ensemble de toutes les propositions du langage `sfL`, tandis que `a` désignera le singleton contenant la proposition `a`.
appartenant à `R`
appartenant à `ccP(sfL)`
Ces propositions de sfL_1 sont des règles de déduction opérant sur le langage sfL, Elle produise leur sémantique interne. Ainsi, par exemple la proposition `X=>a` correspond à la règle qui déduit `a=>a`, `b=>a`, `c=>a`, `d=>a`, `e=>a`.
X|->(X=>a)
---- 28 mai 2022 ----
Puis on définit un système de démonstration sous forme d'un logiciel qui publiera toutes les déductions possibles. Le système comprend un ensemble `sfH` de propositions initiales qui doivent être publiées, et un ensemble `sfE` de toutes les propositions publiées, qui va s'accroitre au cours du temps.
L'ordre de publier une proposition `p` se notera par la commande `p"≫"`. L'ordre de lancement d'un programme sur l'évènement déclenché par la publication d'une proposition se notera `"≫"s` où la proposition publiée qui a déclenché l'évènement est récupérée en `s`.
---- 28 mai 2022 ----
Et il va exécuter en parallèle les programmes informatiques associés à ces propositions. Cela va remplir l'ensemble `sfE` des propositions publiées.
On associe au connecteur `"⇒(.,.)"` le programme informatique suivant mettant en oeuvre le modus ponens : Il prend deux arguments `p,q` appartenant au langage `sfL`, le terme `p"⇒"q`, tel un appel de procédure, lance le programme itératif suivant : Il publie la proposition `p"⇒"q`. Si `p` est présent dans l'ensemble `sfE` alors il publie `q`, et pour chaque proposition `s` qui est publiée de l'exterieur si `s=p` on publie `q` :
`p"⇒"q :={`
`(p"⇒"q)>>`
si `p"∈"sfE` alors q>>`
sur l'évènement `>>s` faire
si `p=s` alors q>>`
`}`
L'ensemble `sfE` regroupe toutes les publications. Ce programme est itératif. Une partie se répète à chaque fois qu'une nouvelle proposition est publiée. Le démonstrateur parcours l'ensemble `sfH` des hypothèses, exécute chacune d'elle et exécute chaque nouvelle proposition qui est publiées. L'ordre dans lequel sont éxecutés ces programmes n'a pas d'importance du moment que leur partie itérative sont exécutés périodiquement, le processus énumératif ne s'arrétant jamais.
---- 28 mai 2022 ----