Le raisonnement exacte est un procédé mécanique c'est à dire dont la production et la vérification peut être faite par une machine, un automate composé de rouages et de pièces mécaniques parfaitement bien emboîtés sans aucun jeu, et en appliquant la mécanique classique. On formalise cette machine en un ordinateur, ou en un procédé dit effectif. Le raisonnement, pour être incontestable, doit pouvoir s'effectuer par un programme informatique de taille finie mais qui n'est ni limité par sa mémoire au cours du calcul, ni limité par le temps de calcul. On résume cette propriété en disant qu'il doit être calculable. Le raisonnement est un calcul. Et qu'importe la quantité de mémoire utilisée au cours de l'exécution ni le temps que cela nécessite. Aucune borne n'est imposée à ce calcul autre que la taille des données initiales et du programme initiale qui doit être finie.
Fonder les mathématiques sur ce principe de mécanique classique débarassé des contraintes de temps et de taille pour le calcul mais en partant toujours d'une donnée et d'un programme de taille finie, est le choix du "formalisme" défendu par David Hilbert.
Néanmoins, même si nous considérons la nature du raisonnement comme étant mécanique, il existe une partie inexacte qu'est l'intuition et qui est la partie la plus intéressante de la recherche. Elle se rapproche davantage d'une culture, d'un corpus idéologique ou d'une âme que d'un procédé mécanique et n'est pas préconstruite puisque c'est à nous de la construire, à l'observateur de s'en faire une, et qui, parceque revendiquant une part de liberté irréductible, constituera une part de lui-même.
En particulier le sens réel que l'on peut donner à ces formules mathématiques construites de façon purement mécanique n'est pas défini. Une mathématique coupée du réel, dont le lien ne peut s'établir que par une interface intuitive qui sort nécessairement du cadre formel exacte et touche au mystère essentiel.
David Hilbert (1862-1943) ne connaissait par la hierarchie de Chomsky esquissée en 1956 et démontrée en 1959, une classification des langages avec leur grammaire qui constitue une programmation de leur énumérateur. Cette classification des grammaires est un théorème fondamentale d'une importance considérable comme il y en a un tous les milles ans, et Noam Chomsky est sans doute le seul savant encore vivant pouvant s'enorgueillir d'une telle avancée pour l'humanité. En intégrant cette découverte, le "formalisme" est en mesure de réunifier tous les courants de pensées mathématiques.
La logique dans son sens général est la science du raisonnement. Et on ne peut concevoir de raisonnement sans langage formel. Qu'est-ce qu'un langage formel ? c'est un ensemble de mots composés d'un nombre fini de caractères, qui est énumérable par une machine.
On a donc un alphabet `A` qui regroupe tous les caractères utilisées. Apparaît alors un langage mère plus vaste et plus simple qui contiendra notre langage formel, et qui est l'ensemble de tous les mots possibles avec cet alphabet `A`. On note cet ensemble avec l'étoile de Kleene, `A"*"`, et il comprend le mot vide noté `epsilon`.
Notez que si le langage formel doit être énumérable pour prétendre être commun à chacun d'entre-nous, son complément dans ce langage mère ne l'est pas forcement et n'est nullement nécessaire.
L'alphabet doit également être énumérable. En effet, si le langage est énumérable, en énumérant tous les mots du langage qui sont par principe de taille finie, on peut énumérer tous les caractères utilisés, et définir ainsi l'alphabet.
Si l'aplphabet est infini, étant énumérable par une machine, on peut l'identifier à l'ensemble des entiers naturels `NN`. On remarque alors la possibilité de remplacer chaque tel caractère par une succession fini de chiffres binaires délimitée par un caractère supplémentaire "|", ramenant ainsi l'alphabet `NN` à l'alphabet `{0,1,"|"}`. Autrement dit, il n'y a nulle restriction à ne concevoir que des alphabets finis. Considérons un exemple :
`A = {a,b,c}`
`A"*" = {epsilon, a,b,c,aa,ab,ac,ba,b b,bc,ca,aaa,aab,...}`
On résume la situation comme suit :
La machine qui énumère le langage peut avoir un programme informatique de forme particulière et interpréter une grammaire telle que Noam Chomsky les a définies. La grammaire constitue le programme informatique de la machine, écrit dans un langage de programmation. Le "formalisme" peut tout reconstruire grâce à l'étude de ces machines.
La hierarchie de Chomsky est une découverte fondamentale démontrée en 1959 par Noam Chomsky, célèbre linguiste américain. Il classifie les langages formels en 4 types inclus l'un dans l'autre, du plus général au plus simple :
Pour établir cela, il part d'un langage mère, `A"*"`, l'ensemble des mots d'un alphabet fini `A`, qui joue le rôle de carrière. C'est le langage le plus simple dans lequel sont inclus tous les autres langages. Description par ChatGPT4
Nous n'allons pas nous intéresser à la base de cette classification que sont les langages rationnels, mais directement au sommet, que sont les langages énumérables. Et par définition, on appellera "langage formel" les seuls langages énumérables. Ce premier choix découle des principes du formalisme, le langage devant être commun à chacun d'entre-nous, il est forcement énumérable par une machine.
On remarque qu'en ordonnant les caractères, on définit une bijection canonique entre `A"*"` et l'ensemble des entiers naturels `NN`. Chaque mot du langage mère est associé de façon biunivoque à un entier écrit en base `n`, où `n` est le nombre de caractères de l'alphabet `A`. On obtient ainsi le langage mère `NN` qui peut sembler constituer le langage le plus simple.
On remarque qu'en faisant apparaitre l'opérateur binaire de concaténation `"∗"` entre chaque caractère d'un mot, on projette un langage terminologique sur le langage `A"*"`. Ainsi, au lieu d'utiliser le langage rationnel `A"*"` comme carrière nous pouvons utiliser un langage terminologique noté `A°` qui est un langage algébrique plus riche qu'un langage rationnel, où `A` est un ensemble d'opérateurs dit générateurs, avec chacun une arité préfixée. Le langage terminologique est l'ensemble des compositions closes finies d'opérateurs générateurs non-évaluées appelées termes. C'est le domaine de Herbrand. Par exemple :
`A = {a,b,f"(.)",g"(.,.)"}`
`A° = {a,b,f(a),f(b),g(a,a),g(a,f(a)), f(f(b)), g(f(a),f(b)),...}`
Comme nous définissons un langage mère plus vaste, il est inutile de se contraindre à un bridage arbitraire qu'est l'arité préfixée des opérateurs. On considère donc que tout opérateur possède toutes les arités finies possibles. Ainsi les termes suivants font partie du langage mère, `a, a(a), a(a,a), ...` On remarque qu'en donnant aux termes le rôle d'opérateurs, abolissant la distinction entre opérateurs et termes, le terme se comporte comme un opérateur et peut s'appliquer à son tour à une liste de termes. Cela définit le langage alpha. Par exemple :
`A = {f,g}`
`A^"◎" = {f,g,f(f,f),f(g)(f,g),f(f)(g),f(f,g)(g(f)(f),f)(f),...}`
On résume la situation comme suit :
Puis, rien n'interdit de choisir comme carrière des langages encore plus évolués, de type contextuel. En effet, les propositions mathématiques ont une partie déclarative qui déclare des opérateurs variables, et qui va donc changer le sens de ce qui suit, une caractéristique des langages contextuel. Le sens d'une expression dépend du contexte. Comment introduire cette fonctionalité de façon la moins arbitraire ? Nous ne répondrons pas à la question tout-de-suite.
Après avoir défini la carrière, un langage formel, mère de tous les langages formels (qui sont des sous-enembles de l'ensemble mère), on précise le deuxième critère propre au langage : Il doit être énumérable par une machine. Et ce dernier point se décrit à l'aide de machines dont la définition formelle pose une difficultée toujours irrésolue qui est discutée dans la thèse de Church-Turing. Voir ChatGPT4.
L'intérêt de partir de la forme la plus générale du raisonnement et du calcul, de ce qu'on appelle un procédé effectif, est de pouvoir étudier toutes les logiques possibles et inimaginables.
Dans le "formalisme" c'est une machine qui va tout construire mécaniquement.
Il n'y a pas de différence entre une théorie et une proposition, elle doivent être toutes les deux lisibles en un temps fini et donc de taille finie. Les propositions sont les mots de notre langage formel défini précédement.
Il existe une mécanique et donc un raisonnement avant même la logique. Il faut d'abord la décrire.
Avant la logique, la contradiction n'existe pas, ou plus précisément la négation n'existe pas, cette étonnante symétrie est ignorée, non-atteinte ou non-construite. Néanmoins le raisonnement existe. Il est même nullement altéré dans sa complexité par l'absence de négation. Il est dit prélogique ou sans négation. La proposition n'ayant pas de négation, elle obtient les qualités générales d'un élément, c'est pourquoi on l'appelle aussi un élément. C'est l'élément (ou le mot) d'un langage formel.
Les propositions n'ont pas de négation, elles sont connues ou inconnues. Lorsqu'elles sont connues c'est qu'elles ont été démontrées, produite par la machine démonstrative. Et lorsqu'elles sont inconnues, c'est qu'à l'état actuel où on les évoque, elles n'ont pas encore été démontrées. Les propositions démontrées, sont dites tautologiques. Puis en se plaçant à la fin des temps..., les propositions qui ne sont toujours pas démontrées sont dites indémontrables.
Dans les cas non-triviaux, l'ensemble des propositions indémontrables n'est pas énumérables. C'est à dire qu'il n'existe pas de machine capable d'énumérer cet ensemble. Et on peut le démontrer assez facilement grâce au paradoxe de Godel-Turing, qu'est l'indécidabilité du problème de l'arrêt.
Au départ, on part d'un langage prélogique noté `L` dont on ne connait rien sauf que c'est un ensemble énumérable de propositions, et qui constituera l'ensemble des propositions mises à la disposition du logicien que nous sommes. La machine souche que l'on nomme pareillement `L` énumère cet ensemble.
Puis, il existe un sous-ensemble énumérable regroupant toutes les tautologies, les propositions démontrables, noté `T`, qui est énuméré par un processus appelé système de démonstration ou machine démonstrative. La machine démonstrative que l'on nomme pareillement `T` énumère cet ensemble. Une propostion est démontrée si elle est produite au bout d'un certain temps par cette machine.
Il existe donc deux machines, l'une dite souche `L` qui énumère les propositions, et l'autre dite démonstrative `T` qui énumère les seuls propositions démontrables. La machine démonstrative `T` est plus complexe que la machine souche `L`. En particulier elle la contient, car la machine démonstrative ne doit évidement produire que des propositions appartenant à `L` mais pas toutes, en ne retenant que certaines d'entre-elles, celles dites démontrables.
Du point de vue de la seule calculabilité, cette situation est équivalente à la présence de deux machines : la machine souche `L` qui énumère les propositions, et une machine démone `D` qui énumère les propositions dites démontrables mais dans un langage qui peut-être plus vaste de telle sorte que c'est l'intersection du langage `L` et du langage `D` qui définit le langage `T`.
Notez que si deux langages sont énumérables, leur intersection l'est également. Cela se démontre simplement en construisant la machine qui va énumérer leur intersection : Considérons les deux machines `L, D`. Et programmons notre machine `T` qui va énumérer `L nn D` : On lance l'énumérateur `L`, et à chaque proposition `p` produite, on lance en parallèle l'énumérateur `D`. A chaque production de `L` le nombre d'énumérateurs `D` en cours d'exécution en parallèle s'accroit, et on passe en revue chacun d'eux en comparant ce qu'à produit le `D` correspondant avec la proposition `p` initiale corespondantes, et si elles sont égales alors elles sont produites. Pour formaliser davantage cette démonstration, il convient de fonder un langage de programmation adapté pour écrire simplement cet algorithme.
for `x"∈"L` {
& for `y"∈"D` {
if `x"=="y` {
`x"≫"`
break
}
}
}
L'instruction `x"≫"` produit en sortie la proposition contenue dans la variable `x`. L'opérateur `&` crée un sous-processus exécutant en parallèle la commande qui suit. Le nombre de sous-processus s'accroit propostionnellement au nombre de propositions explorées du langage `L` et persiste dans la durée pour celles indémontrables (soit une infinité). C'est cette contrainte non-réductible de mémoire nécessaire, qui est nécessaire pour pouvoir couvrir tout le domaine de calculabilité.
En définissant la prélogique au chapitre précédent, on a quand même fait un choix de construction arbitraire, qu'est la définition d'une unique valeur de vérité appelée le `"vrai"`. Cette valeur prélogique regroupe toutes les propositions qui sont démontrées (ou posées comme axiomes en nombre fini). Les propositions démontrables possèdent la valeur prélogique `"vrai"` tandis que les autres, les indémontrables, ne possèdent aucune valeur prélogique. C'est la construction la plus simple ne comprenant qu'une unique valeur prélogique, définie par un moteur qui énumère toutes les propositions possédant cette valeur prélogique.
Dans ce paradigme programmatif, où l'on fonde la logique par la programmation, une valeur prélogique définit un ensemble de propositions énuméré par une machine.
Nous pouvons définir non pas une valeur, mais deux valeurs prélogiques, appelées également valeurs de vérités, le `"vrai"_A` et le `"vrai"_B`, et permettre aux propositions d'avoir plusieurs valeurs prélogiques. C'est le cas pour les théories logiques contradictoires où toutes les propositions sont à la fois vrais et fausses. C'est aussi le cas précédement où les propositions indémontrables n'ont pas de valeur prélogique, ou autrement-dit, ont un ensemble vide de valeurs prélogiques ce qui laisse à penser qu'il peuvent avoir un ensemble de plusieurs valeurs prélogiques. Dans ce cas, cela entraine un moteur `T_A` de production des propositions possédant la valeur prélogique `"vrai"_A`, et un moteur `T_B` de production des propositions possédant la valeur prélogique `"Vrai"_B`, et rien n'interdit qu'une même proposition puisse être produite par les deux moteurs.
Nous pouvons faire un autre choix de construction, et définir plusieurs valeurs de vérité exclusives et exhaustives, telle que par exemple le `"vrai"` et le `"faux"`. L'exhaustivité et l'énumérabilité des propositions ayant une ou plusieurs valeurs prélogiques va rendre tout décidable et violer le problème de l'arrêt. Il faut donc enlever l'exhaustivité, et définir plusieurs valeurs de vérité exclusives mais non-exhaustives telles que le `"vrai"_1` et le `"vrai"_2`. C'est-à-dire qu'une proposition pourra ne pas posséder de valeur de vérité, mais si elle en possède, elle ne peut en posséder qu'une seule, le `"vrai"_1` ou le `"vrai"_2`
En terme de calculabilité, cette situation est plus compliqué à décrire : Il existe un moteur énumérant toutes les propositions `"vrai"_1` ou `"vrai"_2` qui seront appellées les propositions vrai. Et dans cet ensemble, il existe une fonction caractéristique calculable, qui appliqué à une proposition vrai, produira toujours `1` ou `2` en un temps fini, selon que la proposition est `"vrai"_1` ou `"vrai"_2`.
Cela revient à la situation où il existe un moteur `T_1` qui produit les propositions `"vrai"_1` et un moteur `T_2` qui produit les propositions `"vrai"_2`, et où il doit y a voir un moyen explicite implémenté dans leur algorithme pour s'assurer que les deux moteurs de produirons jamais une même proposition. (Remarquez que ce moyen ne peut pas s'appuyer sur les parties complémentaires qui elles ne sont pas énumérables dans des cas non-triviaux.)
La machine souche énumérant le langage mère choisi comme langage formel est la première conçue puisque définissant le langage sur lequel repose le calcul et le raisonnement, qui doit être commun à chacun d'entre-nous.
Et d'une manière générale, tout raisonnement est un calcul et tout calcul se ramène à celui d'une machine. En étudiant la machine on étudie la logique.
Son programme est une grammaire, un ensemble de mots (ou de termes ou d'alpha-termes selon la forme de la carrière `A"*"` ou `A°` ou `A^"◎"`) et de règles de substitution de portion contiguë de mot (ou de sous-terme, ou de sous-alpha-terme ), dans un alphabet `A` augmenté de symboles non-terminaux.
Voyons comment, par une succession de 3 étapes que sont l'ajout d'un opérateurs de conjonction, l'ajout d'un opérateur de production, et l'ajout de plusieurs symboles non-terminaux, un telle langage de programmation couvrant le domaine de calculabilité, peut apparaître pour chacune de ces trois carrières.
Dans le langage `A"*"`, chaque mot (qui est une suite finie de caractères appartenant à `A`) désigne une proposition prélogique.
Le langage de programmation reprend le langage mère `A"*"` en ajoutant un opérateur de conjonction, permettant de désigner une succession de mots, un ensemble fini de mots. Le moteur produisant cet ensemble fini de mots est simplement définie par cet ensemble de mots.
On adopte ainsi le paradigme conjonctif, qui fait la distinction entre les propositions atomiques et les ensembles finis de propositions atomiques.
Puis on ajoute un opérateur de production s'appliquant à deux mots pour former une règle. La règle est un couple de mots, séparé par le symbole `"→"`. Par exemple en posant l'alphabet `A={a,b,f,g}`, la règle `ab"→"fg` permet de remplacer n'importe où dans un mot déjà produit, une occurrence du sous-mot `ab` par le sous-mot `fg`. De plus, la règle peut s'appliquer également à une règle déjà présente pour produire une nouvelle règle.
Le langage étendu comprend les mots de `A"*"` et les règles qui sont les couples de mots de `A"*"` :
`A"*"uuA"*"^2`
Une proposition étendue atomique est un mot du langage étendu c'est-à-dire soit un mot de `A"*"` ou soit une règle appartenant à `A"*"^2`. Une proposition étendue est un ensemble fini de mots du langage étendu c'est-à-dire un ensemble fini de mots de `A"*"` ou de règles appartenant à `A"*"^2`. Une proposition étendue constitue une grammaire.
Le mot vide noté `epsilon` permet d'écrire la règle `ab"→"epsilon` qui peut supprimer les sous-mots `ab` n'importe où dans un mot déjà produit. La règle `epsilon"→"ab` peut intercaler des sous-mot `ab` n'importe où dans un mot déjà produit.
La machine (le moteur) qui énumère l'ensemble `A"*"` peut se programmer à l'aide de la grammaire suivante :
`{ epsilon,`
`epsilon"→"a,`
`epsilon"→"b,`
`epsilon"→"f,`
`epsilon"→"g`
`}`
On simplifit l'écriture en prenant comme second membre de la règle non pas un mot mais un ensemble fini de mots que l'on note en séparant ses éléments par le symbole `"|"` :
`{epsilon, epsilon"→"a"|"b"|"f"|"g}`
Le concept de mot vide n'est pas indispensable. Cette fonctionnalité n'est pas nécessaire pour couvrir le domaine de calculabilité des sous-ensemble de `A"*"`. Il y a donc une seconde option qui'il convient de présenter et qui consiste à utiliser le langage étendu suivant :
`A^"+"uu(A^"+")^2`
où `A^"+"` désigne l'ensemble des mots non-vides d'alphabet `A`. Dans cette situation, le mot vide n'existe pas. La machine qui énumère le langage `A"*"` peut se programmer avec la grammaire suivante :
`{ a,`
`a"→"aa,`
`a"→"b,`
`a"→"f,`
`a"→"g`
`}`
et qui s'écrit :
`{a, a"→"aa"|"b"|"f"|"g}`
Ce procédé n'est pas suffisant pour couvrire le domaine de calculabilité des sous-ensembles de `A^"+"`. Il faut recourire à des symboles supplémentaires dits non-terminaux et en nombre non-borné. On déclare de nouveaux symboles par exemple `L,M,N` que l'on ajoute dans l'alphabet `B=Auu{L,M,N}`. Et on définit le langage étendu suivant :
`B^"+"uu(B^"+")^2`
Par exemple, le langage `A"+"` est énuméré par la grammaire suivante :
`{ L,`
`L"→"LL,`
`L "→"a,`
`L"→"b,`
`L"→"f,`
`L"→"g`
`}`
et qui s'écrit :
`{L, L"→"LL"|"a"|"b"|"f"|"g}`
On peut représenter les grammaires par des égalités récurcives d'ensembles, ainsi la grammaire précédente peut s'écrire par l'égalité `L = {LL,a,b,f,g}`. La grammaire va produire des propositions étendues. Un mécanisme simple peut filtrer et ne garder que les productions appartenant à `A"+"`, appelé la production terminale.
On voit donc apparaitre l'aspect déclaratif du langage mathématique, ici, pour déclarer les nouveaux symboles dit non-terminaux, et qui porte le langage mathématique au niveau Type 1, celui des langages contextuels.
La hierarchie de Chomsky nous assure que ce langage de grammaire avec un nombre fini mais non borné de symboles supplémentaires dits non-terminaux, constitue un langage de programmation suffisament puissant pour pouvoir programmer (toujours en un programme de taille finie, c-à-d en une grammaire de taille finie) pour chaque sous-ensemble énumérable de `A"+"`, un moteur en production terminale l'énumérant.
Nous avions déjà ce résultat avec la machine de Turing, mais celle-ci n'était vraiment pas pratique pour la programmation, et aussi avec le lambda-calcul, le langage inventé par Church pour définir les fonctions récurcives. Mais avec Chomsky, on l'a de façon plus adaptable, avec un choix du langage de programmation que l'on peut adapté au problème.
On munit ce langage étendu `B^"+"uu(B^"+")^2` d'une sémantique. Chaque grammaire, qui est un ensemble fini de mots et de couples de mots dans un alphabet augmenté des symboles non-terminaux, énumère dans sa production terminal un sous-ensemble de `A"+"`. Et tous les sous-ensembles énumérables de `A"+"` possède au moins une telle grammaire.
La grammaire énumère également un sous-ensemble du langage étendu qui s'appelle sa complétion. En particulier elle énumèrera de nouvelles règles obtenues par combinaison de règles. Cela ne réduira pas la complexité de production des mots qui est définie comme étant le nombre de règles qu'il faut utiliser pour produire le mots, mais par-contre cela réduira la complexité de production d'un ensemble de mots puisque une même règles composite pourra être appliquées plusieurs fois.
On pourrait ne pas préciser les arités des opérateurs en les autorisant tous, car cela peut être fait aprés coup en se restreingnant dans l'utilisation de ces opérateurs.
Néanmpoins si on autorise toutes les arités finies d'une manière non-bornée, une petite difficulté apparait qui est résolu plus loin. C'est pourquoi on considère d'abord un langage terminologique où les opérateurs peuvent avoir les arités bornées, 0,1,2,3,4 par exemple.
Le langage mère est l'ensemble des compositions closes non-évaluées d'opérateurs appartenant à `A` et possédant toutes les aritées 0,1,2,3,4, noté `A°`. Dans ce langage, chaque terme, qui est une composition close d'opérateurs appartenant à `A`, désigne une proposition prélogique. Notez que le terme vide n'existe pas.
Le langage de programmation reprend le langage mère `A"°"` en ajoutant un opérateur de conjonction. Dans un langage terminologique qui possède une capacité d'expression plus forte, cet opérateur, intégré aux autres opérateurs, peut-être utilisé pour définir un demis-treillis. Par exemple, considérons la proposition suivante :
`"∧"(a,b,c,"∧"("∧"(d,e),"∧"(f,g),h))`
Que l'on note avec une syntaxe centrée comme suit :
`a"∧"b"∧"c"∧"((d"∧"e)"∧"(f"∧"g)"∧"h)`
Elle désigne la conjonction des propositions atomiques `a,b,c,d,e,f,g,h` mais dans un ordre arborescent particulier représenté par un demi-treillis. Les membres `a,b,c` sont en position de rang 1. Le membre `h` est en position de rand 2. Et les membres `d,e,f,g` sont en position de rang 3. Le moteur produisant cet ensemble fini de proposition atomiques est simplement définie par cette conjonction. Et le demis-treillis va préciser dans quel ordre la production va se faire.
On adopte le paradigme conjonctif, qui fait la distinction entre les propositions atomiques, celles n'utilisant pas l'opérateur de conjonction `"∧"` , et les autres.
Puis on ajoute un opérateur de production noté `"→(.,.)"` pour écrire les règles. On le muni d'une syntaxe centrée ce qui nous permet de réécrire `"→(x,y)"` en `x"→"y`. Par exemple, la règle `f(a)"→"g(a,a)` permet de remplacer n'importe où dans un terme déjà produit, une occurrence du sous-terme `f(a)` par le sous-terme `f(a,a)`. La règle peut s'appliquer également à une règle déjà présente pour produire une nouvelle règle.
Dans le langage terminologique remplacé un terme par un autre terme s'apparente à une égalité entre terme. La règle est une demi-égalité. La règle d'égalité `f(a)=g(a,a)` correspond aux deux règles :
`f(a)"→"g(a,a)`
`g(a,a)"→"f(a)`
C'est à dire à la proposition étendue `(f(a)"→"g(a,a))"∧"(g(a,a)"→"f(a))`
Dans un langage terminologique qui possède une capacité d'expression plus forte, l'opérateur de production `"→(.,.)"` étant intégré comme opérateur générateur, des propositions étendues de la forme `f(a"→"b)`, `(a"→"b)"→"(c"→"d)` apparaissent. La proposition étendue `f(a"→"b)` n'opère pas comme une règle mais comme un élément, et la proposition étendue `(a"→"b)"→"(c"→"d)` remplace une occurence de `a"→"b` par `c"→"d`.
Puis une conjonction de règles appliquée à une proposition, retourne la conjonction des résultats de chaque règle appliquée à la proposition :
`(a"→"b"∧"c"→"d)(f(a,a,c)) = f(b,a,c)"∧"f(a,b,c)"∧"f(a,a,d)`
Ce procédé n'est pas suffisant pour couvrire le domaine de calculabilité des sous-ensembles de A"°" . Il faut recourire à des symboles supplémentaires dits non-terminaux et en nombre non-borné. On déclare de nouveaux symboles par exemple `L,M,N` que l'on ajoute dans l'alphabet `B=Auu{L,M,N}`. Et on définit le langage étendu suivant :
`B"°"["∧", "→(.,.)"]`
en donnant à ces opérateurs `"∧", "→(.,.)"` le rôle dynamique précédement décrit.
Le langage `A"°"` restreint aux arités inférieur ou égale à 4, est énuméré par la grammaire suivante :
`{ L,`
`L "→"a,`
`L"→"b,`
`L"→"f,`
`L"→"g`
`L"→"L(L),`
`L"→"L(L,L),`
`L"→"L(L,L,L),`
`L"→"L(L,L,L,L),`
`}`
et qui s'écrit :
`{L, L"→"a"|"b"|"f"|"g"|"LL"|"LLL"|"LLLL}`
Mais une difficulté apparait pour pouvoir énumérer le langage sans contrainte d'arité. A cette fin, on définit les séquences, qui sont passées en argument d'un opérateur en définissant l'opération de concaténation de séquence désignée par `*`. On définit le langage étendu suivant :
`B"°"[*, "∧", "→(.,.)"]`
en donnant à ces opérateurs `*, "∧", "→(.,.)"` le rôle dynamique précédement décrit. Le langage `A"°"` est énuméré par la grammaire suivante :
`{ L,`
`L "→"a,`
`L"→"b,`
`L"→"f,`
`L"→"g`
`L"→"L(L)`
`L"→"L*L`
`}`
et qui s'écrit :
`{L, L"→"a"|"b"|"f"|"g"|"L(L)"|"L*L}`
La différence entre le langage terminalogique et le langage alpha tient dans la possibilité pour tout terme de se comporter comme un opérateur générateurs possédant toutes les arités fini, et donc de pouvoir s'appliquer à son tour à un ensemble fini d'alpha-terme.
On donne alors à la règle son rôle de règle de production. Ainsi par exemple, l'alpha-terme `(a"→"b)(f(a))` s'évaluera en `f(b)`, et l'alpha-terme `(a"→"b)(g(a,a))` s'évaluera en `g(b,a)"∧"g(a,b)`.
Puis lorsque la règles est apliquée à une conjonction, elle s'applique à chacun des membres de la conjonction et regroupe les résultats en une conjonction.
`(a"→"b)(g(a,c)"∧"g(a,a)) = g(b,c)"∧"g(b,a)"∧"g(a,b)`
Puis une conjonction de règles appliqué à une proposition, retourne la conjonction des résultats de chaque règle appliqué à la proposition :
`(a"→"b"∧"c"→"d)(f(a,a,c)) = f(b,a,c)"∧"f(a,b,c)"∧"f(a,a,d)`
---- 3 mars 2024 ----
9) Smullyan
`{0^E,s^(E->E),"+"^(E×E->E),"*"^(E×E->E),=^(E×E->{0,1}),<^(E×E->{0,1})}`
`x=y |-- s(x)=s(y)`
`x=y |-- x<s(y)`
`x<y |-- x<s(y)`
`x=y |-- x+0=y`
`x+y=z |-- y+x=z`
`x+y=z |-- x+s(y)=s(z)`
`x.0=x`
`x"*"y=z |-- y"*"x=z`
`x"*"y=z |-- x"*"s(y)=z+x`
`x=y |-- y=x`
`x=y" et "y=z |-- x=z`
`x=y" et "y<z |-- x<z`
`x=y" et "z <y |-- z<x`
10) Lambda calcul
La machine démonstrative est plus complexe que la machine souche car elle intégre dans son mécanisme de raisonnement la machine souche, mettant en oeuvre un mécanisme un peu plus générale que ce que l'on appelle le raisonnement hypothético-déductif.
---- 14 février 2024 ----
La machine démonstrative est un producteur récurcif indéterministe.
Quelque soit une proposition `x`, on écrit la règle de production `|--x` pour programmer une machine démonstrative et lui permettre de produire `x` au bout d'un certain temps. Cela a pour conséquence de poser `x` comme axiome.
Quelque soit deux propositions `x,y`, on écrit la règle de production `x|--y` pour programmer une machine démonstrative et lui permettre de produit `y` si elle produit `x` au bout d'un certain temps.
Les règles peuvent s'adjoindrent dans un ensemble pour former une machine démonstrative plus sophistiquée. Ainsi la machine `{"⊢"x, z"⊢"y, "⊢"z}` produit les propositions `{x,y,z}`. La machine est un ensemble applatie de règles c'est-à-dire qu'il peut y avoir plusieurs niveau de crochet `{}` cela n'a pas d'influence, de tel sorte que l'on peut adjoindre des machines et des règles dans un même ensemble pour former une machine démonstrative plus sophistiquée.
Au départ nous avons une prélogique définie par un langage prélogique inconnu quelconque `L` et une machine démonstrative `T` inconnue quelconque qui produit des proposition appartenant à `L` définissant un sous-ensemble `T sube L`. Pour indiquer que la machine démonstrative `T` démontre `x` , on écrit :
`T|--x`
Dans cette prélogique, l'adoption de `x` comme axiome se traduit par une nouvelle machine démonstrative `{T, "⊢"x}`
Ce méta-opérateur `|--` ne fait pas parti du langage prélogique. Il fait partie du métalangage qui nous permet de programmer la machine démonstrative ou d'écrire des méta-propositions.
La définition de la prélogique, pour être complète, doit définir en plus une sémantique.
La syntaxe la plus générale étant ainsi décrite en posant deux machines, une machine souche `L` qui énumère les propositions, et une machine démonstrative `T` qui énumère les seules propositions tautologiques, il convient maintenant de définir la signification réelle des propositions.
La sémantique d'une proposition se définit comme étant l'ensemble des mondes où la proposition est réalisée. Mais on n'a pas défini ce qu'était un monde ni comment une proposition se réalise dans ce monde.
On voit la possibilité d'une construction interne canonique.
On commence par construire une sémantique finie où les mondes finis sont désignés par les propositions. En effet, la caractéristique d'une proposition est d'être finis. Et naturellement, dans un monde désigné par `x`, la proposition `y` se réalise si et seulement si la machine `T` dans laquel on ajoute la règle `|--x` produit au bout d'un certain temps `y`.
`"("x|== y")" <=> ({T, "⊢"x}|-- y)`
`x|==y` signifie que `y` se réalise dans le monde désigné par `x`. On reconnait que l'équivalence `<=>` employé ici est un meta-opérateur car il s'applique à des meta-termes et non à des termes. L'expression `{T, "⊢"x}|-- y` signifie que en posant `x` comme axiome on démontre `y`.
La situation de départ étant une prélogique définie par `L` et `T`, ces paramètres fondamentaux sont sous-entendus dans l'usage du meta-opérateur `"⊢"` perçu comme une proposition. Ainsi la méta-proposition `"⊢"x` signifie `T"⊢"x` et la méta-proposition `x"⊢"y` signifit que l'ajout de `x` comme axiome permet de démontrer `y` c'est-à-dire `{T, "⊢"x}|-- y`
La meta-proposition précédente s'écrit plus simplement :
`"("x|== y")" <=> (x|-- y)`
Autre écriture, au lieu de noter `{T, "⊢"x_1,"⊢"x_2,"⊢"x_3}|-- y` qui signifit que si l'on pose `x_1` et `x_2` et `x_3` comme axiome en plus de la théorie `T` sous-ententue alors on démontre `y`, on notera simplement :
`{x_1,x_2,x_3}|-- y`
Mais le principe d'un monde est qu'il peut réaliser une infinité arbitraire de propositions, faisant que le monde ne peut pas se résumer en une proposition. On peut définir les mondes comme désignés par les ensembles de propositions qu'ils doivent satisfaire.
Considérons un ensemble infini de propositions `{x_1,x_2,x_3,...}` posées comme axiomes. Comme le procédé effectif de démonstration ne mettra en oeuvre à chaque démonstration nécessairement qu'une partie finie de cet ensemble d'axiomes. Cet ensemble démontre `y` si et seulement s'il existe une partie finie de cet ensemble qui s'ils sont posés comme axiome démontre `y`.
On définit alors la sémantique comme suit : Les mondes sont désignés par des ensembles de propositions. La sémantique d'une proposition `y` est l'ensemble des mondes qui ont au moins une partie finie qui, s'ils sont posés comme axiome, démontre `y`.
Etant donné un monde `M`, celui-ci est désigné par un ensemble de propositions qui peut être infini. On note `M|==y` pour signifier que le monde `M` réalise `y`. Quelque soit un monde `M` et une proposition`y`, le monde `M` réalise la proposition `y` si et seulement s'il existe une partie finie de `M` qui, s'ils sont posés comme axiome, démontre `y` :
`"("M"⊨" y ")" <=> EE P underset("fini")("⊆") M, (uuu_(x in P) {x}) |-- y`
Le métalangage s'enrichie d'un itérateur d'union portant sur une partie finie incluse dans `M`, et d'un quantificateur existentiel portant l'ensemble des parties finies de `M`. Le procédé de résolution est-il toujours effectif ?
L'ensemble `M` n'est pas forcement énumérable par une machine. Cette éventuelle restriction n'est effectivement nullement avancée dans la définition des mondes. Parcontre l'ensemble `M` est assurement dénombrable puisque étant une partie de l'ensemble `L` (le langage prélogique) qui est énuméré par la machine souche.
Si aucune machine ne peut énumérer les éléments de `M`, sans même se préocuper de savoir s'il en est de même pour les éléments n'appartenant pas à `M`, vous ne pourrez pas faire grand chose avec `M`, fusse-t-il dénombrable.
Le moyen de sortir de cette impasse consiste à replacer la responsabilité de la définition de `M` sur `M`, et d'adopter la conception du monde réel basé sur un axiome du choix qui ne s'appliquerait qu'à cet ensemble : L'ensemble `M`, qui représente un monde réel, connait les propositions quelle contient en sachant les énumérer par un procédé qui peut ne pas être calculable et que l'on notera sous le même nom `M`. L'énumérateur `M` est à priori non-calculable. On l'appellera un révélateur.
En procédant ainsi on regroupe le caractère non-calculable sur l'unique énumérateur `M` appelée révélateur. Tout se passe donc comme si une entité magique nous avait mis à disposition ce révélateur `M. En l'intégrant à notre capacité de calcul, on va augmenter notre domaine de calculabilité sans introduire de contradiction par ailleurs. Par ce fait, `M` devient énumérable. L'ensemble des parties finies de `M` le devient également, Explication par ChatGPT4. Et l'ensemble des propositions réalisées dans `M` le devient également.
Une autre façon de contourner le problème consiste à proposer une définition restreinte des mondes : "Un monde est un ensemble énumérable de propositions".
Il y a donc nécessairement un choix arbitraire d'une conception du monde qui peut être non-mécanique et qui prédispose à la définition de la sémantique, et donc aussi à la définition de la logique et du formalisme.
---- 11 février 2024 ----
6) L'implication `(."⇒".)`
en ajoutant au langage prélogique un opérateur logique à deux arguments propositionnels qu'est l'implication `(".⇒.)"`, et en étendant la machine démonstrative par le seul ajout de juste deux règles de production que sont la règle du modus ponens et sa réciproque :
Quelles que soient deux propositions `x`, `y`, si les propositions `x` et `(x"⇒"y)` sont démontrées alors `y` est démontrée.
Quelles que soient deux propositions `x`, `y`, si le fait d'ajouter dans la machine démonstrative la règle qui dit que `x` est une tautologie, permet de démontrer `y`, alors `(x"⇒"y)` est démontrée.
On note le langage prélogique étendu `L["⇒"]`.
On définit pour chaque proposition `x in L["⇒"]`, une machine démonstrative que l'on nomme pareillement `x` qui est une copie de la machine démonstrative initiale représenté par le méta-opérateur `|--`, et dans laquelle on a ajouté la règle de production `|--x` qui dit que la proposition `x` est une tautologie. Ainsi, la machine `x` énumére un ensemble de propositions appelées les conséquences de `x` et en particulier elle produit `x`.
Etant donné deux propositions `x, y` appartenant à `L["⇒"]`, on note `x |-- y` pour signifier que `y` est une conséquence de `x`, Autrement dit, la machine `x` finira au bout d'un certain temps par produire `y` au cours de son monologue énumératif. On dira que `x` démontre `y`, on dira aussi que `x` produit `y`.
La machine démonstrative préexiste avant notre construction et est définie par la règle de production énumérant les tautologies :
`|--`
On ajoute les premières règles de production communes à toutes les machines démonstratives. Ces règles de production s'appliquent quelque soit `x` et `y` deux propositions quelconques du langage prélogique étendu `L["⇒"]`.
L'identité :
`x|--x`
Le modus ponens :
`(|--x) "et" (|--x"⇒"y) |--y`
Et sa réciproque :
`(x|--y) |-- x"⇒"y`
A ce stade le métalangage permettant de définir la machine démonstrative comprend les deux méta-opérateurs `|--`, `"et"`, et le langage prélogique sur lequel nous n'avons pas d'information est augmenté d'un opérateur à deux arguments propositionnels `=>`, ce qui se note `L["⇒"]`. L'ordre des priorités syntaxiques est le suivant du plus prioritaire au moins prioritaire :
`¬` `"et"` `<=>` `underset("meta")(<=>)` `<=>`
Le symbole `|--` est par principe un méta-opérateur.
On reconnait que le `"et"` employé ici est un meta-opérateur car il s'applique à des meta-termes et non à des termes.
Constatez que si `x` démontre `y` alors à l'aide de la réciproque du modus ponens, `x` démontre `(x"⇒"y)`.
Constatez que si `x` démontre `(x"⇒"y)`, comme `x` démontre `x`, en appliquant le modus ponens, `x` démontre `y`.
Ainsi, quelque soit deux propositions `x,y` appartenant au langage prélogique étendu, la proposition `x` démontre la proposition `y` si et seulement si la proposition `x` démontre la proposition `(x"⇒"y)` :
`(x|--y) <=> (x|--x"⇒"y)`
On reconnait que l'équivalence `<=>` employé ici est un meta-opérateur car il s'applique à des meta-termes et non à des termes.
On ajoute l'opérateur d'équivalence `(."⇔".)` ce qui se note `L["⇒", "⇔"]`. On étend la machine démonstrative par l'ajout de deux règles de production que sont l'élimination de l'équivalence, et l'introduction de l'équivalence. Ces règles de production s'écrivent comme suit : Quelque soit deux propositions `x,y` appartenant au langage prélogique `L["⇒", "⇔"]` :
`(|-- x"⇔"y)|--x"⇒"y` `(|-- x"⇔"y)|--y"⇒"x`
`(|-- x"⇒"y) "et" (|-- y"⇒"x) |-- x"⇔"y`
Remarquez que le `"et"` est un méta-opérateur puisque s'appliquant à des méta-termes, tandis que le `"⇒"` et le `"⇔"` font partie du langage prélogique étendu noté `L["⇒", "⇔"]`
Chaque proposition `x` appartient à une classe d'équivalence notée `hat x` qui est l'ensemble de tous les propositions `y` tel que `|--x"⇔"y` :
`hat x = {y "/" |--x"⇔"y}`
Chaque classe représente une configuration logique différente.
On ajoute l'opérateur vrai noté `⊤` et l'opérateur faux noté `⊥`, ce qui se note `L["⇒", "⇔","⊤","⊥"]`. On étend la machine démonstrative par l'ajout de deux règles de production que sont la définition du vrai et la définition du faux. Ces règles de production s'écrivent comme suit. Quelque soit une proposition `x` appartenant au langage `L["⇒", "⇔","⊤","⊥"]` :
`|-- ⊤` `⊥ |-- x`
On peut commencer par définir une sémantique finie portant sur les seuls mondes finis. La sémantique finie d'une proposition `x` est l'ensemble des mondes finis qui satisfont `x`.
La caractéristique d'être fini est celle des propositions. On va encore se renfermer sur nous-même dans une construction interne qu'on pourrait qualifier de schizophrène. Les mondes sont les propositions à équivalence près.
Un monde `y` réalise une proposition `x` si et seulement si la proposition `y` démontre la proposition `x`. L'ensemble des mondes qui satisfont `x` est l'ensemble des propositions qui implique `x` à équivalence près, appelé aussi l'ensemble des inductions de `x` à équivalence près.
Ainsi l'élément `x in L["⇒", "⇔"]` possède quatre rôles :
La sémantique finie de `x` est l'ensemble des inductions de `x`, l'ensemble des mondes satisfaisant `x`, l'ensemble des propositions démontrant `x`.
Dans les cas non-triviaux, l'ensemble des propositions qui ne sont pas conséquences de `x`, ou autrement-dit qui ne se réalise pas dans le monde `x`, forme un ensemble non-énumérable.
On note `x |== y` pour signifier que le monde `x` réalise `y`.
Dans cette sémantique finie, du fait de notre construction hermétique, quelque soit deux propositions `x,y`, le monde `x` réalise la proposition `y` si et seulement si `x` démontre `y` :
`"("x|== y")"<=> (x |-- y)`
Mais le principe d'un monde est qu'il peut réaliser une infinité arbitraire de propositions, faisant que le monde ne peut pas se résumer en une proposition. On peut définir les mondes comme des ensembles de propositions qu'ils doivent satisfaire. On va définir une telle sémantique encore par construction interne.
On ajoute au langage prélogique un second opérateur logique à deux arguments propositionnels qu'est la conjonction `"et"`, et en étendant la machine démonstrative par le seul ajout de juste deux règles de production que sont l'élimination de la conjonction, et l'introduction de la conjonction.
Quelles que soient deux propositions `x`, `y`, si la propositions `(x "et" y)` est démontrée, alors `x` est démontrée et `y` est démontrée.
Quelles que soient deux propositions `x`, `y`, si `x` est démontrée, et que `y` est démontrée, alors la propositions `(x "et" y)` est démontrée.
Ces règles de production s'écrivent comme suit : Quelque soit deux propositions `x,y` appartenant au langage prélogique étendu par les deux opérateurs `"⇒", "et"` :
`(|-- x "et" y)|--x` `(|-- x "et" y)|--y`
`(|-- x) "et" (|--y) |-- x "et" y`
Remarquez que le premier `"et"` est un méta-opérateur puisque s'appliquant à des méta-termes, tandis que le second `"et"` fait partie du langage prélogique.
Ainsi la proposition `(x "et" y)` représente de façon suffisante et nécessaire un monde qui satisfait `x` et qui satisfait `y`. La machine démonstrative `(x "et" y)` est obtenue à partir de la machine démonstrative en cours en lui ajoutant deux règles de déduction que sont `|--x` et `|--y`, ou dit autrement en ajoutant les axiomes `x` et `y`.
Considérons maintenant un ensemble infini de propositions `{x_1,x_2,x_3,...}` posées comme axiomes. Comme le procédé effectif de démonstration ne mettra en oeuvre à chaque démonstration nécessairement qu'une partie finie de cet ensemble d'axiomes. Cet ensemble démontre `z` si et seulement s'il existe une partie finie de cet ensemble qui, sous forme de conjonction, démontre `z`.
On définit alors la sémantique comme suit : Les mondes sont des ensembles de propositions. La sémantique d'une proposition `p` est l'ensemble des mondes qui ont au moins une partie finie qui, sous forme de conjonction, démontre `p`.
Etant donné un monde `M`, celui-ci est un ensemble de propositions qui peut être infini. On note `M|== x` pour signifier que le monde `M` réalise `x`. Quelque soit un monde `M` et une proposition`x`, le monde `M` réalise la proposition `x` si et seulement s'il existe une partie finie de `M` qui, sous forme de conjonction, démontre `x` :
`"("M"⊨" x ")" <=> EE P underset("fini")("⊆") M, (^^^_(z in P) z) |-- x`
Le métalangage s'enrichie d'un itérateur de conjonction portant sur une partie finie incluse dans `M`, et d'un quantificateur existentiel portant l'ensemble des parties finies de `M`. Le procédé de résolution est-il toujours effectif ?
L'ensemble `M` n'est pas forcement énumérable par une machine. Cette éventuelle restriction n'est effectivement nullement avancée dans la définition des mondes. Parcontre l'ensemble `M` est assurement dénombrable puisque étant une partie de l'ensemble `L` (le langage prélogique) qui est énuméré par la machine souche.
Si aucune machine ne peut énumérer les éléments de `M`, sans même se préocuper de savoir s'il en est de même pour les éléments n'appartenant pas à `M`, vous ne pourrez pas faire grand chose avec `M`, fusse-t-il dénombrable.
Le moyen de sortir de cette impasse consiste à replacer la responsabilité de la définition de `M` sur `M`, et d'adopter la conception du monde réel basé sur un axiome du choix qui ne s'appliquerait qu'à cet ensemble : L'ensemble `M`, qui représente un monde réel, connait les propositions quelle contient en sachant les énumérer par un procédé qui peut ne pas être calculable. On note le moteur de production
On note la fonction caractéristique `M(x)` qui retourne `1` si `x` appartient à `M`, et ne s'arrête jamais, ou retourne `0`, si `x` n'appartient pas à `M`. La fonction `M(x)` est à priori non-calculable. On l'appellera révélation.
En procédant ainsi on regroupe le caractère non-calculable sur l'unique fonction caractéristique `M(".")` appelée révélation. Tout se passe donc comme si une entité magique nous avait mis à disposition cet révélation `M(".")`. En l'intégrant à notre capacité de calcul, on va augmenter notre domaine de calculabilité sans introduire de contradiction. Par ce fait, `M` devient énumérable. L'ensemble des parties finies de `M` le devient également, Explication par ChatGPT4. Et l'ensemble des propositions réalisées dans `M` le devient également.
Une autre façon de contourner le problème consiste à proposer une définition restreinte des mondes : "Un monde est un ensemble énumérable de propositions".
Il y a donc nécessairement un choix arbitraire d'une conception du monde non-mécanique qui prédispose à la définition de la sémantique, et donc aussi à la définition de la logique et du formalisme.
---- 10 février 2024 ----
On étend le langage prélogique en un langage logique `L["⇒","⇔","⊤","⊥","¬"]` en lui ajoutant l'opérateur de négation noté `¬(.)` en créant une symétrie parfaite inversant les conséquences et les inductions à l'aide des règles de production suivantes ajoutées à la machine démonstrative :
`(|-- x=>y) |-- ¬y=>¬x` `"¬¬"x|-- x `