On cherche l'éveil d'une intuition, c'est pourquoi on va se donner un corpus idéologique susceptible d'alimenter substantiellement cette intuition. En retour, c'est elle qui va nous permettre de faire les bons choix, de définir les concepts pertinents et de les faire dans un ordre presque déterminé selon une philosophie, élémentarienne, batissant un langage d'opérateurs et de procédures, comme un jeu de légos, d'une façon la plus libre possible afin d'obtenir une syntaxe simple donnant une large capacité d'expression.
La théorie se comporte alors comme un entonnoir, elle s'applique sur un large spectre de configurations et produit par le calcul ses démonstrations favorites, se comportant ainsi comme un canaliseur.
Nous procédons étape par étape pour que chaque choix puisse découler de source, et on décrit un environnement, une nature, qui donne à ces opérateurs et ces procédures un sens plus profond alimentant l'intuition qui nous guide.
La construction s'appuit sur la programmation qui est le véritable fondement de la logique. Les mécanismes de typage par inférence que l'on trouve dans plusieurs langages informatiques seront utilisés abondament dans notre langage mathématique. On fera des mathématiques comme on fait de la programmation.
Selon les préceptes élémentariens, la garantie de cohérence du système est reportée dans le processus constructif auquel nous nous soumettons. En privilègiant une approche constructive, on s'assure ainsi que le raisonnement purement logique que nous allons mettre en oeuvre gardera toujours les pieds sur Terre.
Les élémentariens utilise l'axiome du choix pour skolémiser les théories mais toujours en distinguant ce qui est calculable de ce qui ne l'est pas. Ils acordent de l'importance à ce qui est calculable et considère inutile ce qui ne l'est pas. Il considère inutile le continuum des nombres réels, et s'attache à une représentation dénombrable en ne retenant que les seuls réels calculables c'est-à-dire déterminée par suite de cauchy calculable à coefficient rationnel. On construit l'espace à partir du processus programmatif, énumératif, ou démonstratif, qu'est la construction des entiers naturels `NN`. On construit le corps des réels calculables qui nous permet de mesurer toutes les constructions géométrique. On l'étend aux infinis en le corps des hyperréels calculables, permettant de formaliser les ordres de grandeurs différentiels. On revisite ainsi les fondements de l'analyse.
L'analyse étudie la notion de limite, de continuité, de dérivation et d'intégration. L'approche classique générale pour aborder l'analyse passe d'abord par la notion de distance et d'espace métrique. Une fois la distance définie, apparait naturellement la notion de topologie, de continuité, de dérivation et d'intégration. Une autre façon plus innovante consiste à développer l'analyse en même temps que la construction des nombres et de la métrique. On développe ainsi l'analyse en repartant de zéro par un processus purement logique.
Qu'est-ce que la continuité ?. Deux possiblités s'offrent à nous de définir la continuité. Soit d'une manière intuitive et constructive. Ou soit d'une manière beaucoup plus libre encore mais dans un espace bimétrique plus riche, contenant deux métriques. L'une pour désigner les passages continues. L'autre pour désigner les passages discontinues « à vole d'oiseaux ».
L'analyse développée à partir de zéro dans un processus purement logique va nous permettre de définir d'une manière la plus générale qui soit ce qu'est une demi-droite et ce qu'est une droite.
Le langage logique utilise la notion d'opérateur typé. On commence par décrire succinctement le langage engendré par des opérateurs typé, appelé « langage terminologique » ou simplement « terminologie », puis on décrit succinctement le langage décrivant les types que l'on appelle « langage typologique » ou simplement « typologie ». Et on commence par survoler une brève description du langage mathématique.
Pour éviter l'usage intensif des parenthèses, on fixe un ordre de priorité syntaxique des opérateurs binaires, du plus prioritaire au moins prioritaire :
`"∗","×"` `+` `"→"` `"∈"`,`"∉"` `"<","⩽",">","⩾"` `"et", "ou"` `"⇒", "⇔"` `"=","≠"` `"⊨","⊭"`
Ainsi par exemples, pour tout élément `x,y,z`, pour tout ensemble `E`, pour tout prédicat unaire `A"(.)",B"(.)"`, et pour tout booléen `P,Q,R`, nous avons :
Certains opérateurs unaires ont une syntaxe collé-gauche tel que l'opérateur `"-(.)"` qui appliqué à `x` se note en collant l'opérateur sur sa gauche sans mettre de parenthèse `"-"x`, ainsi que l'opérateur de négation `¬`. On les munit également d'une priorité syntaxique. Le moins unaire et de priorité juste au dessus de celle de l'addition. La négation est de priorité supérieur à tout, faisant que :
Les déclarations de variable universelle ou existentielle ont une syntaxe la moins prioritaire, faisant que :
Le produit se note parfois par absence de symbole, par exemple : `xyz = x"∗"y"∗"z`
On utilise les opérations `"+"`, `"∗"`, indifféremment sur des éléments ou des ensembles d'éléments, sauf mention contraire. Ainsi par exemples, pour un élément `a` et des ensembles `U` et `V`, nous avons :
`a"+"U = {a"+"u "/" u "∈" U}`
`aU = {au "/" u "∈" U}`
`U"+"V = {u"+"v "/" u "∈" U, v "∈" V}`
`UV={uv "/" u "∈" U, v "∈" V}`
On identifie les valeurs logiques aux booléens, le vrai est identifié au booléen `1`, le faux est identifié au booléen `0`
On adopte les conventions suivantes : Un ensemble de propositions désigne leur conjonction. Et de même, un vecteur de propositions désigne leur conjonction. Par exemple, pour toute variables booléennes `P, Q, R`, nous avons :
L'expression `((P),(Q),(R))`, ainsi que l'expression `{P,Q,R}`, en tant que proposition, signifie `P "et" Q "et" R`
L'approche dichotomique propose des propositions définies par morceaux pouvant se recoupés qui ont la forme suivante où les proposition `A_1,A_2, A_3` sont particulièrement choisie comme étant simple à calculer :
`((A_1"⇒"R_1),(A_2"⇒"R_2),(A_3"⇒"R_3))`
L'exemple comprend 3 composantes mais il peut y en avoir autant que l'on veut.
On décrit une méthode rudimentaire de construction de terme qui s'apparente à un jeu de Légos. On pose des opérateurs de base ou dits générateurs, caractérisés par un nom et une arité. Par exemple `a,b,f"(.)",g"(.,.)"` où le suffixe `"(.,.)"` précise que l'opérateur est binaire, où le suffixe `"(.)"` précise que l'opérateur est unaire, et où l'absence de suffixe précise que l'opérateur est nullaire.
On définit un langage terminologique permettant de définir les termes, autrement dit, on définie une terminologie. C'est l'ensemble des compositions closes finies d'opérateurs de base. C'est le domaine de Herbrand. La clôture par composition close finie se note en entourant de crochets la liste des opérateurs de base ou dits générateurs :
`"<"a,b,f"(.)",g"(.,.)>" = {a,b,f(a),f(b),g(a,a),g(a,f(a)), f(f(b)), g(f(a),f(b)),...}`
La terminologie est dite monotype car les éléments arguments des opérateurs sont tous d'un même type, c'est à dire appartiennent à un même ensemble dit sous-jacent. Le terme correspond à un calcul déterminant un élément dans cet ensemble sous-jacent.
Les termes `a` et `b` désigne des éléments de base ou dits générateurs c'est-à-dire qui font partis de la présentation du langage, tandis que les termes `f(a), g(a,f(a))` désignent des éléments qui, s'ils sont distincts de `a` et de `b`, ne sont pas générateurs. La différence qui existe entre un élément et un terme tient en ce que deux termes d'expression distinctes peuvent désigner le même élément. Le terme est le désignant, l'élément est le désigné. Le terme fait parti du langage correspondant à la structure libre, l'élément fait parti des objets désignés par le langage.
Un opérateur est une application d'un ensemble de départ vers un ensemble d'arrivé. Etant donné des ensembles `A,B,C` qui constituent les types de base, l'ensemble des opérateurs de `A` vers `B` se note `A"→"B` et constitue un nouveau type.
Les types sont des meta-opérateurs, de telle sorte que comme avec les opérateurs on va définir une terminologie des types qui s'appellera une typologie.
Remarquez qu'un terme peut posséder plusieurs types, par exemple il peut être à la fois de type `A` et de type `B` s'il appartient à l'intersection des ensembles `A` et `B`. Mais plus surprenant, il peut être à la fois un élement de type `A` et un élément de type `B"→"C` faisant qu'il appartient à l'intersection des ensemble `A` et `B"→"C`, et il peut cumuler plusieurs rôles distincts, ce qui entraine toute une conséquence d'égalités comme nous le verrons plutard. Rappellons-nous qu'une des propriétés paradigmatiques de l'élément consiste en la capacité de pouvoir désigner toute chose, et que deux éléments intialement distincts peuvent toujours être rendus égaux par simple hypothèse.
Le méta-opérateur binaire `"→(.,.)"` que l'on note avec le suffixe `"(.,.)"` pour rappeller son arité, va permettre de construire de nouveaux types à partir d'autres types. Sa syntaxe est centrée c'est à dire qu'appliqué à `(A,B)` il constitue le terme `A"→"B`. On définit ainsi un langage typologique, une typologie, désigant les différents types possibles. C'est l'ensemble des compositions closes finies de meta-opérateur de base, ce qui se note par exemple :
`"<"A,B,C,"→(.,.)>"`
La typologie est dit monometatype car les arguments des meta-opérateurs, et pour l'instant il n'y en a qu'un, `"→"`, sont tous d'un même type de type, d'un même meta-type de base qui est le meta-type ensemble. Il n'y a qu'un seul type de types.
Noter que cette typologie ne permet pas de désigner l'ensemble des couples `A"×"B`. Mais pour n'importe quel type `E` du langage typologique, elle permet de désigner l'ensemble des applications de `A"×"B"→"E` sous forme curryfiée, par le type `A"→"(B"→"E)`.
Nous sommes dans une logique classique régie par deux valeurs de vérité : le vrai représenté par la valeur `1` et le faux représenté par la valeur `0`, et qui permet de définir le quanta de quantité d'information qu'est le bit. C'est pourquoi on définit le type booléen noté `{0,1}`.
On consate que le type `{0,1}"→"E` désigne le type `E^2`. Les éléments de ce type s'appellent des couples d'éléments de `E`. Le type `E"→"{0,1}` désigne les sous-ensemble de `E`. Les éléments de ce type s'appellent des sous-ensembles de `E` ou des prédicats définis sur `E`. Le type `{0,1}"→"{0,1}` désigne les opérateurs unaires booléens. Le type `{0,1}"×"{0,1}"→"{0,1}` désigne les opérateurs binaires booléens. Le type `{0,1}"×"E"→"E` désigne le type `2E`. Les éléments de ce type s'appellent des couples composés d'un premier argument booléen et d'un second argument élément de `E`.
La terminologie multitype ne complexifie pas outre mesure. Le terme devient plus général puisque qu'il compose des opérateurs générateurs de type variée en respectant les types attendus. Le terme désigne un calcul à partir d'opérateurs générateurs, de telle sorte qu'une formule sans quantificateur constitue un terme.
Une théorie est écrite dans un langage logique que l'on définit par une liste d'opérateurs. Le langage de la théorie fait partie de la théorie. Et il doit être possible d'écrire une théorie qui ne comprend qu'un langage sans autre propriété. Par exemple :
`EEa "∈" E,EEs"∈" E"→"E, EE"+" "∈" (E"×"E"→"E), EE"⩽ ∈"(E"×"E"→"{0,1})`
Le langage de cette théorie est décrit par la liste `(E,a,s,"+","⩽")` comprenant un type `E` et 4 opérateurs `a,s,"+","⩽"`, que l'on complète en précisant leur type en exposant :
`(E, a^E, s^(E"→"E),"+"^((E"×"E)"→"E),"⩽"^( E"×"E "→"{0,1}))`
La première variable `E` est un type c'est à dire un méta-opérateur. Il se distingue des opérateurs en ce qu'il n'a pas de type plus précis que celui d'ensemble. C'est un prédicat qui peut s'appliquer à tout élément, `E={x "/" E(x)}`, une définition purement logique. C'est un type de base désignant l'ensemble sous-jacent. Dans les cas simples d'une terminologie monotype où il n'y a qu'un ensemble sous-jacent `E`, celui-ci est alors sous-entendu :
`(a, s"(.)","+(.,.)" "|" "⩽(.,.)")`
Il y a alors deux sortes d'opérateur, ceux dits internes qui ont un résultat appartenant à l'ensemble sous-jacent, et ceux apppelés prédicats qui ont un résultat de type booléen. Les prédicats sont mis après les opérateurs internes, et le symbole tube "`"|"`" termine la liste des opérateurs internes pour commencer la liste des prédicats internes. Le contexte précisera que l'opérateur `"+"` et le prédicat `"⩽"` ont une syntaxe centrée.
La déclaration existentielle de variable nous permet de définir une terminologie, un langage terminologique, autrement dit, une structure libre engendrée, que l'on note en entourant de crochets les opérateurs de base :
`"<"a, s"(.)","+(.,.)" "|" "⩽(.,.)>"`
La structure libre comprend tout les termes du langage. À ce stade, la structure libre est synonyme de langage terminologique.
Puis on ajoute au langage de la théorie, un prédicat binaire interne qui est celui de l'égalité `"=(.,.)"`, qui est de type `E"×"E "→"{0,1}` et qui a également une syntaxe centrée.
Puis on ajoute l'opérateur logique booléen de négation `"¬", qui est de type `{0,1}"→"{0,1}`. Puis on ajoute les opérateurs logiques booléens de conjonction `"et", de disjonction "ou", et d'implication "⇒"`, qui sont de type `{0,1}"×"{0,1}"→"{0,1}` et qui ont également une syntaxe centrée.
Les termes qui produisent un boolean sont appelées des propositions.
Les proposition n'utilisant pas les opérateurs logiques sont appelés des littéraux positifs, puis s'ils sont négativés par la négation alors ils sont appelés des littéraux négatif.
Un littérale est un littérale positif ou négatif.
Une clause est une disjonction de littéraux.
Chaque proposition de décompose en une conjonction de clauses de façon unique à l'ordre près et à une permutation près des variables de même type.
Le langage logique est un langage contextuel c'est à dire qu'une même sous-proposition n'a pas la même signification selon où elle se place, sa signification dépend du contexte. Le contexte dont il est question est un langage terminologique, une terminologie qui se modifie à chaque déclaration de nouvelle variable existentielle ou universelle, et qui s'étend sur une portée appelé bloc ou contexte. De tel sorte que les contextes s'emboitent les uns dans les autres pour former un arbre. En cela, c'est un langage contextuel plus particulier dit déclaratif.
Le langage logique est un langage déclaratif. Il existe deux sortes de déclarations, les déclarations de variable existancielle et les déclarations de variable universelle, qui ont chacune une portée limité à un bloc. La nouvelle variable qui va jouer le rôle d'un nouvel opérateur, est ajouté à la terminologie du contexte. Si la variable fait déjà partie du contexte, la nouvelle variable va masquer l'ancienne durant toute la portée du bloc.
La proposition est dite du premier ordre si les déclarations de variables quelle contient sont toutes d'un même type d'élément, sinon les variables peuvent être de toute sorte de type.
On utilise l'axiome du choix permettant la skolemisation. Ainsi, toute formule se ramène à une théorie n'utilisant que des quantificateur universelle et les connecteur et et ou et n'itilisant pas la negation négation des dans une terminologie racine.
Considérons la proposition suivante :
`AAxEEy,P(x,y)`
La forme skolémisée de cette proposition est :
`EEy"(.)"AAx,P(x,y(x))`
La forme skolémisée entraine de façon évidente la forme initiale. Réciproquement la forme initiale entraine la forme skolémisée grâce à l'axiome du choix qui permet de définir l'opérateur `y"(.)"` en constitutant son graphe en faisant une infinité de choix. On place ainsi la déclaration des variables existentielles en premier, formant un langage terminologique racine que l'on munie de la théorie universelle restante.
Par symétrie vis-à-vis de la négation, l'opération contraposée s'appelle l'herbrandisation. Considérons la proposition suivante :
`EExAAy,P(x,y)`
La forme herbrandisée de cette proposition est :
`AAy"(.)"EEx,P(x,y(x))`
On place ainsi la déclaration des variables universelle en premier.
La logique IF (Independence-Friendly), littéralement « respectueuse de l'indépendance » 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.
Nous commençons par décrire une variable quantifiée existentiellement de façon indépendante d'une variable quantifiée universellement, et qui a l'avantage de produire une forme skolémisée plus simple. Puis nous décrirons l'indépendance d'une disjonction vis-à-vis d'une variable quantifiée universellement.
Considérons un prédicat quaternaire `P"(.,.,.,.)"`. Et considérons la propriété suivante :
`AAx EEa AAy EEb, P(x,a,y,b)`
Le choix de `a` dépend de `x` et le choix de `b` dépent de `(x,y)`. La skolemisée est :
`EEa"(.)" EEb"(.,.)" AAx AAy, P(x,a(x),y,b(x,y))`
Parcontre si nous prenons comme hypothèse que le choix de `b` peut ne dépendre que de `y` alors il faut enrichir la notation pour pouvoir l'exprimer au premier ordre. On utilise à cet effet les quantificateurs de Henkin, mettant au dénominateur la liste :
`AAx EEa AAy (EEb"/"AAx), P(x,a,y,b)`
Cette propriété signifie littéralement : « Quelques soit `x`, il existe `a`, quelque soit `y`, il existe `b` indépendament de `x` tel que `P(x,a,y,b)` ». La skolemisée est :
`EEa"(.)" EEb"(.)" AAx AAy, P(x,a(x),y,b(y))`
Notez que les liens de dépendance d'une variables quantifiée existentiellement ne concernent que des variables quantifiées universellement, et inversement par contraposée. On peut aussi utiliser une notation explicitant les dépendances mais cette dernière notation s'alourdie lorsque l'on doit mettre également les dépendances contraposées. La formule initiale s'écrit :
`AAx EEa{x} AAy{a} EEb{x,y}, P(x,a,y,b)`
La formule introduisant l'indépendance de `b` vis-à-vis de `x` s'écrit:
`AAx EEa{x} AAy{a} EEb{y}, P(x,a,y,b)`
La disjonction indépendante d'une variable déclarée universellement `AAx`, se note comme suit :
`"ou"/(AAx)`
Elle signifie qu'il faut choisire l'un ou l'autre des arguments du connecteur mais de façon indépendante de la valeur de `x`. La disjonction indépendante de `x` est plus restrictive que la simple disjonction. Dans le cas trivial, nous avons :
`AAx,P(x) "ou"/(AAx) Q(x)`
Il doit exister un critère indépendant de `x` qui tranche la disjonction, et qui n'est ici dépendant de rien d'autre, c'est donc un booléen `B` qui tranche la question :
`AAx,(B "et" P(x)) "ou" ("¬"B "et" Q(x))`
C'est à dire :
`(AAx,P(x)) "ou" (AAx,Q(x))`
Prenons un exemple plus générale où une autre variable intervient :
`AAxAAy, P(x,y) "ou"/(AAx) Q(x,y) `
Cette proposition signifie qu'il existe un critère de choix de l'alternative qui est indépendant de `x` c'est à dire qui n'est fonction que des autres variables mises en jeu, arguments de `P` ou de `Q`, c'est à dire ici qui est fonction de la seul variable `y`. Appellons ce selecteur `S`. C'est un opérateur de `E ->{0,1}` qui appliqué à `y`, tranche l'alternative :
`AAxAAy, (S(y) "et" P(x,y)) "ou" ("¬"S(y) "et" Q(x,y))`
Puis il faut déclarer explicitement l'existence de `S`. On l'ajoute au contexte par une déclaration de variable existentielle de type `E ->{0,1}` dans une logique du second ordre :
`EES^(E->{0,1}) AAx AAy, (S(y) "et" P(x,y)) "ou" ("¬"S(y) "et" Q(x,y))`
Notez que lorsque le type des variables n'est pas indiqué dans leur déclaration, par défaut c'est le type `E`. La forme ainsi obtenue est déjà skolémisée :
Le langage racine devient : `(S^(E->{0,1}), P^(E×E->{0,1}), Q^(E×E->{0,1}))`
La théorie universelle devient : `AAxAAy, (S(y) "et" P(x,y(x))) "ou" ("¬"S(y) "et" Q(x,y(x)))`
La négation d'une proposition n'utilisant que les quantificateurs `EE,AA` avec la notation de Henkin ou la notation explicitant les dépendances, ainsi que les seuls connecteurs logiques `"¬", "et", "ou"`, s'obtient toujours facilement en inversant les quantificateurs `EE` et `AA`, en inversant les connecteurs `"et"` et `"ou"`, et en négativant chaque littéraux.
Proposition |
Proposition skolemisée |
|
| `AAx EEa AAy EEb, P(x,a,y,b)` | `<=>` | `EEa"(.)" EEb"(.,.)" AAx AAy, P(x,a(x),y,b(x,y))` |
| `AAx EEa AAy (EEb"/"AAx), P(x,a,y,b)` | `<=>` | `EEa"(.)" EEb"(.)" AAx AAy, P(x,a(x),y,b(y))` |
Par négation, nous avons :
Proposition |
Proposition herbrandisée |
|
| `EEx AAa EEy AAb, P(x,a,y,b)` | `<=>` | `AAa"(.)" AAb"(.,.)" EEx EEy, P(x,a(x),y,b(x,y))` |
| `EExAAaEEy (AAb"/"EEx), P(x,a,y,b)` | `<=>` | `AAa"(.)" AAb"(.)" EEx EEy, P(x,a(x),y,b(y))` |
La sémantique d'une proposition se définit comme l'ensemble des mondes où la proposition est réalisée, reste à définir ce qu'est un monde, et comment une proposition se réalise dans un monde.
Un monde est un ensemble de propositions, pouvant être de cardinalité infini, non contradictoire c'est à dire dont chaque partie fini qui constitue de fait une proposition n'est pas une antilogie, et qui possède la propriété de trancher toutes les propositions du premier ordre.
On accumule ainsi dans un monde des propositions, de façon non-contradictoire, nécessaires pour pouvoir trancher toutes propositions.
Une proposition P se réalise dans un monde M s'il existe un sous ensemble de M constituant de faite une proposition, qui démontre P. Considérons un modèle `M` qui réalise `P` ce qui se note :
`M |== P`
On dit que `M` satisfait `P`, c'est-à-dire que la théorie `P` est vrai dans le modèle `M`, c'est-à-dire que `M` est une réalisation de `P`. L'ensemble des réalisations de `P` c'est à dire l'ensemble des modèles où `P` y est vrai, constitue la sémantique de `P`.
Considérons une seconde théorie `Q` de langage plus vaste ou égale à celui de `P`. On utilisera le même symbole `|==` pour désigner l'implication sémantique. L'implication sémantique de `Q` vers `P` signifie que tout modèle satisfaisant `Q` satisfait `P`, et se note pareillement :
`Q |== P`
L'implication sémantique ne découle pas de la démonstration mais découle de la réalité. La sémantique d'une théorie ou d'une structure est l'ensemble de ses réalisations possibles. L'implication sémantique de `Q` vers `P` signifie que toutes les réalisations de `Q` sont des réalisations de `P`, et donc que l'ensemble des réalisations de `Q` est inclus dans l'ensemble des réalisations de `P`, et donc que la sémantique de `Q` est incluse dans la sémantique de `P`.
---- 16 février 2023 ----
La logique du second ordre permet de définir des propositions qui vont rendre toute théorie incohérente. La première telle proposition est décrite par Russel. C'est la question suivante : " L'ensemble des ensembles ne se contenant pas se contient-t-il ".
On ne veut rentrer maintenant dans la description de la déduction. On admet seulement qu'il existe un ensemble de règles de déduction d'ordre syntaxique qui transforment de faite toute théorie dénombrable en un moteur énumérant toutes ses déductions possibles.
L'introduction de la calculabilité est nécessaire pour fonder les logiques d'ordre supérieur, comme seul critère tangible capable d'évacuer la contradiction. Elle se définit en listant les opérateurs servant de briques de construction, transformant une théorie en une structure. Les opérateurs servant de briques de construction sont appelés les opérateurs générateurs de la structure. Ils sont listés dans la présentation de la structure et en constitue son langage.
Chaque opérateur de la présentation de la structure est une procédure élémentaire faisant partie d'une couche logiciel sous-jacente mise à disposition du programmeur. Néanmoins ces procédures élémentaires peuvent ne pas être calculables au sens classique, elles sont alors comme des oracles donnant toujours une réponse et mise à disposition du programmeur comme une procédure d'entrée-sortie.
On considère tous les programmes n'utilisant que ces procédures élémentaires avec bien évidement les bases de la programmation qui correspondent à l'arithmétique.
Les éléments dits calculables de la structure sont définis comme étant ceux produisibles par un tel programme. Autrement dit, ce sont les compositions closes finies d'opérateurs du langage de la structure qui forme le domaine de Herbrand.
Les opérateurs calculables de la structure sont définis comme étant ces programmes, et en fixant un élément calculable comme résultat pour les cas où le programme ne s'arrête jamais.
Comment formaliser l'idée intuitive de distance séparant deux points ? On la formalise en une fonction binaire `d"(.,.)"` appelée métrique, de `E^2` vers `D`, où `E` est un ensemble de points et `D` un ensemble de valeurs de distance possibles.
L'ensemble des valeurs `D` devra satisfaire un certain nombre d'axiomes. Ces axiomes définiront la structure de l'ensemble des valeurs de distances.
La métrique `d"(.,.)"` est une fonction binaire de `E"×"E"→"D` qui devra satisfaire un certain nombre d'axiomes propre à une métrique.
L'ensemble `E`, munie d'une métrique, `(E,D,d)`, est appelé un espace métrique.
Dans notre philosophie, pour définir une nouvelle notion mathématique, on regroupe dans une compréhension, tout ce que l'on peut faire avec, tout ce en quoi elle intéragit avec ses homologues et avec l'exterieur. Car c'est à travers les échanges qu'elle entretient avec son entourage qu'elle se définit. On pourrait dire que c'est son rôle sociale qui la définit. Notre méthodologie consiste à détailler aussi finement que possible toutes ces caractéristiques premières.
Considérons des variables quantifiées universellement `AAxAAyAAz` sur un ensemble de valeurs de distance, `D`. Voici la liste des 11 premiers principes d'une distance :
| `D |== EE "⩽" "∈" (E"×"E"→"{0,1})` |
| `x"⩽"x` |
| `x"⩽"y "et" y"⩽"x => x"="y` |
| `x"⩽"y "et" y"⩽"z => x"⩽"z` |
| `x"⩽"y "ou" y"⩽"x` |
| `D |== EE"+" "∈" (E"×"E"→"E)` |
| `(x"+"y)"+"z=x"+"(y"+"z)` |
| `x"+"y=y"+"x` |
| `x"⩽"(x"+"y)` |
| `x"⩽"y => ∃s, x"+"s"="y` |
| `x"+"z"="y"+"z => x"="y` |
Le principe n°10 introduit une variable existentielle et s'écrit :
`AAxAAyEEs, x"+"s"="y "ou" ¬(x"⩽"y)`
La négation `¬(x"⩽"y)` se note `x">"y`. La quantification`EEs` ne dépend que de `(x,y)`. La forme skolémisée de l'axiome n°10 est :
`EEs"(.,.)"AAxAAy, x"+"s(x,y)"="y "ou" x">"y`
L'opérateur `s"(.,.)"` peut être ainsi ajouté à la théorie produisant la forme skolémisée de la théorie. Mais attention, si on ajoute de plus cette opération à la présentation de la structure alors cela va modifier la définition des éléments calculables de la structure. En effet, en ajoutant `s"(.,.)"` comme une procédure élémentaire mise à disposition du programmeur, on change de faite la définition des éléments calculable de la structure. L'ensemble des éléments calculables devient plus grand. Et comme dans notre philosophie élémentarienne on ne s'intéresse qu'à la sous-structure des éléments calculables, cela agrandit la structure.
On précise dans les principes suivants qu'elles sont les opérateurs mis à disposition du programmeur, engendrant la sous-suctructure des éléments calculables.
Si `D` n'est pas vide, il existe au moins une valeur `a "∈" D`. À partir de cette valeur on définit l'élément `0` comme suit :
`0=s(a,a)`
Cette élément sera appelé la distance nulle. Et il s'agit bien de la distance nulle, élément neutre de `"+(.,.)"`, car :
`a+s(a,a) = a`
`x+0 = x+s(a,a)`
`x+0+a= x +s(a,a)+a`
`x+0+a= x +a+s(a,a)`
`x+0+a = x+a`
`x+0 = x`
On considère toujours `D` non-vide. L'élément `0` est donc déjà un élément calculable. La valeur `s(x,y)` correspond intuitivement à `y - x` lorsque `x"∈"y`. Et dans ce cas, grace à l'axiome n°11, `s(x,y)` est la seul et unique valeur qui peut être ajoutée à `x` pour donner `y`. Comme cet opérateur a été ajouté au langage de la structure, on préfère tout-de-suite fixer sa définition complète, et on choisie la solution la plus simple qui consiste à lui donner comme résultat `0` lorsque `x"<"y`.
On appelle valeur tout élément de `D`, et on appelle grandeur tout élément non-nul de `D`. L'ensemble des grandeurs se note `D^"∗"`.
Une proposition logique `a "et" b => c` est équivalente à la clause `c "ou" ¬a "ou"¬b`. À ce stade, la structure `D` des valeurs de distance est définie par la présentation des trois opérateurs `"+", s, ⩽` et par 9 axiomes sous forme de clause de littéraux :
`D|==("+(.,.)", s "(.,.)" "|" "⩽(.,.)")`
`AAxAAyAAz,`
`x"⩽"x`
`x"⩽"(x"+"y)`
`x"+"y=y"+"x`
`x"⩽"y "ou" y"⩽"x`
`x"+"z"≠"y"+"z "ou" x"="y`
`x">"y "ou" y">"z "ou" x"⩽"z`
`x">"y "ou" y">"x "ou" x"="y`
`x"+"s(x,y)"="y "ou" x">"y`
`(x"+"y)"+"z=x"+"(y"+"z)`
La présentation de la structure découle des principes n° 1, 6, 10, 12, 13, 14. Les 9 axiomes découlent des principes n° 2, 3, 4, 5, 7, 8, 9, 10, 11. Puis on ajoute les constructions secondaires qui définissent `<` et `0` :
`x">"y = "¬" (x"⩽"y)`
`0 = s(x,x)`
Puis, après cette énumération précise des caractéristiques premières et secondes, notre méthodologie procède de façon inverse. On regroupe toutes ces caractérstiques en une ou deux propriétés globales qui les engendrent. À ce stade, `D` représente une demi-droite partant d'un point zéro. Les points sont totalement ordonnées et ils forment un monoïde commutatif simplifiable où l'ordre coïncide avec le prés-ordre d'accumulation du monoïde. Mais cette dernière description peut être simplifiée en la remplaçant par une propriété globale de symétrie plus parlante, qui introduit l'idée de repère. Il y a bien un repère qui est le point zéro, un repère absolu. Mais les propriétés d'une loi associative, commutative et simplifiable, peuvent peut-être se traduire plu globalement par une symétrie, un mécanisme de changement de repère.
On fait agire `D` sur lui-même par translation. Cela signifie que l'on donne un second rôle aux éléments de `D`. Chaque point `u` de `D` possède comme second rôle, une application de `D"→"D` qui envoie tout point `x` sur `u"+"x`. L'application `u` est appelé une translation :
`u(x)=u"+"x`