Une manière concrète de définir ce que sont les catégories, consiste à les construire par étapes d'abstraction successives à partir de la structure du langage même que nous utilisons.
On commence par la catégorie des algèbres de type fini c'est à dire engendrées par un nombre fini d'opérateurs, puis la catégorie des algèbres multi-sortes. C'est l'approche la plus simple des ensembles énumérables. Et on plonge toutes ces tructures algébriques de type fini dans une immense carrière qu'est l'algèbre libre engendrée par tous les opérateurs évoqués.
On formalise le langage logique multitype. Cela met en avant le mécanisme d'unification de termes qui est de complexité linéaire, et qui peut constituer l'opération fondamentale de tout raisonnement.
Le langage est la clé qui permet d'écrire le problème et de le résoudre, et ce n'est qu'un langage algébrique déclaratif c'est à dire munie d'opérateur spéciaux augmentant le langage algébrique en cours de route en créant de nouveaux opérateurs dans de nouveaux contextes. C'est une façon de présenter la logique d'une manière algébrique
Puis on complète ces algèbres avec une notion très générale de morphisme relationel entre algèbre, qui permet de définir la notion d'algèbres non-déterministes. La notion de relation à l'avantage d'être parfaitement symétrique contrairement à la notion de fonction.
Puis on procède à l'abstraction finale en ne retenant que les liens entre objets de la catégorie, pour définir la catégorie.
On construit un langage algébrique en présentant ses éléments générateurs et ses opérateurs générateurs entre crochet `"<...>"`. Chaque opérateur possède une arité. Elle est indiquée occasionnellement par le suffixe `(".")` pour unaire, `(".,.")` pour binaire, `(".,.,.")` pour ternaire. Exemple :
`L = "<"a,b,f("."), g(".,."),h(".,.,.")">"`
Les éléments générateurs sont considérés comme des opérateurs générateurs d'arité nulle. Le langage algébrique L est l'ensemble de toutes les compositions closes d'opérateurs générateurs :
`L = {a,b,f(a),f(b),g(a,a),g(a,b),f(f(a)),g(a,g(a,f(b))),...}`
De ce fait, le langage algébrique `L` constiture une structure libre.
Considérons une application `f` de `A` vers `B`. On note `A"→"B` l'ensemble des application de `A` vers `B`. Ainsi `f in (A"→"B)`, et il y a trois types `A`, `B`, `A"→"B` qui correspondent à trois ensembles.
L'inférence de type restreint le domaine des variables aux ensembles de départ déclarés des applications dont ils sont arguments et aux ensembles d'arrivé déclarés des applications dont ils sont le résultat. Par exemple considérons les déclarations suivantes :
`f in (A"→"B)`
`g in (C"×"D"→"E)`
Considérons une proposition écrite sous la contrainte de ces déclarations :
`AAxEEyAAz f(f(x))"="g(f(y),x)`
Celle-ci est identique à :
`AAx"∈"f^-1(A"∩"B)"∩"D, AAy "∈" f^-1(B"∩"C), f(f(x))"="g(f(y),x)`
Les variables peuvent être également contrainte d'appartenir à une structure `L`. Deux notation sont valables. On peut utiliser le nom du type (ici le nom de la structure `L`) pour désigner une variable appartenent à `L`. Mais celle-ci désignera à chacune de ses occurences une variable d'identité distincte, et toutes ses variables ne pourront éventuellement être quantifiés que d'une façon identique en un même bloque. Exemples :
On peut utiliser le nom du type (ici le nom d'une structure `A`) acollé avec un entier pour désigner une variable de type `A`. Ainsi, `n` variables appartenant à la structure `A` s'écrivent : `A1,A2,A3,...,An`
La variable vectorielle `vec x` désigne une séquence de `n` éléments `x_1,x_2,...,x_n`, qui peut être vide, et qui peut toujours s'ajouter comme dernier membre d'une séquence. Ainsi :
`(a,b,vecx) = (a,b,x_1,x_2,...,x_n)`
Entouré de parenthèse elle forme un vecteur ou une liste, `(vec x) = (x_1,x_2,...,x_n)`, et on laisse l'inférence de type déterminer `n`. Ainsi la propriété suivante affirme l'injectivité de chaque opérateurs structurels :
`AA lambda "∈""sign"(L) AAvecxAAvecy (lambda(vecx)"="lambda(vecy)) =>(vecx"="vecy)`
Le type de `vecx` n'est pas mentionné car l'inférence de type le détermine, `vec x` étant la séquence d'arguments d'une application de `L^n"→"L`, le vecteur `(vecx)` est de type `L^n`.
Par soucis de lisibilité, le symbole `vec" "` n'est que redondant dans le nom. Il précise que la variable qu'il chapotte est vectorielle faisant que `vec x` et `x` désigne la même variable qu'il convient toujours de chapotter par la flêche pour rappeler que c'est une variable vectorielle.
La variable vectorielle peut être typée. Etant donné une structure `L`, la variable vectorielle `vecL` désigne `n` variables appartenent à `L` mais de nom distincts, où l'inférence de type détermine `n`, et où chaque occurrence de `vecL` correspond à d'autres variables de noms toujours distincts, toutes ces variables n'étant éventuellement quantifiés que de façon identique en un même bloque.
La variable vectoriel peut être typé de façon plus individuelle en acollant la variable vectoriel avec un entier. Ainsi, 3 variables vectoriel de tailles pouvant être distinctes s'écrivent : `vec(L1)`, `vec(L2)`, `vec(L3)`
On fait une distinction entre les opérateurs générateurs engendrant un ensemble, et les opérateurs structurels définissant la signature d'une structure. La structure `L` muni de ces opérateurs structurels se note entre parenthèse en commençant par le nom de la structure :
`(L,a,b,f("."), g(".,."), h(".,.,."))`
La signature de la structure est :
`"sign"(L) = {a,b,f("."), g(".,."), h(".,.,.")}`
Le type de la structure est la liste les arités par ordre croissant :
`"type"(L) = (0,0,1,2,3)`
On appelle terme clos une composition d'opérateurs structurels. Exemple : `g(f(a),a)`
On appelle terme une composition d'opérateurs structurels et de variables. Exemple : `g(g(x,a),g(y,x))` où `x,y` sont des variables.
Une structure est dite complète si elle est engendrée par ses opérateurs structurels.
`L "complet" <=> "<@sign"(L)">" "=" L`
Où les crochet entourant une séquence d'objets se composant `"<"...">"` désigne la cloture par composition close, et où le symbole `"@"` défait l'ensemble pour insérer ses éléments dans une séquence.
Une structure complète est libre si et seulement chaque terme clos désigne un élément distinct. Ce qui revient à dire que les opérateurs structurels sont injectifs et que les opérateurs structurels ont des images disjointes.
La condition nécessaire et suffisante pour qu'une structure soit libre tient en trois points :
Cette troisième condition est difficile à transcrire dans le cas des structures incomplètes. Par contre, elle est vériifié de fait dans les structures complètes. Et... ne cherchant pas la difficulté, on ne traitera que des structures complètes.
Dans une structure `(L,a,b,f,g)` chaque terme désigne une application `n`-aire où `n` est le nombre de variables distinctes contenues dans le terme. Par exemple le terme `g(f(x),g(y,x))` désigne l'application `(x,y)|->g(f(x),g(y,x))` où les variables dans l'appel de l'appplication sont choisies selon leur première apparition lorsqu'on parcourt le terme de gauche à droite.
On note `Sigma_0(L,n)` l'ensemble de ces applications `n`-aire correspondantes aux termes de `L` avec `n` variables. Néanmoins, les variables ne sont pas encore typées. Elle peuvent donc désigner n'importe quoi. Et lorsque l'application n'est pas concrétisé c'est à dire n'a pas de définition spécifique, alors elle se comporte comme un opérateur générateur abstrait en retournant le terme d'appel non évalué et qui en constitue son évaluation. .
Un genre trés simple d'automate consiste en un ensemble de termes notés sous forme de production. Par exemple :
`A = {"⊢"a, (x,y)"⊢"g(x,f(y)), x"⊢"g(x,x)}`
Le principe de cet automate est simple, il possède un ensemble initialement vide de même nom que l'automate et qui accumule tout ce qu'il produit. La règle s'applique pour chaque variables de type voulu. Par défaut, le type des variables dans un automate est l'ensemble engendré par l'automate.
L'automate `A` énumère tous les termes clos par taille croissante dans un ordre précis selon l'algorithme classique (voir lien) :
`A |-- (a, g(a,a), g(a,f(a)), g(a,f(g(a,a))), ...)`
`A |-- (A(0),A(1),A(2),...)`
L'automate est donc aussi une fonction de `NN` vers `L` dont l'image est l'ensemble `A` final.
L'automate d'une structure est sa signature où les opérateurs sont notés sous forme de production. L'automate de `(L,a,b,f,g)` est `{"⊢"a, "⊢"b, x"⊢"f(x), (x,y)"⊢"g(x,y)}`.
Les variables peuvent appartenir d'une manière récurcive à l'ensemble énuméré par l'automate lui-même (type par défaut). Et elles peuvent appartenir à d'autres structures et à d'autres ensembles énumérés par des automates. On note ces variables en acollant le nom du type avec un entier. Ainsi `n` variables appartenant à la structure `L` s'écrivent : `L1,L2,L3,...,Ln`, et trois variables de l'automate `A` s'écrivent `A1,A2,A3`. On peut aussi utiliser le nom du type (ici le nom de la structure `L`) seul pour désigner une variable appartenent à `L` mais où chaque occurence de `L` correspondra une variable d'identité distincte.
Ne considérant que des structures complètes, ce qui simplifie grandement la structure sans restreindre la diversité des algèbres, l'ensemble sous-jacent d'une structure correspond à l'ensemble énuméré par son automate.
Considérons deux ensembles `A, B`. On note le cardinal de l'ensemble `A` simplement par l'expression `|A|`.
`|Ø| = 0`
`|{a}| = 1`
L'ensemble des applications de `A` vers `B` se note de deux façons possibles :
`(A"→"B) = B^A`
Lorsque `A` et `B` sont de cardinalité finie, nous avons : `|A"→"B| = |B|^|A|`
On note l'ensemble `n = {0,1,2,3,...,n"-"1}`. L'ensemble des parties de l'ensemble `A` correspond à l'ensemble des applications de `A` sur `2`, chaque partie correspondant au noyaux (l'image inverse de `0`) de chaque application.
C'est pourquoi l'ensemble des parties de `A` est noté `2^A` ou `A"→"2`.
Etant donné une application `f in (A->B)` et étant donné un élément `a in A`, on note l'élément image de `a` par l'application `f` simplement par l'expresion `f(a)`. On utilise une seconde notation d'appel avec des chevrons à la place des parenthèses pour appliquer `f` à un ensemble. Etant donnée une partie `E` de `A` c'est à dire `E in 2^A` nous avons :
`f〈E〉 = {f(x) | x in E}`
L'image de `f` se note alors simplement par `f〈A〉`. Les chevrons attendent un argument ensemble, c'est pourquoi pour éviter toute ambiguité la notation des variables typées anonymes ne s'applique pas ici.
Une relation `R` de `A` vers `B` est une partie de `A"×"B`.
On note `aRb` pour indiquer qu'un arc de la relation `R` part de `a` pour aller sur `b`. La relation `R` est aussi une application de `2^A` vers `2^B`. D'où les trois notations équivalentes suivantes :
`aRb`
`(a,b) in R`
`b in R〈{a}〉`
Cela à pour conséquence, qu'après la déclaration suivante :
`R ∈ 2^(A"×"B)`
Ou après la déclaration plus simple suivante :
`R sube (A"×"B)`
L'expression `R〈x〉` impose que la variable `x` est de type `2^A`.
Lorsque les ensembles sont finis, le lien entre `2^(A"×"B)` qui est l'ensemble des relations de `A` vers `B`, et `2^A"→"2^B` qui est l'ensemble des applications de `2^A` vers `2^B`, ce lien devient une bijection si et seulement si on se restreint au seules applications de `2^A` vers `2^B` vérifiant :
`R〈Ø〉=Ø`
`AAxAAy R〈x"∪"y〉=R〈x〉"∪"R〈y〉`
Lorsque les ensembles sont infinis, les égalités doient également être valables pour les unions infinies. La propriété se réécrit comme suit :
`AAX, R〈uuu_(p in X) p 〉 = uuu_(p in X) R〈p〉`
De même pour les relations ternaires. Une relation `R` de `A"×"B` vers `C` est une partie de `A"×"B"×C"` et c'est aussi une application de `2^(A×B)"→"2^C` vérifiant dans le cas fini :
`R〈Ø,x〉=Ø`
`R〈x,Ø〉=Ø`
`AAxAAy R〈x"∪"y,z〉=R〈x,z〉"∪"R〈y,z〉`
`AAxAAy R〈x,y"∪"z〉=R〈x,y〉"∪"R〈x,z〉`
Et vérifiant dans le cas infini :
`AAxAAy, R〈uuu_(p in x) p, y〉 = uuu_(p in x) R〈p,y〉`
`AAxAAy, R〈x, uuu_(p in y) p〉 = uuu_(p in y) R〈y,p〉`
Ou en regroupant les composantes de `A"×"B` :
`AAx, R〈uuu_(p in x) p〉 = uuu_(p in x) R〈p〉`
Pour atteindre la plaine puissance d'un langage logique dit du premier ordre, il faut introduire la déclaration de variables d'un unique type, quantifiées soient universellement `"∩"` ou existenciellement `"∪"`, et qui correspondra dans une algèbre à l'intersection ou la réunion des images.
On adopte la notation ensembliste qui fait que pour tout application `f` partant de `L`, nous avons `f〈{a}〉 = {f(a)}` et que `f〈L〉` égale l'image de `f`. Les variables `x` sont de type `2^L`, autrement dit `x sube L`.
Les quantificateurs sont définis comme suit :
`("∪"x, f 〈x〉) = uuu_(x sube L) f〈x〉`
`("∩"x, f〈x〉) = nnn_(x sube L) f〈x〉`
Les termes de ce langage étendu sont appelés des formules. Les formules closes n'ont pas de variable libre, et désigne une combinaison d'unions et d'intersections d'images d'opérateurs structurels. Ainsi nous avons :
`("∪"x, f〈x〉) = f〈L〉`
Puis si l'application `f` n'est pas constante, nous avons :
`("∩"x, f〈x〉) = Ø`
Puis si l'application `f` s'évalue comme suit `f = (x |-> c)`, alors nous avons :
`("∩"x, f〈x〉) = {c}`
Les formules de la structure `L` ont alors comme valeur de vérité un ensemble, et le faux correspond à l'ensemble vide.
Dans cette approche constructive on définit les opérateurs du langage logique multi-type dans un ordre presque naturel constituant, de fait, une génèse.
On part de l'élément qui, dans son principe, peut constituer tout chose identifiable. Son utilité est justement de servir d'identifiant. C'est pourquoi l'absence de typage correspond par defaut au type élément. C'est le type parent de tous les types, te type le plus générale qui englobe tout.
(En cela, on ne va pas s'entendre avec les théories NBG et MK pour lesquels une classe ne peut pas être un élément.)
La première construction qui vient naturellement après le concept d'élément est la dispositions d'éléments qui, dans sa seule plus grande liberté, est la liste finie que l'on représente par l'énumération de ses éléments `(x_1,x_2,x_3,...,x_n)`. Mais si on continue dans cette voie, on sort du cadre classique qui pose l'ensemble des éléments concernées avant leur éventuelle disposition. Dans le cas classique, la liste de `n` éléments correspond alors à `n` choix successifs d'éléments d'un ensemble préalablement déclaré.
La première catégorie évoquée est celle des ensembles notées `"Conjuto"`, qui n'est pas un ensemble à cause du paradoxe de Russel "Les ensembles ne se contenant pas se contient-t-il ?" Comme on ne peut pas l'appeler un ensemble, on l'appelle une catégorie. La propriété `A "∈""Conjuto"` diffère de la signification habituelle. Mais c'est toujours une spécification de type. Cela précise que la variable `A` est un ensemble.
On pourrait dire que la propriété des ensembles, c'est soit d'être vide ou de contenir des éléments tous distincts. Mais qu'est ce que veut dire "être contenu". La catégorie des ensembles est munie d'un prédicat binaire `"∈"` qu'est le lien d'appartenance, définie par sa théorie. Les objets de la catégories satisfont une théorie du premier ordre mais la categorie elle-même, non.
Mais là encore, si on continue dans cette voie, on sort du cadre classique qui pose toujours un ensemble circonscrivant tous les éléments concernées. La structure des ensembles correspond alors à un ensemble `Omega` que l'on agrandit autant que nécessaire mais en restant toujours un ensemble, munie d'une relation binaires `"∈"` satisfaisant un certain nombre de propriété appelé théorie des ensembles.
Pour définir cette relation d'appartenance, on prend la théorie de Zermelo–Fraenkel à laquelle on ajoute l'axiome du choix pour pouvoir traiter les infinies.
Puis accessoirement, on remplacera l'axiome de fondation par un schéma d'axiomes beaucoup plus intéressant, rendant égaux des ensembles définis récurcivement de la même manière.
L'introduction du prédicat binaire `"∈"` s'accompagne de la théorie ZFC (Zermelo–Fraenkel + Axiome du Choix)
Le langage logique `L` comprend un prédicat binaire `"∈"`, l'égalité `"="`, les connecteurs booléens `0`, `1`, `"¬"`, `"∧"`, `"∨"`, `"→"` `"↔"`, les varaiables booléennes `x_1,x_2,x_3,...x_n` quantifiées `AA` ou `EE`.
Une formule `varphi` du langage `L` est identifié à une application propositionnelle `n`-aire où les `n` variables libre (c'est à dire non quantifiées) sont disposées dans l'appel de l'application dans l'ordre de leur première apparition lorsqu'on parcours la formule de gauche à droite. Par exemple la formule `AAxEEy,` `x "∈" y => z "∈" x` correspond à l'application `z |-> (AAxEEy,` `x "∈" y => z "∈" x)`
L'ensemble des formule `n`-aire du premier ordre se note `Sigma(L,n)`
Les expressions du genre `((P),(Q))` signifie `P "et" Q`
On définie le quantificateur d'un élément unique pour chaque formule unaire `varphi` comme suit :
`EE!x varphi(x) <=> ((EEx varphi(x)),(AAyAAy ((varphi(x)),(varphi(y))) => x"="y))`
Axiomes :
Extensionalité |
`AA A AA B‚(AAx‚x"∈"A <=> x"∈"B) => A"="B` |
Paire |
`AAa AAb EEp AAx‚x"∈"p <=> ((x"="a),(x"="b))` |
Réunion |
`AAE EER AAx‚x"∈"R <=> EEp‚((x"∈"p),(p"∈"E))` |
Puissance |
`AA EE∃P AAA‚A"∈"P <=> AAx‚x"∈"A => x"∈"E` |
Infini |
`EEX‚((Ø"∈"X),(AAx‚x"∈"X => EEz‚((z"∈"X),(AAt‚t"∈"z <=>(t"="x "ou" t"∈"x )))))` |
Choix |
`AAX‚(AAy‚y"∈"X=>y"≠"Ø) => EECAAy‚y"∈"X=> EE!z‚((z"∈"y),(z"∈"C))` |
Schéma d'axiomes :
Séparation |
`AAφ(".") "∈" Sigma(L,1)‚AAxEEyAz‚z"∈"y <=> ((z "∈" x),(varphi(z)))` |
Remplacement |
`AAφ(".,.") "∈" Sigma(L,2)‚AAXEEYAAy‚y"∈"Y<=>EEx,((x"∈"X),(φ(x,y)))` |
Le langage a été construit ici en vue de trouver les axiomes les plus faibles (pour être indépendants) nécessaire à la théorie des ensembles, et n'utilisant que la relation `"∈"`. Or cela n'est pas du tout notre approche. Il convient de trouver les propriétés les plus fortes même si elles ne sont pas indépendantes, pour proposer l'écriture la plus pratique.
Pour la paire, on définit l'usage des braquettes `{x_1,x_2,...,x_n}` et pour les cas infini `uuu_(i in I) {x_i}` avec l'application `(i |-> x_i)`. Pour la réunion on utilise `uuu_(x in X) x`. Pour la puissance, l'ensemble des partie on utilise `uuu_(x sub X) {x}`
On remplacera l'axiome de fondation par un schéma d'axiomes rendant égaux des ensembles définie récursivement de la même manière.
Considérons deux ensembles `e_1,e_2` chacun contenant uniquement lui-même :
`AAx, x"∈"e_1 <=> x"="e_1`
`AAx, x"∈"e_2 <=> x"="e_2`
En quoi `e_1` et `e_2` sont-ils différent ? En rien, le nom des variables ne constitue pas une information car les variables peuvent être renommées toujours de façon distincte sans que cela de change le sens de la formule, c-à-d sans que cela ne change sa sémantque. On peut donc vouloir augmenter l'axiome d'extensionalité afin que dans une telle situation, nous puissions déduire que `e_1"="e_2`, autrement dit, qu'il existe un unique ensemble qui contient exactement un élément qui est lui-même. L'axiome d'extentionalité devient :
`AAx, x in (A <=>x in B) => A=B`
`((A={A}uuX),(B={B}uuX)) => A=B`
Le principe dit que le nom utilisé pour définir l'ensemble, ne fait pas partie de la définition, et donc n'apportant accune information il peut être changé. Si ce nom est utilisé dans la définition elle-même, une définition dés lors récurcive, il faut prendre en compte que ce nom est relatif. Et cela s'applique aux définitions multiples. Par exemple si on définit `A` et `X` en posant :
`A = {X,a,b}`
`X = {A,c}`
Les noms `A` et `X` n'apporte, par principe d'une définition, aucune information. Et donc si on définit `B` et `Y` en posant :
`B = {Y,a,b}`
`Y = {B,c}`
Les noms `B` et `Y` n'apporte également aucune information, on en déduit que `A"="B` et `X"="Y`.
La généralisation de ce principe au graphe non-ordonné que représente les ensembles pouvant se contenir nous amène au concept de morphisme d'ensemble, une application qui respecte ce lien d'étre contenue soit directement ou soit indirectement.
Un ensemble, étant identifé par son seul contenue, n'est pas un identifiant. Omega munie de la relation d'appartenance forme un graphe non-ordonnée où chaque noeud du graphe correspond à un ensemble ou à un élément qui n'est pas un ensemble.
(Elemento×Elemento->Conjuto)