C'est à cause du paradoxe de Russel que l'on s'interesse à la notion de catégorie. En effet, ne pouvant définir l'ensemble des ensembles, on se contente de définir la catégorie des ensembles, une catégorie qui n'est pas un ensemble. Mais la catégorie obéït à la même théorie des ensembles ZFC, réitérant le même paradoxe, et aboutissant à concevoir un nouveau type de catégorie qui n'est pas une catégorie, et ainsi de suite. Ainsi il existe une infinité de catégories d'ensemble.
Puis nous utilisons l'axiome du choix qui nous permet de traiter des infinis. Cet axiome permet que chaque ensemble puisse être rendu bien ordonnée, autrement dit, qu'il existe un ordre dans le quel chaque partie de l'ensemble contient un plus petit élément. Ce qui rend possible la récurcivité transfinie. Intuitivement, comme nous le verrons, cela signifie que notre vision constructive énumérable des mathématiques prétendu naïve contient en faite toutes les mathématiques.
Alors, amusons-nous dans une telle construction. On part du point de vue élémentarien où tout est calcul. Puis dans une spirale exploratrice ascendante, on revisite les bases de l'algèbre et de la logique en réordonnant les définitions. La logique peut être définie à travers l'algèbre même, permettant ainsi une génèse commune. Les mathématiques élémentariennes sont jumelles de l'informatique, n'usant comme seul fondement, que du langage et de la programmation.
La formalisation des démonstrations entraine une complexité croissante qui nuit à la compréhension globale noyant l'important dans le détail. Mais le choix d'un langage adapté résoud d'autant cette complexité. Ne dit-on pas que l'exposé d'un problème dans un langage adapté constitue la moitier de sa résolution ?
Nous procèdons à une construction rigoureuse des mathématiques, comme l'on fait le groupe N. Bourbaki, mais avec une autre optique basée sur la construction des objets, du langage et des programmes plutôt que sur celle des démonstrations, la construction d'une sructure constituant la démonstration de son existence. Cela passe toujours par la construction de structures de données, de langages formels et de programmes exécutables.
Le point de départ est l'élément. Un élément est un identifiant unique, qui sert de référence pour désigner toute chose que nous créons.
Mais l'élément peut être nommé de plusieurs manières par des termes d'un langage et par une théorie qui en définit son unicité. Du point de vue élémentarien, on constatera qu'un élément ne peut contenir qu'une quantité finie d'information. Et pourtant, il peut simuler les infinis les plus invraisemblabes, grâce à l'axiome du choix qui assure l'existence d'un bon ordre et permet la récurrence transfini.
L'élément peut désigner toute chose. Mais c'est avant tout un identifiant..., et qui peut juste se désigner lui-même.
Si on conçoit une génèse, un ordre de création des éléments, ce que s'apprète à faire l'algèbre naissante, il est alors toujours possible de concevoir de nouveaux éléments distincts. On commencera par l'action consistant à ajouter un nouvel élément `e` assurement distinct des autres. Et il est possible d'ajouter une infinité de nouveaux éléments `e_1,e_2,e_3,...` `=` `(e_i)_(i in NN)` tous distincts et distinct de tous les autres, voir d'en ajouter une infinité encore plus grande `(e_i)_(i in RR)`. Mais faut-il pour cela d'abord définir `NN` et `RR` ?
L'algèbre dont l'origine historique vient du berceau des civilisations, de Babylone, 1800 av. J.C. peut constituer l'origine du langage mathématique et donc des mathématiques elle-mêmes. L'élément est conçu en même temps que l'algèbre qui propose une définition constructive des ensembles.
Néanmoins nous avons sauté une étape importante qui est celle de l'égalité propre aux éléments. Il existe des logiques aussi sophistiquées dans lesquelles l'égalité n'existe pas. Il convient dans ce cas là, de donner un autre nom aux éléments. On pourra parler d'individu car plus individuel et aussi indistinct dans son essence. l'IA propose de les appeler des structa (sructum au singulier) :
Dans ton contexte, Structum me paraît particulièrement fécond. On pourrait avoir une terminologie comme : Un structum est un objet du domaine d'une structure logique dépourvue d'égalité.
L'introduction de l'égalité permet ensuite de considérer les structa comme des éléments, en identifiant ceux qui sont substituables.Cela permettrait même le pluriel latin structa :
Le mot exprime bien une différence conceptuelle : un structum est quelque chose qui est là ou qui est construit, sans que la logique dispose encore du mécanisme permettant d'affirmer son identité avec autre chose.`x,y` sont des structa
La génèse ouvre une temporalité et met en premier lieu, l'action, celle de créer et de choisir. Une liste d'éléments est une succession de choix d'éléments, et donc, où le choix d'un élément dépend du choix des éléments précédents. S'il on veut s'affranchir de cette dépendance chronologique, on définit l'ensemble comme un choix simultanée de tous ses éléments.
De cette divergence nait deux visions de l'ensemble, l'une est dite cosmogonique basée sur la construction par récurrence (et par récurrence transfinie pour les ensembles infinis plus grand que `NN`), l'autre est dite cosmologique basé sur la logique du premier ordre.
La vision cosmogonique est capable de décrire une génèse. Tandis que la vision cosmologique part d'un état de fait, qu'est l'existence d'un monde mathématique, et déplace les processus de construction nécessaire sur le seul langage logique qui le décrit.
Une variable quantifiée universellement n'est pas limitée à appartenir à un ensemble. C'est cette différence, qui peut paraître infime, qui donne aux objets qui en sont issus, le caractère cosmologique, un caractère qui porte une multitude de paradoxes inhérents à l'évocation du tout sans limite. Cela justifie une dénomination distincte.
C'est pourquoi une fonction définie, non pas sur un ensemble de départ mais sur la catégorie de tous les éléments, est appelé un foncteur. Et on verra en quoi cette définition antique rejoint la définition moderne d'un foncteur.
De même une fonction caractéristique définie, non pas sur un ensemble de départ, mais sur la catégorie de tous les éléments, est appelé un prédicat.
La logique du premier ordre ne manipule qu'un seul type d'élément (d'où son nom), et ce type s'appelle la catégorie des éléments.
Le formalisme mathémamique est fondé par la logique. Et en logique classique il n'y a que deux valeurs de vérité le vrai et le faux. Il y a donc une première étape sans variable élémentaire, qu'est le langage propositionnel et son système de démonstration (le calcul des propositions ou comment résoudre un système d'équations booléennes) qu'il convient de décrire.
Le calcul des propositions se construire à travers une algèbre, faisant que l'algèbre dans son aspect purement mécanique est présente avant la logique. On parlera d'un système prélogique. Un moyen pédagogique de montrer cela sans trop d'effort, consiste à partir d'un langage logique minimaliste, puis à énumérer de façon exhaustive les règles de démonstration, d'en démontrer la complétude, puis d'étendre progressivement le langage logique.
La logique propositionnelle possède une version minimale, ne manipulant que l'élément `0` représentant le faux, et le connecteur d'implication `"→"`. Cela définit un langage et une algèbre `L= "<"0,"→"">"` que l'on compléte avec des variables. Les termes de ce langage utilisant par exemple deux inconnus `x,y`, noté `L[x,y]`, sont appelées des propositions, par exemple :
En logique classique, les connecteurs sont définis sur l'ensemble `{0,1}`, les variables sont booléennes, et l'implication `"→"` est définie comme suit :
`0"→"1=1`
`1"→"0=0`
`1"→"1=1`
On peut alors demander à l'IA quelles sont les règles de la déduction naturelle dans ce langage propositionnel réduit `L="<"0,"→"">"`. Toute la déduction naturelle tient en 4 mécanismes conceptuels :
Faire l'hypothèse d'une proposition `A` écrite dans le langage `L[x_1,x_2,...,x_n]` Si l'hypothèse `A` nous permet de démontrer `B`, alors cela démontre `A"→"B`.
Si on démontre `A`, et si on démontre `A"→"B` alors cela démontre `B`.
double négationSi on démontre `(A"→"0")→"0` alors cela démontre `A`.
Pour décrire concrètement ce mécanisme de raisonnement qui est prétendu exhaustif pour la logique propositionnelle, il convient de coder en pseudo code l'algorithme correspondant. On programme une procédure récurcive :
On se fixe d'abord une dimension `n`, c'est le nombre d'inconnus booléens que l'on veut mettre en jeux, `x_1,x_2,...,x_n`, et on part d'une base de connaisance vide, c'est l'ensemble `E` de toutes les propositions déjà démontrées. `E={}`.
La procédure prend comme argument cet ensemble `E`. Puis la procédure commence par prendre une hypothèse `A` qui est un terme quelconque du langage `L[x_1,x_2,x_3,...,x_n]` et qui est, de fait, ajouté dans l'ensemble `E` en cours. Puis 4 possibilités s'offrent à elle :
Cet procédure énumère des propositions tautologiques. Mais énumère-t-elle toutes les propositions tautologiques ? Autrement dit, est-t-elle complète ? C'est à dire, quelque soit une proposition `A`, énumère-t-elle toujours soit `A` ou soit `A"→"0` ?
Avant de répondre à cette question, on souhaite révéler le mécanisme de démonstration de l'algèbre par construction. Voyons les premières démonstrations que nous pouvons faire avec ce seul procédé.
| Supposons `A` Le contexte en cours est l'ensemble des propositions démontrées sous cette hypothèse qui est `E_1={A}` Nous choisissons la conclusion `A` pour clore cette hypothèse. On retourne le résultat `A"→"A` |
La démonstration peut se coder en utilisant un emboitement de crochets `[ ]` pour chaque hypothèse. Le premier membre du crochet est l'hypothèse (qui est un terme quelconque du langage). Les membres suivants sont des termes obtenus par modus ponens ou par suppression de la double négation de termes du contexte en cours (c'est à dire évoqués précédement dans la démonstration), ou bien sont d'autres démonstrations c'est à dire commençant par un crochet et une hypothèse. L'expression `[H,X,Y,Z]` où `H,X,Y,Z` sont des termes, signifie que `H` démontre par modus ponens et suppression de la double néfgation `X,Y,Z`, et qu'il faut donc ajouter au contexte en cours, une fois sortie de l'hypothèse, les propositions `H"→"X`, `H"→"Y`, `H"→"Z`
La démonstration de `A"→"A` se note simplement : `[A, A]`
Puis essayons de démontrer les schémas d'axiomes du calcul propositionnel de Hilbert :
| Supposons `A` Nous avons `E_1={A}` Supposons `B` Nous avons `E_2={B,A}` Nous choisissons `A` On retourne le résultat `B"→"A` Nous avons `E_1={B"→"A,A}` Nous choisissons `B"→"A` On retourne le résultat `A"→"(B"→"A)` |
| Supposons `A"→"(B"→"C)`, Nous avons `E_1={A"→"(B"→"C)}` Supposons `A"→"B` Nous avons `E_2={A"→"B, A"→"(B"→"C)}` Supposons `A` Nous avons `E_3={A, A"→"B, A"→"(B"→"C)}` Modus Ponens : `B` Modus Ponens : `B"→"C` Modus Ponens : `C` Nous avons `E_3={B, B"→"C, C, A, A"→"B, A"→"(B"→"C)}` Nous choisissons `C` On retourne le résultat `A"→"C` Nous avons `E_2={A"→"C, A"→"B, A"→"(B"→"C)}` Nous choisissons `A"→"C` On retourne le résultat `(A"→"B)"→"(A"→"C)` Nous avons `E_1={(A"→"B)"→"(A"→"C), A"→"(B"→"C)}` Nous choisissons `(A"→"B)"→"(A"→"C)` On retourne le résultat `(A"→"(B"→"C))"→"((A"→"B)"→"(A"→"C))` |
| Supposons `(A"→"0)"→"(B"→"0)` Nous avons `E_1={(A"→"0)"→"(B"→"0)}` Supposons `B` Nous avons `E_2={B, (A"→"0)"→"(B"→"0)}` Supposons `(A"→"0)` Nous avons `E_3={ (A"→"0), B, (A"→"0)"→"(B"→"0)}` Modus Ponens : `B"→"0` Modus Ponens : `0` Nous avons `E_3={B"→"0, 0, (A"→"0), B, (A"→"0)"→"(B"→"0)}` Nous choisissons `0` On retourne le résultat `(A"→"0)"→"0` Nous avons `E_2={(A"→"0)"→"0, B, (A"→"0)"→"(B"→"0)}` Suppression de la double négation : `A` Nous avons `E_2={A, (A"→"0)"→"0, B, (A"→"0)"→"(B"→"0)}` Nous choisissons `A` On retourne le résultat `B"→"A` Nous avons `E_1={B"→"A, (A"→"0)"→"(B"→"0)}` Nous choisissons `B"→"A` On retourne le résultat `(A"→"0)"→"(B"→"0)"→"(B"→"A)` |
Ainsi les démonstrations des schémas d'axiomes du calcul propositionnel de Hilbert sont :
Schéma d'axiome |
Démonstration |
`A"→"(B"→"A)` |
`[A,[B, A]]` |
`(A"→"(B"→"C))"→"((A"→"B)"→"(A"→"C))` |
`[A"→"(B"→"C), [A"→"B, [A, B, B"→"C,C]]]` |
`(A"→"0)"→"(B"→"0)"→"(B"→"A)` |
`[(A"→"0)"→"(B"→"0), [B, [A"→"0, B"→"0, 0], A]]` |
Notez que chaque terme dans la démonstration, en dehors des hypoyhèses qui sont les premiers termes des crochets, s'obtient en opérant un modus ponens sur deux termes évoqués précédement, ou en opérant une suppression de la double négation d'un terme évoqué précédement, sachant qu'une expresssion telle que par exemple `[H,X,Y,Z]` n'évoque pas les termes `X`, `Y`, `Z`, mais évoque les termes `H"→"X`, `H"→"Y`, `H"→"Z`