Qu'est ce que le raisonnement formel. C'est un langage formel et un système de démonstration formel. Et il n'est pas nécessaire de donner un sens au formule, une sémantique, pour définir finalement une théorie... car le raisonnement n'est qu'un calcul sur la forme, qui peut être effectué par un algorithme énumérant toutes les déductions possibles.
Nous allons construire en parallèle, le langage des propositions, `ccL`, et le système de démonstration, `ccM`, en ajoutant un à un des connecteurs au langage `ccL` qui permettront de construire des propositions complexes, et une à une des règles de déduction, au système `ccM`, qui permettront d'effectuer des démonstrations complexes. La construction passe par des stades embryonnaires qui sont des systèmes évoluant pas à pas s'apparantant à des chaines de Markov pour finalement aboutir à la définition de la logique minimale.
Pour avoir une visions concrète du système de démonstration, on développe un algorithme mettant en oeuvre ces règles de production et qui énumère toutes les déductions possibles. On développe en parallèle le langage de programmation pour écrire cet algorithme.
On discute des principes intuitifs qui prédisposent les premiers choix de construction, et on présente une génèse révèlant un ordre canonique dans lequel sont introduit les concepts de base. Nous développons ainsi en parallèle trois langages ; le nouveau langage logique génésique, le langage logique classique utilisé pour le décrire, et un langage de programmation pour le simuler.
On commence par le langage élémentaire `ccL_0` le plus rudimentaire ne contenant que des propositions atomiques. Leur signification n'est pas précisée. Ces propositions ne doivent pas être considérées comme des variables booléennes, mais juste comme des éléments désignés par des noms.
`ccL_0 = {a,b,c,d,...}`
Il y a déjà là un choix important qui définit l'élément comme étant le signifié, le signifiant étant le nom utilisé. Ce choix résulte de notre objectif : Fonder le raisonnement formel à partir de l'écriture. Rien n'interdit que deux noms d'élément désignent le même élément.
Il résulte néanmoins de ce choix que les éléments au delà de leur noms, sont nécessairement distincts et intrinsèquement discernés. On aurait pu considérer, en s'inspirant de la mécanique quantique, un ensemble de particules indiscernables... se comportant différemment qu'un ensemble de particules bien identifiés individuellement car le nombre de configurations distinctes possibles n'est pas le même. Qu'importe, dans ce cas là, nos éléments distincts sont alors les configurations distinctes et non les particules.
L'élément est intemporelle, autrement dit, il a existé et existera toujours, c'est son aspect mathématique.
L'élément ne possède pas de valeur booléenne. Une proposition, représentée ici par un élément de `ccL_0`, n'est ni vrai ni fausse, elle est seulement désignée par un nom.
A ce stade, l'état du système est une proposition atomique de `ccL_0`. Comme nous sommes des être limités, la quantité d'information que représente notre état sera toujours fini. Il en résulte que `ccL_0` et `ccM_0` sont finis. Et cet état change à l'instant suivant en appliquant une règle de production de `ccM_0`, principe de l'évolution d'un système pas à pas. L'évolution du système de dépend que de l'état en cours. Les règles de production sont donc de la forme :
`x"⊳"y`
Où `x` et `y` sont des propositions atomiques appartenant à `ccL_0`. On les identifie aux couples `(x,y)`. Ces règles sont les seuls choses qui ont une définition précise, une sémantique que l'on connait puisque qu'on les construit, concernant notre langage génésique. Le moteur `ccM_0` se conçoit naturellement comme un ensemble quelconque de telles règles.
`ccM_0 sube ccL_0^2`
Les règles de production indique un sens du temps. Pour inverser l'évolution, on inverse chaque règle et cela revient à inverser le sens du temps.
S'il existe deux règles `a"⊳"b` et `a"⊳"c` alors l'état du système peut choisir d'évoluer selon l'une ou l'autre règle. Le moteur sera indéterministe.
S'il n'existe aucune règle prenant comme premier argumant `a` alors le devenir de l'état `a` n'existe pas, l'univers est inachevé et l'évolution du système se bloque sur une erreur invalidant toute l'évolution. Il existe donc une contrainte sur le moteur, celui-ci doit constituer une relation de première composante partout définie :
`AAx "∈" ccL_0, EE(y,z) "∈" ccM_0, x"="y`
C'est le stade élémentaire.
On utilise un langage de programmation pour écrire l'algorithme évolutif qui constitue la véritable concrétisation du raisonnement. Et on utilise la logique classique pour décrire notre système. Dès lors, il existe trois langages bien distincts :
N'ayant mis en oeuvre que les deux concepts, celui d'éléments représentant un état possible du système, et ceui de moteur représentant un ensemble de règles inclus dans `ccL_0^2`. Les instructions possibles du langage de programmation sont trés rudimentaires. On conçoit :
Pour décrire l'algorithme de calcul nous allons utiliser un langage de programmation le plus proche possible de notre langage mathématique pour réduire l'effort de transcription et ainsi le risque d'erreur. L'algorithme s'écrit :
`AA(E,x) "∈" ccM_0, E"="x`
L'instruction `AA(E,x) "∈" ccM_0,` est une boucle "for". Elle est interprété dans un contexte où la variable `E` est déjà déclarée puisqu'il s'agit de l'état du système. C'est une boucle "for" où le terme `(x"→"y)` avec la variable `x` liée et la variable `y` libre, est unifié à tour de rôle à chaque élément de `ccM_0`. L'instruction `E"="x` change l'état de `E` en le positionnant sur la proposition `x`. Remarquez que l'algorithme ne détaille pas dans quel ordre est fait le calcul. Cette ordre est au hasard, ce qui garantie une équiprobabilité en cas d'indéterminisme.
Les propriétés possibles sur une proposition atomique `a` appartenant à `ccL_0` sont de formes très rudimentaires :
l'état du système à l'instant `t`, est la proposition `a`. l'état du système à l'instant `t`, est différent de `a`. `a` et `b` désignent le même élément. `a` et `b` désignent deux éléments distincts. l'état `a` peut évoluer en l'état `b`. l'état `a` ne peut pas évoluer en l'état `b`. Quelque soit un élément `x` de `ccL_0`, il satisfait la propriété `P(".")`. Il existe un élément `x` de `ccL_0`, il satisfait la propriété `P(".")`.
Le développement du langage `ccL` ne devra pas utiliser les mêmes symboles que ceux de la logique classique.
Conjonction Disjonction Équivalence Implication
en une étapeNégation La logique classique : La logique génésique :
On considère que l'état du système est un ensemble de propositions. C'est le moyen le plus simple pour rendre déterministe l'évolution décrite précédément qui proposait différents états futures possibles chacun caractérisé par une proposition atomique. On prend comme état future non pas une de ces possibilités mais l'ensemble de tous ces états futures possibles. Cela inclus l'ensemble vide `Ø` s'il n'y avait aucun état future. Ainsi le processus redevient déterministe et n'est jamais bloqué. Autrement-dit, on pose comme premier axiome que l'état du système `E` est un ensemble de propositions atomiques :
`E sube ccL_0`
Le langage génésique devient `ccL_1 = ccP(ccL_0)`. En identifiant la proposition atomique au singleton la contenant, on perçoit le langage `ccL_1` comme un agrandissement de `ccL_0`. Les propositions sont maintenant des ensembles de propositions atomiques.
Sans doute un avatar du capitalisme dont nous sommes porteur, le chemin qui nous semble le plus naturel pour procéder à ce regroupement des états futures est la notion d'accumulation des connaissances, et des pouvoirs qui en résultent. L'état du système correspond à l'état de nos connaissances et il évolue pas à pas à chaque instant. L'état est un ensemble de propositions atomiques correspondant à une conjonction logique. Et chaque connaissance est associée à un pouvoir de production qui s'ajoute. Si un ensemble de propositions `y` contient l'ensemble `x`, alors `y` produit au moins ce que produit `x`. Le second axiome est donc le suivant :
`AA(x,y,z) "∈" ccL_1^3, (x"⊳"z "et" x"⊆"y) => (y"⊳"z)`
Les règles de production sont de la forme :
`x"⊳"y`
Où `x` et `y` sont des ensembles de propositions atomiques. On les identifie aux couples `(x,y)`. Le moteur `ccM_1` se conçoit naturellement comme un ensemble quelconque de telles règles.
`ccM_1 sube ccL_1^2`
On commence par présenter l'algoritme car c'est le plus facile à décrire puisque c'est ce qui est le plus concret. S'il l'ensemble vide n'intervient pas dans les règles, l'algorithme s'écrit ainsi :
`EE F "⊆" ccL_0, F"="{}`
`AA(x,y) "∈" ccM_1, "if" (x "⊆" E) "then" y"≫"F`
`E"="F`
L'instruction `EE F "⊆" ccL_0,` déclare une variable `F` de type ensemble de propositions atomiques. Cette variables est initialisée à vide `F"="{}`. L'instruction `AA(x,y) "∈" ccM_1,` est une boucle for où l'indexe `(x,y)` composé de deux variables libre de type ensemble de propositions atomiques, est unifié à tour de rôle à chaque élément de `ccM_1`. L'instruction `y"≫"E` ajoute les proposition atomiques contenue dans `y` dans l'ensemble `E`. Remarquez que l'algorithme ne détaille pas dans quel ordre est fait le calcul. Cet ordre n'a pas d'importance. L'évolution est déterministe.
Mais l'interprétation de l'ensemble vide est particulière. Car c'est à la fois un ensemble et une proposition atomique.
`{}"="Ø`
Si l'état `x` ne produit rien alors il produit l'ensemble vide et donc tout ensemble contenant `x` doit produire l'ensemble vide. Pour que le présent algorithme mettent en oeuvre cette fonctionnalité, il faut un condition sur le moteur, à savoir que tous les éléments atomiques qui produisent l'ensemble vide doivent apparaître sous la forme de règle `{x}"⊳"Ø`. Et en particulier si l'ensemble vide produit l'ensemble vide, la règle `Ø"⊳"Ø` doit être présente dansle moteur `ccM_1`
---- 2 août 2024 ----
Pour définir algébriquement ces ensembles, on étend le langage `ccL_0` en lui ajoutant un connecteur binaire `"∧(.,.)"` et un élément `Ø`. Cela définit un langage étendu noté `ccL_1= ccL_0["∧(.,.)", Ø]` dans lequel les propositions sont des arbres binaires où les noeud sont des connecteurs `"∧"` et où les feuilles sont des propositions atomiques de `ccL_0` ou l'élément `Ø`. Et on pose comme premier axiome que ces connecteurs soit capablent de définir un ensemble de propositions où l'ordre des propositions n'a pas d'importance. Autrement-dit, on pose comme premier axiome que le connecteur soit commutatif et associatif et admet `Ø` comme élément neutre :
`x"∧"Ø = x`
`x"∧"y = y"∧"x`
`x"∧"(y"∧"z) = (x"∧"y)"∧"z`
Apparait une proposition particulière qui regroupe toutes les propositions du langage, noté paraillement `ccL`.
L'ensemble des connaissance à un instant `t` peut être vide, `E(t)"="{}` ce qui ne correspond à la proposition `Ø`. Et donc dans ce cas `E(t)"="Ø`.
Notez que ces égalités sont des propriétés sur les éléments de `ccL_1` qui affirme des transformations possibles d'un élément en un autre et réciproquement, par des règle de la logique classique et qui ne sont pas encore intégrés dans le moteur `ccM_1`.
On explore différentes propriétés en logique classique sur les propositions de `ccL_1` qu'il est possible de définir : Du fait du caractère ensembliste de la conjonction, un connecteur associatif et commmutif, et de la présence de la proposition vide `Ø`, les éléments de `ccL_1` se comportent comme des ensembles de propositions atomiques de `ccL_0`. On peut donc définir l'inclusion et la non inclusion. La propriété `x"⊆"y` signifie que toutes les propositions atomiques contenue dans `x` sont dans `y`. L'inclusion se définit comme suit :
`(x "⊆" y) <=> EEz "∈" ccL_1, (x"∧"z)"="y`
Notez que pour parcourir tous les éléments contenant `x` il suffit de parcourir tous les éléments en l'ajoutant à `x`. La propriété `x"⊈"y` signifie qu'il existe une proposition atomique contenue dans `x` qui n'est pas dans `y`. L'inclusion se définit comme suit :
`(x "⊈" y) <=> AAz "∈" ccL_1, (x"∧"z)"≠"y`
Sans doute un avatar du capitalisme dont nous sommes porteur, le chemin qui nous semble le plus naturel pour procéder à ce regroupement des états futures est la notion d'accumulation des connaissances, et des pouvoirs qui en résultent. L'état du système correspond à l'état de nos connaissances et il évolue pas à pas à chaque instant. L'état est un ensemble de propositions atomiques correspondant à une conjonction logique. Et chaque connaissance est associée à un pouvoir de production qui s'ajoute. Si un ensemble de propositions `x` contient l'ensemble `y`, alors `x` produit au moins ce que produit `y`. Le second axiome est donc le suivant :
`(x"⊳"z) => (x"∧"y)"⊳"z`
Les règles de production du moteur `ccL_1` sont de la forme `x"⊳"a` où `x` est une proposition de `ccL_1` et `a` une proposition atomique de `ccL_0`. On étend cette relation `"⊳"` au cas où `a` est une proposition quelconque de `ccL_1` en adoptant l'axiome suivant :
`(x"⊳"(y"∧"z)) <=> ((x"⊳"y) "et" (x"⊳"z))`
Cet axiome affirme une forme de distributivité de `"⊳"` par rapport à la conjonction `"∧"`. À ce stade le moteur `ccM_1` est un ensemble quelconque de règles de la forme `x"⊳"y` où `x,y` sont deux propositions de `ccL_1`.
Cet état ensembliste `E(t)` sous forme d'une grande conjonction regroupe toute notre connaissance. Il nous représente d'une certaine façon. Son identité est donc liée à notre identité, et est donc sujet aux mêmes questions. Et l'évolution introspective que nous décrivons ici ne dépend que de cet état en cours.
À ce stade nous pouvons apprendre comme nous pouvons oublier.
Ainsi à un instant donné `t`, chaque proposition atomique est soit connue ou inconnue, et rien ne présage du devenir de ces propositions. Les valeurs logiques, vrai et faux, n'existent pas encore, ce sont les valeurs muables de connu ou de inconnu qui existent, et à l'instant suivant ces valeurs peuvent changer.
Ce n'est pas l'identité des éléments qui est remise en cause ici, c'est notre identité qui change. L'élément est immuable, notre connaissance, non.
Et la situation est symétrique si on inverse le temps, les règles de productions sont inversées, et à ce stade de la génèse où il n'y a pas de règle, il n'y a pas de sens privilégié du temps, et donc en particulier il n'y a pas de début.
Toute proposition doit être par principe de taille finie car elle doit pouvoir être lue. Et notre connaissance globale doit être également finie, car nous sommes des êtres limités. Notre connaissance globale apparait sous la forme d'un ensemble de propositions atomiques `E(t)` qui est une conjonction et donc une proposition nécessairement de taille finie.
Une proposition `x` est connue à l'instant `t` si et seulement si elle est incluse dans `E(t)`. Elle restera connue à l'instant suivant, si et seulement si on la produit à partir du moteur `ccM_1` en une seule étape et en supposant que `E` est connu à l'instant d'avant.
`(E(t)"⊳"x) <=> (x sube E(t"+"1))`
`E(t)"⊳"E(t"+"1)`
C'est le stade déterministe.
La règle de production en une seule étape, `"↦"`, est la procédure la plus précise que nous connaissons sur notre nouveau langage puisque nous la construisons. Il convient maintenant d'introduire le connecteur de production `"↦"` dans le langage `ccL_1`. On définit ce connecteur que l'on note pareillement `"↦"`. Ce connecteur a une signification complétement définie et qui est la même que `"⊳"` en logique classique.
On étend le langage `ccL_1` en lui ajoutant un connecteur binaire `"↦(.,.)"`. Cela définit un langage étendu noté `ccL_2=ccL_1["↦(.,.)"]` dans lequel les propositions sont des arbres binaires où les noeud sont des connecteurs `"↦"` et où les feuilles sont des propositions de `ccL_1`.
Quelque soit `x,y` deux propositions quelconques de `ccL_2`, la proposition `x"↦"y` a la même signification que la propriété `x"⊳"y`. Elle signifit que l'on peut produire `y` en une seul étape en utilisant les règles de `ccM` et en supposant `x` connu. En logique classique on parlera de la relation `"⊳"` opérant dans `ccL_2`, et dans le langage génésique on parlera de connecteur `"↦"`
Jusqu'à présent les propositions n'avait pas de sémantique. Et là, on donne une sémantique bien précise aux propositions de la forme `x"↦"y`. Et on reporte la contrainte de cette sémantique sur le moteur `ccM`. La proposition `x"↦"y` affirme la propriété `x"↦"y` qui s'écrit `x"⊳"y`. Mais elle n'est pas au sens propre une règle de production, ce n'est qu'une directive appartenant au langage `ccL_2`. Les règles de production sont appelées règles moteurs et appartiennent au moteur `ccM`, et elles mettront en oeuvre la directive, ce qui en assurera sa sémantique. On supprime donc toutes les règles moteurs pour n'en garder qu'une mais avec des variables quantifiées universellement. La règle moteur qui permet de mettre en oeuvre ces directives est le modus ponens.
Les axiomes qui accompagnent l'introduction des connecteurs `"↦,∧,Ø"` sont :
`x"∧"Ø = x`
`x"∧"y = y"∧"x`
`x"∧"(y"∧"z) = (x"∧"y)"∧"z`
`(x"↦"z) => (x"∧"y)"↦"z`
`(x"↦"(y "∧" z))<=>((x"↦"y) "et" (x"↦"z))`
Ces axiomes peuvent être transcrit dans le moteur `ccM_2` comme suit :
`x"∧"Ø "↦" x`
`x"↦"x"∧"Ø `
`x"∧"y "↦" y"∧"x`
`x"∧"(y"∧"z) "↦" (x"∧"y)"∧"z`
`(x"∧"y)"∧"z"↦"x"∧"(y"∧"z)`
`(x"↦"z) "↦" ((x"∧"y)"↦"z)`
`(x"↦"(y "∧" z))"↦"((x"↦"y) "et" (x"↦"z))`
`((x"↦"y) "et" (x"↦"z))"↦"(x"↦"(y "∧" z))`
aux quels on ajoute le modus ponens :
`(x"∧"(x"↦"y)) ⊳ y`
Le résultat n'est pas propice à concevoir un algorithme de déduction efficace. On reformule l'état du sytème en introduisant un connecteur ensembliste.
L'état du système est un ensemble de propositions. Il peut être décrit en utilisant à la place du connecteur binaire `"∧(.,.)"`, un connecteur multi-aire `{...}` de définition d'ensemble. Cela inclus l'ensemble vide `{}` obtenu en appliquant le connecteur multi-air à zéro arguments. Et, le nombre de propositions atomiques étant fini, cela inclus l'ensemble de toutes les propositions atomiques `ccL_0`.
Et on pose comme premier axiome que le connecteur ensembliste est applati, c'est à dire qu'il n'existe pas d'ensemble d'ensembles, que lorsque on ajoute un ensemble non vide dans un autre on ne fait qu'ajouter ces éléments dans l'autre. Autrement dit, un ensemble ne peut pas avoir comme élément un ensemble autre que l'ensemble vide. Et on identifie la proposition `x` au singleton `{x}`.
On rejoint une logique du second ordre comprenant deux types de variables, les propositions atomiques de `ccL_0` désignées par des variables majuscules, et les proposition de `ccL_1` désignées par des variables minuscules sachant que ces dernières contiennent les premières.
Les règles de production du moteur `ccL_1` sont de la forme `x"⊳"A` où `x` est une proposition de `ccL_1`, et `A` une proposition atomique de `ccL_0`. On étend cette relation `"⊳"` au cas où `A` est une proposition quelconque de `ccL_1` en adoptant l'axiome suivant : La production d'un ensemble de propositions est équivalente à la production de chaque proposition de l'ensemble :
`(x"⊳"y) <=> AAZ"∈" y, x"⊳"z`
Que l'on transcrit en utilisant que des variables de `ccL_1` :
`(x"⊳"y) <=> AAz"⊆"y, x"⊳"z`
Un premier principe déterministe, c'est à dire au stade avant le principe d'identité, précise la nature conjonctive et accumulative des ensembles applati de propositions. Si un ensemble de propositions produit une proposition `z` alors tout ensemble de propositions le contenant produit également `z` :
`(x"⊳"z "et" x"⊆"y) => (y"⊳"z)`
L'évolution du système est déterminé et ne dépend que de l'état en cours. S'il existe deux règles `x"⊩"y` et `x"⊩"z` alors cela à la même signification que la règle `x"⊩"(y"∪"z)`. Autrement dit, l'évolution pas à pas est une application croissante `f` appartenant à `ccL_1"→"ccL_1` c-à-d telle que :
`(x"⊆" y)=>(f(x) "⊆" f(y))`
-*-*-*-*-*-*-*-*-*
`f(X)` désigne ce que produit la connaissance seule de `X` en une seule étape. Si l'état du système est à un instant `A`, alors il évoluera comme suit :
`A,f(A), f(f(A)), f^3(A), f^4(A),....`
La propriété `X"⊩"y` équivaut à `y "∈" f(X)`, elle signifie que `y` est produit en une étape à partir de la connaissance des propositions de `X`. À ce stade déterministe, le moteur est représenté par un ensemble de règles de la forme `X"⊩"Y`
La première règle de production que l'on considère est celle du modus ponens qui affirme que quelque soit deux propositions `X,Y,` si `x` et `x"↦"y` sont connus alors la règle du modus ponens produit `y` et donc met `y` dans l'ensemble des propositions connus. Vous aurez remarqué que le modus ponens est mis en oeuvre avant même le principe d'identité. Le modus ponens se définit algorithmiquement comme étant la règle moteur de production en une étape.
`(x "et" (x"↦"y)) ⊳ y`
Littéralement : Si `x` appartient à `E(t)` et si `x"↦"y` appartient à `E(t)` alors `y` appartiendra à `E(t"+"1)`. On peut donc écrire le modus ponens également comme suit, avec comme priorité syntaxique du plus prioritaire au moins prioritaire : `"∈", "et", =>`:
`x"∈"E(t) "et" (x"↦"y)"∈"E(t) => y"∈"E(t"+"1)`
Le modus ponens assure ainsi que la sémantique de la proposition `a"↦"b` correspond bien à celles de `a"⊳"b`.
Ajouté à la règle d'identité, le modus ponens ne suffira pas pour définir une logique. Car cette règle élimine un connecteur de production `"⊳"` mais aucune autre règle à ce stade ne permet de le réintroduire dans les productions. De sorte que les productions ne sont que des sous-termes, ce qui est insuffisant pour définir une logique. Il conviendra donc d'ajouter une règle réciproque en quelque sorte qui introduit le connecteur de production dans ses productions, et c'est ce que fera le raisonnement hypothético-déductif qui en l'état actuel avec comme seul connecteur de production celui à une seul étape, ne peut pas êtte mis en oeuvre.
Le modus ponens se définit mathématiquement comme étant la règle moteur qui va donner à la relation de déduction `"↦"` la propriété suivante :
`(x"↦"y) => (x"⊳"y)`
Pour décrire l'algorithme de calcul nous allons utiliser un langage de programmation le plus proche possible de notre langage mathématique pour réduire l'effort de transcription et ainsi le risque d'erreur. Le modus ponens se définit par l'algorithme suivant :
`AAx"∈"E, AA(x"↦"y)"∈"E, y"≫"E`
L'instruction `AAx"∈"E,` est une boucle "for" où l'indexe `x` parcours tous les éléments de `E`. L'instruction `AA(x"↦"y)"∈"E,` est interprété dans un contexte où la variable `x` est déjà déclarée. C'est une boucle "for" où le terme `(x"↦"y)` avec la variable `x` liée et la variable `y` libre, est unifié à tour de rôle à chaque élément de `E`. L'instruction `y"≫"E` ajoute la proposition `y` dans l'ensemble `E`. Remarquez que l'ensemble `E` s'agrandissant, les boucles for s'agrandissent et que l'algorithme ne détaille pas dans quel ordre est fait le calcul mais exige qu'il énumère bien tous les cas dans un processus énumératif unique, ce qui exige un parallélisme de calcul et une gestion évènementielle.
On applique la méthode Shadok c'est à dire qu'on remplaçe les boucles "for" par une succession de `n` tirages au sort. Et on choisie une heuristique, 2 nombres de tirages, une pour chaque boucle "for".
---- 27 juillet 2024 ----