Pour interpréter correctement ce que signifie une succession de quantifications telle que `AAxEEy`, il convient d'étudier l'équivalence de Skolem ainsi que sa contraposée appelée l'équivalence de Herbrand. Et deux cas sont à envisager ; soit la proposition est à support fini, ou soit elle ne l'est pas. On dit qu'une proposition est à support fini si les éléments évoqués par ses quantificateurs peuvent être circonscrits à un ensemble fini.
Par exemple considérons la proposition `AAx EEy, P(x,y)` où `P` est un prédicat binaire. Elle signifie littéralement « Quelque soit `x` il existe `y` tel que `P(x,y)` ». La proposition est du premier ordre. Il n'y a qu'un seul type de variable, que l'on représente par l'ensemble `E` appelé l'ensemble support de la proposition. Si cet ensemble est fini l'équivalence de Skolem est valide :
Et sa contraposé, l'équivalence de Herbrand, est donc valide aussi :
Cela est valable pour tout type d'opérateur ou de prédicat. Considérons un élément `x` de type `X`, un élément `y` de type `Y`, et une fonction propositionnelle `P"(.,.)"` de type `X"→"Y"→"{0,1}`. Si la proposition est à support fini, c'est à dire si `X` et `Y` sont des ensembles finis, alors l'équivalence de Skolem est valide, et s'écrit comme suit :
Et sa contraposé, l'équivalence de Herbrand, est donc valide aussi :
On note le type de la variable quantifiée en exposant.
Les mathématiques sont une science expérimentale. Le langage mathématique qui sert à écrire les propositions, sert également à construire les mondes finis qui les satisfont ou les récusent. Et la difficulté epistémologique qui apparaît avec l'infini doit être ramené à sa juste mesure sachant que le consensus sur la cosmologie tend à nier l'existence d'infini physique.
Étant donné une proposition `P` en logique classique et un monde fini `M`, chacun pourra constater de lui-même, qu'après avoir exploré toute les facettes du monde fini `M`, invoquées par la proposition `P`, que l'une ou l'autre alternative se réalise obligatoirement :
`P "⊨" M" ou "P "⊭" M`
C'est le principe du tiers fini exclus, une constatation empirique pour les mondes de petite taille, puis démontré par récurrence pour les mondes et propositions de taille quelconque, valable pour tout les mondes finis et propositions également finies. Il convient, de la même façon qu'une proposition est par défaut de taille fini, de considérer qu'un monde est par défaut fini, et faire du monde infini l'exception.
---- 24 janvier 2021 ----
Toute théorie admet une forme prénexe skolémizée où tous les quantificateurs existentiels sont placés en premier, et admet une forme prénexe herbrandisée où tous les quantificateurs universels sont placés en premier.
Si la théorie est à support fini, alors ces deux équivalences sont exactes. Mais dans le cas général et selon le paradigme élémentarien où tout est dénombrable, l'équivalence n'est pas tout à fait exacte.
Les mêmes notations sont utilisée, seul le paradigme change. Ainsi l'ensemble dénombrable `(E"→"Y)` désigne l'ensemble des applications calculables de `E` vers `Y`. C'est à dire l'ensemble des programmes de calcul de taille finie prenant en entrée un élément de `E` et retournant en sortie un élément de `Y`.
La forme skolémisée est un chouia plus forte, car elle stipule que les fonctions existentielles évoquées sont calculables. L'expression `EEx^(E"→"Y)` signifie qu'il existe un programme de calcul de taille finie prenant en entrée un élément de `E` et retournant en sortie un élément de `Y`.
La forme herbrandisée est un chouia plus faible, car elle stipule que les fonctions universelles évoquées sont calculables. L'expression `AAy^(E"→"Y)` signifie quelque soit un programme de calcul de taille finie prenant en entrée un élément de `E` et retournant en sortie un élément de `Y`.
Remarquez que `E` et `Y` ainsi que tous les ensembles définissables avec ce langage logique sont donc, par principe élémentarien, des ensembles dénombrables.
La logique respectueuse de l'indépendance (RI), de terme anglophone « Logical Independence-Friendly » (IF), est une extension de la logique standart du premier ordre, qui a été conçue en 1989 par Jaakko Hintikka, logicien et philosophe finlandais (1929 Vantaa - 2015 Porvoo) et Gabriel Sandu, logicien et philosophe finlandais, professeur de philosophie théorétique à l'université de Helsinki.
On décrit cette logique, selon le paradigme élémentarien. L'ensemble support est donc posé dénombrable. La proposition `AAx, P(x)` est equivalente à la conjonction série suivante :
`P(a_1) ^^ P(a_2) ^^ P(a_3) ^^...`
où `(a_i)_(i in sfN)` est une suite d'éléments qui couvre l'ensemble support `E`. Autrement dit, nous avons :
`AAx, P(x) <=> ^^^_(x in E) P(x)`
Pareillement, la proposition `EEx, P(x)` est equivalente à la disjonction série suivante :
`P(a_1) vv P(a_2) vv P(a_3) vv...`
où `(a_i)_(i in sfN)` est une suite d'éléments qui couvre l'ensemble support `E`. Autrement dit, nous avons :
`EEx, P(x) <=> vvv_(x in E) P(x)`
La notion d'indépendance peut alors se formaliser comme suit. Quand les variables sont quantifiées de la même sorte, la quantification porte alors sur un couple de variables, et il n'y a pas lieu de se poser la question d'une dépendance ou d'une indépendance entre ces deux variables. Par contre, lorsque une variable `x` est quantifiée universellement, et une variable `y` est quantifiée existentiellement, alors 3 situations peuvent se produirent, soit l'une dépend de l'autre, ce qui se note dans l'ordre des dépendances, ce qui introduit une temporalité dans la notation, ou bien les variables sont indépendantes ce qui se note en vecteur :
`AAxEEy,P(x,y)`
`EEyAAx,P(x,y)`
`[(AAx),(EEy)],P(x,y)`
Les quantifications sont misent en vecteur pour indiquer qu'elles ne s'imbriquent pas, et elles définissent donc des variables indépendantes. C'est la notation intemporelle. Et nous avons :
`EEyAAx,P(x,y) => [(AAx),(EEy)],P(x,y) => AAxEEy,P(x,y)`
Prenons par exemple l'ensemble support `E"="{0,1}`. Le nombre de mondes possibles est `ccP(E"×"E) = 2^4 = 16`. Les mondes satisfaisant
`EEyAAx,P(x,y)` `[(AAx),(EEy)],P(x,y)` `AAxEEy,P(x,y)`
L'indépence d'un connecteur "ou" vis-à-vis d'une variable quantifiée universellement.
L'indépence d'un connecteur "et" vis-à-vis d'une variable quantifiée existantiellement.
Dans la proposition `AAxEEy,P(x,y)`, la variable `y` dépend de `x`. À chaque valeur de `x` il existe au moins une valeur de `y` satisfaisant `P(x,y)`. On explicite cette dépendance par un lien fonctionnelle non nécessairement calculable `y(x)` :
`AAxEEy,P(x,y) <=> [(AAx),(EEy("."))], P(x,y(x))`
Ainsi `y` est dépendant de `x`. Et `y(".")` n'est pas dépendant de `x`. Noter que les éléments `x` et `y` appartiennent à l'ensemble support `E`, tandis que l'élément `y(".")` appartient à l'ensemble des applications non nécessairement calculables de `E` vers `E`. Par contraposé et en posant `AAaAAb, Q(a,b)=¬P(a,b)`, nous avons :
`EExAAy,Q(x,y) <=> [(EEx),(AAy("."))], Q(x,y(x))`
Dans le sens inverse, cela est moins intuitif, c'est pourquoi on passe par la négation, et on constate la même règle. D'une manière générale, une variable quantifié `EE` sera dépendante de toutes les variables quantifiées `AA` appartaissant antérieurement dans la proposition prénexe. et réciproquement, une variable quantifié `AA` sera dépendante de toutes les variables quantifiées `EE` appartaissant antérieurement dans la proposition prénexe. Par exemple :
`AAxEEyAAzEEt,P(x,y,z,t) <=> [(AAx),(EEy(".")),(AAz(".")),(EEt"(.,.)")], P(x,y(x),z(y),t(x,z(y)))`
Noter que l'éléments `x` appartient à l'ensemble support `E`, tandis que les éléments `y(".")` et `z(".")` appartiennent à l'ensemble des applications non nécessairement calculables de `E` vers `E`, et `t"(.,.)"` appartiennent à l'ensemble des applications non nécessairement calculables de `E"×"E` vers `E`.
On utilise soit les quantificateurs de Henkin explicitant les indépedances, ou soit une notation inverse explicitant les dépendances.
---- 22 janvier 2021 ----
Par exemple considérons la proposition `EExAAyEEz, P(x,y,z)`
Par exemple, considérons la proposition `P` suivante : Quelque soit `x`, il existe `u`, quelque soit `y`, il existe `v` indépendant de `x`, tel que `R(x,y,z,t)`.
Notation utilisant les quantificateurs de Henkin Notation explicitant les dépendances implicite `AAEE` Forme skolèmisée `EEu"(.)" EEv"(.)" AAx AAy, P(x,u(x),y,v(y))` Négation de la forme skolèmisée
Notation utilisant les quantificateurs de Henkin Notation explicitant les dépendances implicite `EEAA` Forme herbrandisée `AAx AAy(u) EEu EEv, P(x,u,y(u),v)` Négation de la forme skolèmisée
On prend la négation de P :
Notation utilisant les quantificateurs de Henkin Notation explicitant les dépendances implicite Forme skolèmisée `EEu"(.)" EEv"(.)" AAx AAy, P(x,u(x),y,v(y))` Négation de la forme skolèmisée
La logique RI du premier ordre étend la logique classique du premier ordre, sans atteindre complètement la logique du second ordre.
L'équipotence de deux ensembles `A` et `B` est définie par :
`AAxAAy(EEtta"/"AAx)(EEttb"/"AAy), (((x "∈" A) => (ttb"∈"B)),((y"∈"B)=>(tta"∈"A)),((ttb"="y)<=>(tta"="x)))`
Ce qui signifie littéralement « Quelques soit `x`,`y`, il existe `a` indépendant de `x`, et il existe `b` indépendant de `y` tels que si `x` appartient à `A` alors `b` appartient à `B`, et si `y` appartient à `B` alors `a` appartient à `A`, et si `b"="y` alors `a"="x` », et si `a"="x` alors `b"="y` ». Néanmoins, c'est bien la forme skolémisée qui nous sera la plus familière :
La forme skolémisée est :
`EEf"(.)"EEg"(.)"AAxAAy, (((x "∈" A) => (f(x)"∈"B)),((y"∈"B)=>(g(y)"∈"A)),((f(x)"="y)<=>(g(y)"="x)))`
Ce qui signifie littéralement « Il existe deux applications `f` et `g` telles que quelques soit `x,y`, si `x` appartient `A` alors `f(x)` appartient à `B`, et si `y` appartient `B` alors `g(y)` appartient à `A`, et si `f(x)"="y` alors `g(y)"="x`, et si `g(y)"="x` alors `f(x)"="y` ». Autrement dit, il existe une application de `A"→"B` et une application de `B"→"A`, qui sont inverses l'une de l'autre.
La forme herbrandisée est :
---- 20 janvier 2021 ----
L'infinitude d'un ensemble `A` est défini par :
`EEttcAAxAAy(EEtta"/"AAy)(EEttb"/"AAx), ((ttc"∈" A),(tta"≠"ttc),((x "∈" A) => (tta"∈"A)),((tta"="ttb)=>(x"="y)))`
La forme skolèmisée est :
`EEttcEEf"(.)"AAxAAy, ((ttc"∈" A),(f(x)"≠"ttc),((x "∈" A) => (f(x)"∈"A)),((f(x)"="f(y))=>(x"="y)))`
Ce qui signifie littéralement « Il existe un élément `c` appartenant à `A`, et il existe une applications `f` telles que quelques soit `x,y`, on a `f(x)"≠"ttc`, et si `x` appartient `A` alors `f(x)` appartient à `A`, et si `f(x)"="f(y)` alors `x"="y`. Autrement dit, il existe un élément `c` de `A`, et il existe une injection de `A"↪"A"-"{c}`.
---- 20 janvier 2021 ----
Étant donné un ensemble quelconque `A`, il existe un lien biunivoque canonique entre l'ensemble des applications `A"→"{0,1}` et l'ensemble des parties `ccP(A)`. La bijection que l'on choisit pour mettre en évidence ce lien, transforme toute application `f` de `A"→"{0,1}` en la partie `F"="f^-1({1})`. L'application est appelée la fonction caractéristique de `F`. La bijection inverse transforme toute partie `F` incluse dans `A` en l'application de graphe `{x "↦" (x "∈" F) "/" x "∈"A}`. En résumé :
Noté que l'expression `(x "∈" F)` est convertie en une valeur booléenne ; `0` si `x` n'appartient pas à `F`, et `1` si `x` appartient à `F`.
Une application `f` possède un ensemble de départ noté `"Dép"(f)` et un ensemble d'arrivé noté `"Arr"(f)`. L'application `f` appartient à l'ensemble des applications `"Dép"(f)"→""Arr"(f)`, et appliqué à un élément `x` elle retourne son image `f(x)`.
Ce lien biunivoque canonique va nous donner l'occasion de présenter le choix d'un langage formel typé. On va utiliser le même symbole pour désigner des objects différents et de type différent. Et c'est le type qui déterminera complètement l'objet. On implémente la notation étendue aux ensembles de cette façon, en différenciant des types et en overloadant des opérateurs. À partir du type `A"→"B`, on crée le type `ccP(A)"→"ccP(B)`. Et un symbole `f` pourra être interprété comme étant l'un de ces deux types. Ainsi `"Dép"(f)` pourra être égale à `A` ou bien être égale `ccP(A)` et c'est le type qui le déterminera. L'opérateur d'application est overloadé en conséquence en créant un nouveau comportement. L'application de `f` sur une partie `X` incluse dans `A` retourne l'ensemble des image des éléments de X , noté `f(X)` et appelé l'image de `X`. L'opérateur d'inversion est overloadé en conséquence. L'application de `f^-1` sur une partie `Y` incluse dans `B` retourne l'ensemble des prédécesseurs d'au moins un éléments de `Y` :
`f(X) = {f(x) "/" x "∈" X}`
`f^-1(Y) = {x "/" f(x) "∈" Y}`
Notez que le comportement de `f` ainsi décrit est celui d'une relation de `A` vers `B`. Si l'application possède le type « bijection » alors l'opérateur d'inversion est overloadé ici en créant un nouveau comportement, c'est à dire qu'il possède cet autre définition si l'objet sur lequel il s'applique possède le type « bijection ». Dans ce cas `f^-1` peut être également une application de `"Arr"(f)"→""Dép"(f)` qui lorsqu'on l'applique sur un élément `x` retrourne l'antécédent de `x`.
L'expression `f(x)` apparaissant dans une proposition entraine des contraintes de typage sur `x` et sur `f`. Elle impose que `f` est une application et que `x` appartient à l'ensemble de départ de `f` ou bien que `f` possède un ensemble de départ contenant `x`. Et, tenant compte de la notation étendu, il faut ajouter les autres solutions de typages. A savoir le cas où`x` est une partie l'ensemble de départ de `f` ou bien que `f` possède un ensemble de départ contenant la partie `x`. Puis la règle peut s'appliquer plusieurs fois, faisant qu'il est possible d'appliquer `f` à une famille, faisant de `f` une application de `ccP(ccP(A))->ccP(ccP(B))` qui appliquée à une famille va retourner la famille des images, et qui sera appelé la famille image.
`f(bbbX) = {f(X) "/" X "∈" bbbX}`
`f^-1(bbbY) = {X "/" f(X)"∈"bbbY}`
Une surjection peut être désignée par l'ensemble de ses arcs. Cela signifie qu'une conversion implicite s'opère lorsque une variable de type surjection est unifiée avec une variable de type ensemble de couples :
`f = {x"↦"f(x)}`
Notez que dans l'expression de cet ensemble de couples, il n'est pas nécessaire de préciser que `x` appartient à l'ensemble de départ de `f`, car l'expression `f(x)` sous-entend que `x"∈Dép"(f)`, ni de circonscrire le résulat à un ensemble d'arrivé puisque dans le cas d'une surjection l'ensemble d'arrivé est l'ensemble image.
L'ensemble support d'une proposition du premier ordre circonscrit l'ensemble des éléments concernés, ce qui permet par la suite d'omettre de préciser à quoi appartiennent les éléments. Mais des sous-types peuvent être déclarés, et des opértateurs peuvent être overloadés pour ces sous-types. Une proposition peut alors avoir plusieurs significations, une signification pour chaque typage possible, et si le contexte n'en exclut aucun, la proposition s'affirme être vrai pour tous ses typages possibles.
---- 24 janvier 2021 ----
Lorsque l'on explore les ensembles infinis, la théorie des ensembles devient vite incapable de répondre à de nombreuses questions à cause de son inhérente incomplétude. Délors, on la complète de différentes façons. C'est pourquoi il existe une multitude de théories des ensembles toutes autant cohérentes les une que les autres, autant que l'arithmétique peut l'être. Le choix de la théorie des ensembles détermine la signification profonde de ce qu'est un ensemble infini, et même, ce qu'est un ensemble, dans ses éventuelles définitions récurcives. Il s'agit donc avant tout d'un choix politique.
Avec les seuls axiomes minimaux communément admis, il n'est pas possible de démontrer que les cardinaux sont toujours comparables. C'est à dire, étant donné deux ensembles `A` et `B`. On ne peut pas démontrer qu'il existe toujours, soit au moins une injection de `A` dans `B`, ou au moins une injection de `B` dans `A`, simplement par faute de moyen de construction et de définition.
Se peut-il qu'il existe deux ensembles `A` et `B` tels que :
`(A"↪"B)=Ø`
`(B"↪"A)=Ø`
Dans certaine théorie des ensembles cette propriété est démontrable, dans d'autres elle est indécidable, et dans d'autre encore sa négation est démontrable.
En physique, on est amené à concevoir des grandeurs infiniment petites et des grandeurs infiniment grandes de différents ordres qui complètent ainsi l'ensemble des grandeurs. Comment donner un sens mathématique exacte à ces notions d'infini qui sont toujours comparables deux à deux, sans risquer de se mettre des oeillères ? On scinde le problème en deux, l'infiniment petit et l'infiniment grand. Et on commence par rechercher les infiniments grands entiers sous forme d'une catégorie.
On cherche donc à construire une catégorie des grandeurs entières pouvant être infinies et au delà c'est à dire transfinies. Elles sera appelée la catégorie des ordinaux. Et on souhaite que cette catégorie obéisse à 3 règles :
Et il y a plusieurs voix de recherche possibles. Soit on reste dans la théorie des ensembles et on cherche par le haut en tâtonnant, une catégorie d'ensembles ayant ces 3 propriétés. Soit on se détache de la théorie des ensembles, et on utilise la seul logique pour construire par le bas une structure des ordinaux. Puis il y a les puristes qui définissent les structures à la lettre, selon le sens de notre langue, sans se préoccuper de savoir si la structure résultat possède des propriétés intéresssantes ou pas.
Méthode par le haut :
Les caractèristiques des ensembles que nous allons retenir vont déterminer le comportement de leur catégorie. Classiquement, on choisie comme représentation des ordinaux, les ensembles bien ordonnées, c'est à dire des ensembles munie d'une relation d'ordre totale et tel que tout sous-ensemble non vide possède un élément minimal. Cette condition est quand même extrêmement forte !. C'est pourquoi, il est certainement possible de définir des ordinaux plus généraux, avec une condition plus faible que celle du bon ordre.
Méthode par le bas :
On considère une structure possédant ces trois propriétées :
`S = ("<"0, s"(.)>", ⩽ )" / "{`
`"⩽ est une relation d'ordre totale",`
`0 " est minimal pour ⩽" ,`
`s " est l'opérateur successeur direct pour ⩽"`
`}`
Cette structure libre représente les entiers naturels, mais muni seulement d'une relation d'ordre totale `⩽` , d'un plus petit élément `0`, et d'un opérateur successeur direct `s"(.)"`. Et on s'intéresse à toutes les extensions élémentaires qu'il est possible de faire sur cette structure.
Définition des puristes :
Il existe une autre définition des ordinaux plus terre-à-terre, dites idiomatiques, qu'est la catégorie des ensembles totalement ordonnées possèdant un élément minimum et un opérateur successeur direct définie partout sauf pour l'éventuel élément maximum. Autrement dit, un ordinal idiomatique est un ensemble totalement ordonné avec un élément minimum et un opérateur successeur direct définie partout sauf pour l'éventuel élément maximum, à isomorphime près, c'est à dire à bijection près respectant l'ordre, l'élément minimal, l'éventuel élément maximum, et l'opérateur successeur directe. Mais avec cette définition, il n'est pas garantie que les ordinaux soient tous comparables.
L'ensemble des parties non vides de `E` est noté `ccP_(">"0)(E)`.
Un ensemble bien ordonné est un ensemble `E` munie d'une relation d'ordre totale `"⩽"` tel que tout sous-ensemble non vide possède un élément minimal. On remarquera que cet élément minimal est nécessairement unique. On dit que `(E,"⩽")` est un ensemble bien ordonné, et cela s'écrit formellement comme suit :
`AA A "∈"ccP_(">"0)(E),EEa"∈"A,AAb"∈"A,`
`AA(x,y,z)"∈"E^3,`
relation d'ordre
On veut pouvoir définir une fonction de `ccP_(">"0)(E)->E` qui associe à chaque partie non vide de `E`, son élément minimum. Mais, dés que l'on manipule des objets de taille infinie, il convient de formaliser précisement les axiomes qui nous permettent de faire cette manipulation, de faire ce raisonnement, car le caractère infini rend non trivial toutes les moindres transformations.
L'axiome qui permet de construire cette fonction est « l'axiome du choix unique », appelé aussi « l'axiome de définition d'une application » qui dit textuellement :
S'il existe une relation `R"(.,.)"` de `A` vers `B` définissable c'est à dire qui peut s'écrire dans le langage prédicatif en cours, et si cette relation est une fonction c'est à dire qui satisfait `AAx"∈"A, EE!b, R(a,b)`, alors il existe une fonction qui produit cette image `b` pour chaque élément `a` de l'ensemble `A` et qui se définit en appliquant cette axiome.
Notez que l'expression `EE!x, P(x)` signifie textuellement qu'il existe un unique `x` tel que `P(x)`, c'est à dire que:
`EE!x, P(x) <=> EEx, P(x) "et" AAy, P(y) => (y"="x)`
L'existence d'une relation `EER"(.,.)"` définissable, signifie qu'il existe une définition de cette relation `R"(.,.)"` dans le langage prédicatif en cours. Cela n'est pas si restrictif que cela car il est toujours possible d'ajouter au langage prédicatif un nouveaux prédicat générateur `R"(.,.)"` , rendant de faite `R` définissable, sans que nous ayons posé aucune condition sur ce prédicat, seul le langage prédicatif c'est agrandit ainsi que le pouvoir d'expression du langage prédicatf en cours.
Cet axiome se note formellement comme suit :
Axiome de définition d'une application :
Par contre la définitiopn de la fonction `m` ainsi produite n'a pas encore d'écriture directe. L'écriture directe pourrait être `m="fonction"(R)` car ils ont le même graphe, et l'un est un opérateur unaire, et l'autre est un prédicat binaire. Le méta-opérateur `"fonction"` transformerait ainsi une relation fonctionnelle de `A` vers `B` en un opérateur de `A` dans `B`.
La réciproque ne pose pas de difficulté, car étant donné une fonction `m"(.)"`, on peut toujours définir une relation comme suit : `R(x,y) <=> (y"="m(x))`.
Avec cet axiome, nous pouvons déduire que si `(E,"⩽")` est un ensemble bien ordonné, alors il existe une fonction `m` de `ccP_(">"0)(E)->E` qui associe à chaque partie non vide de `E` l'élément minimum. Et cela se note formellement comme suit :
`(E,"⩽") "bien ordonné" => EEm"(.)", AAA "∈"ccP_(">"0)(E), AAa "∈" A, m(A)"∈"E "et" m(A)"⩽"a`
On définit la relation suivante :
`R (A,a) = a "∈"A "et" AAx"∈"A, a"⩽"x`
Cette relation est bien fonctionnelle. Puis on définit l'opérateur comme suit :
`m = "fonction" (R)`
---- 17 février 2019 ----
Cette dernière condition est identique à la propriété qu'il n'existe pas de suites infinies d'éléments strictement décroissante commençant par cet élément. Cette condition est quand même extrêmement forte !. C'est pourquoi, il est certainement possible de définir des ordinaux plus généraux, avec une condition plus faible que celle du bon ordre.
Un ordinal est une catégorie d'ensembles totalement ordonnés avec un élément minimum et une fonction successeur direct définie partout sauf pour l'éventuel élément maximum, dans laquelle les ensembles sont liables deux à deux par des isomorphismes c'est à dire des bijections respectant l'ordre, l'élément minimum et l'opérateur successeur directe.
Un ordinal idiomatique est un ensemble totalement ordonné avec un élément minimum et un opérateur successeur directe définie partout sauf pour l'éventuel élément maximum, à isomorphisme près. Il y a donc deux types d'ordinaux, ceux avec un élément maximum, noté `1`, et ceux sans élément maximum.
`(A,"⩽", 0, 1, s(A"-"{1})) " ensemble totalement ordonné avec élément minimum "0" élément maximum "1" et successeur directe "s"(.)"`
`(B,"⩽", 0, 1, s(B"-"{1})) " ensemble totalement ordonné avec élément minimum "0" élément maximum "1" et successeur directe "s"(.)"`
`"Ord"(A)"=""Ord"(B) <=> ((EEh "∈" (A"↔"B)), (AAxAAy‚ x"⩽"y <=> h(x)"⩽"h(y)), (h(0)=0), (h(1)=1), (AAx‚ h(s(x))=s(h(x))))`
---- 15 février 2019 ----
`(A,"⩽", 0, s"(.)") " ensemble totalement ordonné avec élément minimum 0 et successeur directe s(.)"`
`(B,"⩽", 0, s"(.)") " ensemble totalement ordonné avec élément minimum 0 et successeur directe s(.)"`
`"Ord"(A)"=""Ord"(B) <=> ((EEh "∈" (A"↔"B)), (AAxAAy‚ x"⩽"y <=> h(x)"⩽"h(y)), (h(0)=0), (AAx‚ h(s(x))=s(h(x))))`
Notez que dans cette expression on utilise l'inférence de type. Ainsi la fonction `s"(.)"` est celle de la structure `A` si elle utilise comme argument un élément typé comme apartenant à `A`, et elle est celle de la structure `B` si elle utilise comme argument un élément typé comme apartenant à `B`. La variable `x` évolue dans un domaine restreint à l'ensemble des éléments de `A` si elle est utilisé comme argument de `h"(.)"` et elle diffère de l'élément maximal si elle est utilisé comme argument de `s"(.)"`. L'élément `0` est celui de la structure `A` si il est utilisé comme argument de `h"(.)"`, et il est celui de la structure `B` si il est égale à une image de `h"(.)"`. Et dans la dernière expressions `h(s(x))=s(h(x))`, l'inférence de type entraine que `x` est restreint à un domaine tel que `x in Dép(h)`, c'est à dire `x in A`, et tel que `h(x)` n'est pas maximum et tel que `x` n'est pas maximum.
Il convient de définir ce qu'est un ensemble pouvant servir d'ordinal. C'est d'abord un ensemble munie d'une relation d'ordre totale, que l'on note `"⩽"`. On ajoute comme propriété qu'il doit posséder un élément minimum, que l'on note `0`. Puis on ajoute la propriétété qu'il possède une fonction successeur directe `s` définie sur tous les éléments `x` autre que l'éventuelle élément maximum.
Le qualificatif directe signifie que pour tout élément `x` qui n'est pas l'éventuel élément maximum, nous avons `x"<"s(x)`, et il n'existe pas d'élément `y` pouvant s'insérer comme suit `x"<"y"<"s(x)`.
On distingue donc à première vue deux sortes d'ordinaux ; ceux qui ont un élément maximum et ceux qui n'en ont pas. Mais, à l'aide du mécanisme d'inférence de type, on veut pouvoir définir ces deux sortes d'ensemble en une même structure.
---- 14 février 2019 ----