Les modèles de la logique du premier ordre comportent des objects de types différents. Les opérateurs sont d'arité fixes mais diverses. Ils forment autant d'objets de types différents qu'il y a d'arité différentes. Et deux objects de types différents ne peuvent pas être rendus égaux, ne peuvent pas être identifiés comme étant égaux. De même, on assemble les opérandes nécessaires à un opérateur ou à un prédicat, en une suite d'éléments formant un object qui lui aussi possède plusieurs types différents possibles, un type différents par taille de suite. Deux suites de tailles distinctes ne peuvent pas être rendues égales, ne peuvent pas être identifiées comme étant égales. Hors cette multiplicité des genres crée une complexité qui nous égard. Comment intégrer cette construction des modèles, dans la logique elle-même, dans une logique du premier ordre ? Cela peut se faire en unifiant tous les opérateurs et tous les éléments en un seul type qu'est l'opérateur unaire s'appliquant à un opérateur unaire pour produir un opérateur unaire.
Pour cela, il faut suivre les précepts de la théorie de l'information, et définir ce que l'on entend par opérateur au sens général. C'est ce que nous faisons en décrivant le langage alpha. (Il existe aussi un langage alpha d'arité variable étudié dans l'article Le langage d'opérateurs.) Le principe de base est qu'un opérateur opère sur un opérateur pour produire un opérateur, et qu'il n'y a pas de distinction entre opérateur et élément. Tout élément constitue un opérateur unaire.
Le langage alpha permet de définir une loi de composition interne dans un ensemble d'éléments d'une manière générale, qui ne nécessite pas de déclarer différent types d'opérateurs. Les éléments sont les opérateurs et n'ont qu'un seul type, celui d'opérateur unaire agissant sur eux-même.
Puis, selon les préceptes élémentariens, dans les mathématiques rien n'est immanent ni transcendant, tout doit être construit par un processus de calcul. Les structures sont construites à partir d'éléments de base appelés générateurs.
La description de ce langage d'opérateurs se formalise en 4 axiomes :
de l'axiomeTout générateur est un identifiant et possède un nom unique sous forme d'un caractère. Tout générateur est un terme. Tout terme peut s'appliquer à tout terme appelé opérande pour produire un terme appelé résultat. L'application d'un terme à une opérande produit un terme résultat qui est l'emboitement du terme appliqué à l'opérande.
L'axiome n°1 affirme que le nom d'un générateur est un caractère. C'est le premier axiome car on ne peut rien énoncer si l'on n'a pas de nom. Les générateurs sont ceux énumérés dans la présentation du langage.
L'axiome n°2 permet au langage de se déployer avec un niveau de généralité plus grand. On doit pouvoir évoquer des objets plus généraux autres que ceux posés initialement d'où cet axiome. Les générateurs du langage sont les éléments de base permettant de construire des objets plus généraux appelés termes, et l'on énumère les lois s'appliquant à ces objets plus généraux incluant les générateurs.
La réciproque est fausse. La transformation d'un terme en un générateur nécessite une opération de nommage afin de donner un nom pour ce nouvel élément et de l'ajouter à la présentation du langage.
L'axiome n°3 définie les possibilités de production des termes, c'est à dire définie la composition d'opérateurs unaires. Notez que les compositions faites ne sont jamais closes puisqu'elles produise toujours un opérateur unaire. Le résultat est constitué d'un seul terme. Le résultat n'est composé que d'un terme car s'il était composé de plusieurs termes on pourrait le simplifier en plusieurs termes plus simples ne produisant qu'un terme à la fois. L'axiomatique définie les objets les plus simples qui permettent de construire les autres objets. (Néanmoins la question se reposera lorsqu'on s'intéressera à la complexité de calcul des termes.).
L'axiome n°4 affirme que le résultat de la composition est l'expression telle quelle de la composition. Ainsi est-on assuré qu'il n'y a aucune perte d'information. Par exemple le terme `x` appliqué au terme `y` produit le terme résultat `x(y)`. L'axiome n°4 affirme que la composition correspond à l'emboitement et qu'aucune simplification n'est opérée après. L'axiome n°4 affirme ainsi que le langage n'exprime que lui-même, ou que les termes du langage désigne les éléments d'une structure libre selon son langage, ou autrement dit, que deux termes distincts désignent nécessairement deux éléments distincts.
Si on retire l'axiome n°4 alors on obtient l'axiomatique des structures non nécessairement libre. Les langages ne sont que des structures particulières dites libres. Dans les structures, tous les éléments peuvent être rendus égaux, peuvent être identifiés comme étant égaux. Toute distinction entre générateur et terme peut être effacée.
L'ensemble des termes constitue le langage, tandis que l'ensemble des générateurs constitue la présentation du langage. Les générateurs du langage engendrent à eux seuls tous les termes du langage, et sont eux-mêmes des termes du langage.
De ce qui précède, le langage est calculable, c'est à dire qu'il existe un programme appelé énumérateur du langage qui énumére tous les termes du langage. La présentation du langage, notée `L`, engendre par composition le langage, noté `"<"L">"`. Les crochets `"<">"` entourant des éléments ou ensemble d'éléments désigne la clôture par composition des éléments ou ensembles d'éléments présents. Ainsi l'ensemble `"<"L">"` est la clôture de `L` par composition. S'il n'y a pas de générateur, le langage engendré est vide. Considérons le cas où il y a un unique générateur. Alors celui-ci va non seulement engendrer un langage, mais on verra que ce langage contiendra tous les autres langages possibles. Dans la littérature contemporaine cet opérateur unique porte un nom. Il s'appelle alpha, `alpha`. Il est ici unaire. C'est à dire qu'il peut s'appliquer à tout terme du langage alpha, `"<"alpha">"`. Et il constitue en-soit un terme du langage alpha, `alpha"∈""<"alpha">"`. Regardons comment se construit le langage alpha. Sa présentation est `{alpha}`. À partir du terme `alpha` on peut construire le terme `alpha(alpha)` puis le terme `alpha(alpha(alpha))` ou bien encore le terme `alpha(alpha)(alpha)`.... Autrement dit, le langage `"<"alpha">"` correspond aux arbres binaires nu.
(Le langage alpha est un paradigme de langage mathématique. Il ne faut pas le confondre avec le langage informatique du même nom ALPHA qui est un langage parallèle fonctionnel conçu par Christophe Mauras en 1989 à l'université de Rennes.)
Une structure est un ensemble d'éléments `S` munie d'une loi de composition interne, c'est à dire d'une application de `S"×"S"→"S` qui détermine toutes les compositions d'éléments dans `S`. Par défaut les lois de composition d'une structure sont internes à la structure, et donc il n'est pas besoin de mentionner le qualificatif interne à chaque fois.
Ce choix est dicté par une interprétation orientée théorie de l'information de notre langage d'opérateurs. Les termes opérandes apportent l'information qui commande la transformation. Pas d'opérande, pas de transformation.
Quelque soit deux éléments `a` et `b` appartenant à `S`. La loi de composition de la structure `S` se définie comme suit :
`S : ((S"×"S"→"S),((a,b)"↦"a(b)))`
La loi de composition a aussi une autre forme qui s'applique à chaque élément :
`S : ((S"→"(S"→"S)), (a"↦"(b"↦"a(b))))`
Et on utilise la même lettre que la structure pour désigner ces deux applications. Pour les distinguer, on utilise la notation française pour l'application `S : ((S"→"(S"→"S))`, faisant que l'image par `S` d'un élément `a` est notée `a_S`, et on garde la notation anglaise pour l'application `S : (S"×"S"→"S)`, faisant que l'image par `S` d'un couple `(a,b)` est notée `S(a,b)`, Ainsi nous avons :
`AA (a,b) "∈" S^2, S(a,b) = a_S(b) = a(b)`
Ainsi le langage alpha se comporte comme un magma, c'est à dire comme une structure possèdant un opérateur binaire interne.
Il existe une différence entre l'élément `a` et la fonction `a_S`. L'élément `a` se comporte comme la fonction `a_S` mais il possède un nom complet, il est désigné par un terme du langage. Alors que la fonction est anonyme, elle n'a pas de nom, et est donc définie par sa seule nature de fonction. Autrement dit, il est possible que deux éléments distincts `a` et `b` puissent se comporter comme une même fonction `a_S"="b_S`. Les fonctions sont alors égales mais les éléments, eux, sont distingués par les termes qui les désignent et qui sont assurément distinct dans au moins un modèle qu'est la structure libre du langage.
Du point de vue élémentarien, où tout élément ne peut posséder qu'une quantité finie d'information, et qui grosso modo évacue la puissance du continu, la structure admet au moins un ensemble énumérable d'éléments générateurs, et comprend donc une théorie d'engendrement, qui constitue la véritable fondation des ensembles.
Le type d'une structure est son nombre minimal de générateurs. Une structure est dite :
Etant donné des éléments `x,y`. On note `x(y)` la composition de `x` appliqué à l'opérande `y` dans la structure les contenant. Mais s'ils sont membres de plusieurs structures alors il est nécessaire de préciser dans quelle structure à lieu la composition. Cela se fait en mettant en indice le nom de la structure et qui est le même que le nom de la loi de composition. Par exemple :
`(x,y) in S^2`
`(x,y) in K^2`
`x_S(y)` est la composition de `x` appliqué à l'opérande `y` dans la structure `S`
`x_K(y)` est la composition de `x` appliqué à l'opérande `y` dans la structure `K`
Cela correspond également à la notation d'application à la française
`S(x)=x_S`
`K(x)=x_K`
où l'application `S`, qui a le même nom que la structure `S`, appartient à `S"→"(S"→"S)` et constitue la loi de composition de la structure. Et de même pour `K` qui appartient à `K"→"(K"→"K)`.
Par défaut la composition `x(y)` mise en oeuvre sera celle de la structure que le contexte attribut aux 2 éléments `x,y`. Cela est plus précis que le simple fait d'appartenir à la structure, et cela inclut le typage par infèrence dépendant des déclarations locales formant divers contextes emboités, et non de l'appartenance réel ou supposée à une structure, une somme de techniques orientées objet et fonctionnelles utilisées couramment dans la programmation que nous détaillerons au cas par cas à l'usage.
Considérons par exemple des éléments `f,g,h` appartenant à une structure `S`. La clôture par composition de l'ensemble de ces trois éléments `f,g,h` se note en les plaçant entre crochets `"<"f,g,h">"`. C'est l'ensemble de tous les éléments engendrés par `{f,g,h}`.
Les crochets entourant des éléments ou ensembles d'éléments désignent la cloture par composition de ces éléments.
Étant donné un ensemble `A` inclus dans `S`, la clôture par composition de `A` se note `"<"A">"` et regroupe tous les éléments engendrés par `A` tandis que son complémentaire `S"-""<"A">"` regroupe tous les éléments non engendrés par `A`.
Une structure `K` est une sous-structure de `S` si et seulement si elle est incluse dans `S` et que sa loi de composition est égale à celle de `S` restreinte à `K`, et cela se note `K⊑S`. Ainsi, l'ensemble des sous-structure de `S` se note `{K "/" K"⊑"S}`. Les sous-structures sont les clôtures par composition des sous-ensembles, ce qui se note par :
`{K "/" K"⊑"S} = {"<"A">" "/" A"⊆"S}`
La clôture par composition `"<"A">"` constitue une sous-structure de `S`. C'est aussi l'unique plus petite sous-structure de `S` contenant `A`.
`"<"A">" = "@min" {K "/" A"⊆"K"⊑"S}`
L'opérateur `"min"` appliqué à une famille d'ensembles, retourne la sous-famille des ensembles minimaux par inclusion. L'arobase est utilisé pour convertir un ensemble par son contenu.
Le langage d'opérateurs place au centre des préoccupations mathématiques les deux notions clefs que sont la liberté des éléments et l'égalité des éléments, et permet de définir une troisième notion aussi importante que chacune des deux premières, qu'est l'indépendance des éléments.
On considère que des éléments sont indépendants entre eux si la sous-structure qu'ils engendrent ne peut pas être engendrée en en retirant un. Chaque élément doit apporter une contribution nécessaire. Un ensemble `A` d'éléments est dit indépendant si et seulement si aucun de ses éléments n'est engendré par les autres. Sinon on remarque que l'on pourrait enlever cet élément `x` qui est engendré par les autres, sans que cela ne change la sous-structure engendrée
`x "∈<"A"-"{x}">" <=> "<"A">=<"A"-"{x}">"`
Etant donné une structure `S`. L'ensemble des parties de `S` se note `ccP(S)`.
On appelle une famille ou famille d'ensembles, un ensemble d'ensembles. Et on appelle membre d'une famille, les ensembles qui appartiennent à la famille en question. Les ensembles considérés sont les parties de `S`. Les familles considérées sont les parties de `ccP(S)`. On définie parmis l'ensemble de toutes les familles `ccP(ccP(S))`, les familles suivantes :
La famille des générateurs se note `bbbG`. Un ensemble est dit générateur s'il engendre la structure `S` par clôture par composition.
`bbbG = {A"⊆"S "/" "<"A">=" S}`
La famille des dépendants se note `bbb"D"`. Un ensemble est dit dépendant s'il possède un élément qui peut être engendré par les autres.
`bbb"D" = {A"⊆"S "/" EEx "∈" A, x "∈<"A"-"{x}">"}`
La famille des indépendants se note `bbb"I"`. Un ensemble est dit indépendant si aucun de ses éléments ne peut pas être engendré par les autres.
`bbb"I" = {A"⊆"S "/" AAx "∈" A, x"∉<"A"-"{x}">"}`
La familles des bases se note `bbb"B"`. Une base est un ensemble qui est à la fois un générateur et un indépendant.
`bbbB = bbbI nn bbbG`
Récapitulatif :
On dit alors qu'un élément `e` est dépendant d'un ensemble `A` si et seulement si `e` appartient à `A` ou bien que `A+{e}` constitue un ensemble dépendant. Autrement dit `e` est dépendant de `A` si et seulement si `e` est engendré par `A` ou s'il peut se substituer à un élément de `A` pour toujours être capable d'engendrer `A`. c'est à dire qu'il existe un élément `a` de `A` qui est engendré par `A-{a}+{e}`. La relation de dépendance entre un élément `x` est un ensemble `A` se note `x"←"A`. C'est une relation plus large que la relation d'engendrement :
`x"←"A <=> x"∈<"A">" "ou" EEa "∈" A, a "∈<"A"-"{a}"+"{e}">"`
Et par négation, on dit qu'un élément `e` est indépendant d'un ensemble `A` si et seulement si `e` n'appartient pas à `A` et que `A+{e}` constitue un ensemble indépendant. Autrement dit `e` est indépendant de `A` si et seulement si `e` n'est pas engendré par `A` et qu'aucun élément `a` de `A` n'est engendré par `A-{a}+{e}`. La relation d'indépendance entre un élément `x` est un ensemble `A` se note `x"↚"A`. C'est une relation plus fine que la relation de non engendrement :
`x"↚"A <=> x"∉<"A">" "et" AAa"∈" A, a "∉<"A"-"{a}"+"{e}">"`
On note que la relation de dépendance entre un élément `x` est un ensemble `A` est une relation plus large que la relation d'engendrement, et sa négation, la relation d'indépendance entre un élément `x` est un ensemble `A`, est une relation plus fine que la relation de non engendrement :
`x"∈<"A">" => x"←"A`
`x"↚"A => x"∉<"A">"`
Le matroïde est une structure logique formelle, introduite par H. Whitney en 1935, qui généralise la relation de dépendance linéaire en ne retenant que ses propriétés ensemblistes, à savoir, les 3 propriétés suivantes définissant la famille des ensembles indépendants :
Le matroïde est définie par un couple `(E,bbbI)`. Il comprend un ensemble sous-jacent `E`, et une famille d'ensembles `bbbI"∈"ccP(ccP(E))` qui regroupe tous les indépendants. La relation de dépendance du matroïde se définie de `E` vers `ccP(E)`. Un élément `x` est dépendant d'un ensemble `A`, notée `x"←"A` , si et seulement si il appartient à `A` ou bien `A"+"{x}` est dépendant :
`x"←"A <=> x"∈"A "ou" (A"+"{x})"∉"bbbI`
La structure `(S, bbbI)` est un matroïde si et seulement si elle vérifie :
`Ø "∈" bbbI`
`AAX AAY, (X "∈" bbbI "et" Y"⊆"X) => Y"∈"bbbI`
`AAX AAY, (X"∈" bbbI "et" Y "∈" bbbI "et" |X|">"|Y|) => (EEe, e"∈"X "et" e "∉"Y "et" Y"+"{e}"∈"bbbI)`
Dans l'expression de ces 3 propriétés, les quantifications couvrent `ccP(S)` lorsque la variable est en majuscule, et couvrent `S` lorsque la variable est en minuscule. Autrement dit, les variables majuscules `X` et `Y` sont des parties de `S` et la variable minuscule `e` est un élément de `S`.
Dans une structure quelconque `S`, la relation de dépendance est dite génétique si et seulement si elle coïncide avec la relation d'engendrement :
`AAx"∈"S AAA"∈"ccP(S), x"←"A <=> x"∈<"A">"`
C'est à dire si et seulement si pour tout élément `x"∈"S` et pour tout ensemble `A"∈"ccP(S)`, l'élément `x` est dépendant de `A` si et seulement si il est engendré par `A`. La relation de dépendance est génétique si et seulement si dans tout ensemble dépendant, chaque élément est engendré par les autres :
`AA A"∈"ccP(S), (EEx"∈"A, x"∈<"A">") => (AAx"∈"A, x"∈<"A">")`
Dans une structure `S`, la relation de dépendance est génétique si et seulement si la relation de dépendance est celle d'un matroïde `(S, bbbI)`.
`AA A"∈"ccP(S), (EEx"∈"A, x"∈<"A">") => (AAx"∈"A, x"∈<"A">")`
`<=>`
La structure `(S, {AsubeS "/" AAx "∈" A, x"∉<"A "-"{x}">"})` est un matroïde
Du point de vue élémentarien, tous les matroïdes peuvent se définir ainsi. Il existe un moyen de construire une structure à partir d'un matroïde `(E,bbbI)`, c'est à dire de construire une loi de composition de `E"×"E"→"E` telle que `bbbI = {AsubeE "/" AAx "∈" A, x"∉<"A"-"{x}">"}`
On appelle une famille ou famille d'ensembles, un ensemble d'ensembles. Et on appelle membre d'une famille les ensembles qui appartiennent à la famille en question. Les ensembles considérés sont les parties de `S`. Les familles considérées sont les parties de `ccP(S)`. On utilise couramment 6 opérateurs sur `ccP(ccP(S))` dont voici une courte description.
Étant donné une famille quelconque `bbbF` :
La famille `"sup"(bbbF)` regroupe tous les ensembles contenant au moins un membre de `bbbF`. C'est la clôture par agrandissement de `bbbF`. Une famille invariante par l'opérateur `"sup"` est dite close par agrandissement.
La famille `"sub"(bbbF)` regroupe tous les ensembles contenus dans au moins un membre de `bbbF`. C'est la clôture par inclusion de `bbbF`. Une famille invariante par l'opérateur `"sub"` est dite close par inclusion.
La famille `"max"(bbbF)` regroupe les membres maximaux c'est à dire qui ne sont contenues strictement par aucun membre. C'est la maximalisation de `bbbF`. Une famille invariante par l'opérateur `"max"` constitue une frontière.
La famille `"min"(bbbF)` regroupe les membres minimaux c'est à dire qui ne contiennent strictement aucun membre. C'est la minimalisation de `bbbF`. Une famille invariante par l'opérateur `"min"` constitue également une frontière.
La famille `"¬"(bbbF)` regroupe les ensembles qui ne sont pas membres de `bbbF`. C'est la négation de `bbbF`.
La famille `"∁"(bbbF)` regroupe toutes les négations de ses membres. C'est le complément de `bbbF`.
Récapitulatif :
Opération |
Description |
Définition formelle de l'opération |
`"sup"(bbbF)` |
Clôture par agrandissement. | `"sup"(bbbF) = {X "/" EEA"∈"bbbF, A"⊆"X}` |
`"sub"(bbbF)` |
Clôture par inclusion. | `"sub"(bbbF) = {X "/" EEA"∈"bbbF, X"⊆"A}` |
`"max"(bbbF)`
|
Maximalisation | `"max"(bbbF) = {X "/" X"∈"bbbF "et" AAF"∈"bbbF, X"⊄"F}` |
`"min"(bbbF)`
|
Minimalisation | `"min"(bbbF) = {X "/" X "∈"bbbF "et" AAF"∈"bbbF, F "⊄"X}` |
`¬(bbbF)` |
Négation | `"¬"(bbbF) = {X "/" X "∉"bbbF}` |
`"∁"(bbbF)` |
Complément | `"∁"(bbbF) = {E"-"X "/" X "∈"bbbF}` |
Propriété |
Description |
Définition formelle de la propriété |
`bbbF "=sup"(bbbF)` |
Clos par agrandissement | `AAX "∈" bbbF, AAY"/"X"⊆"Y, Y"∈" bbbF` |
`bbbF "=sub"(bbbF)` |
Clos par inclusion | `AAX "∈" bbbF, AAY"/"Y"⊆"X, Y"∈" bbbF` |
`bbbF "=max"(bbbF)` |
Frontière | `AAX"∈"bbbF,AAY"∈"bbbF,X"⊄"Y` |
`bbbF "=min"(bbbF)` |
Frontière | `AAX"∈"bbbF,AAY"∈"bbbF,X"⊄"Y` |
Notez que `AA Y` signifie `AA Y"⊆"S`.
Notez que le symbole `"⊂"` dénote l'inclusion stricte et donc que nous avons `AA Y, Y "⊄"Y`.
Nous avons les propriétée suivantes :
L'élément est plus générale que le terme. Le terme désigne l'élément. Le terme fait parti d'un langage. L'élément fait partie d'une structure. Le langage est une structure particulière dite libre. L'application, qui associe chaque terme à l'élément qu'il désigne, possède une propriété remarquable. Elle respecte les lois de composition. C'est à dire qu'une composition d'éléments désignés par des termes produira l'élément désigné par le terme résultat de l'emboitement des termes correspondants. Les applications entre deux structures, qui respectent les lois de composition, sont appellées des morphismes.
Un morphisme `f` est une application de `S->K`, où `S` et `K` sont deux structures quelconques, qui respecte les lois de compositions respectives c'est à dire :
`AA (a,b)"∈"S^2, S(a,b) = K(f(a),f(b))`
Ce qui se note en langage alpha par :
`AA (a,b)"∈"S^2, a_S(b) = f(a)_K(f(b))`
Et on le note sans répéter les noms des lois de compositions qui sont déterminés sans ambiguités par le contexte :
`AA (a,b)"∈"S^2, a(b) = f(a)(f(b))`
Si le morphisme est injectif c'est à dire tel que :
`AA (a,b)"∈"S^2, a"≠"b => f(a)"≠"f(b)`
Alors il constitue un plongement. C'est une forme abstraite d'inclusion. `S` est isomorphe à `f(S)` qui est une sous-structure de `K`. Ce qui se note :
`S↪_fK`
ou aussi :
`S~=f(S)subeK`
La notation pour désigner les différents types d'ensembles de morphismes est la même que celle pour désigner les différents types d'ensembles d'applications. Il est laissé au contexte le soin de lever l'ambiguité à savoir si on parle d'ensemble de morphismes ou d'ensemble d'applications. Ainsi, si `A` et `B` sont chacun muni d'une loi de composition, ou autremement dit, si `A` et `B` sont deux structures, alors nous avons :
d'application
de morphisme`A->B` désigne l'ensemble des morphismes de `A` vers `B`.
`A->>B` désigne l'ensemble des constructeurs de `A` en `B`.
`A↪B` désigne l'ensemble des plongements de `A` dans `B`.
`A~=B` désigne l'ensemble des isomorphisme de `A` sur `B`.
Une relation `R` de `A` vers `B` est une application de `A"×"B"→"{0,1}`. Cette application peut être perçue comme une fonction caractèristique définissant un ensemble. La relation `R` est une partie de `A"×"B`. La relation `R` est un ensemble de couples.
`R in ccP(A"×"B)`.
Si `A` et `B` sont deux structures, alors on définie la structure produit `A"×"B` avec la loi de composition suivante :
`(a,b)(a"’",b"’") = (a a"’", b b"’")`
Les lois portent les même nom que leurs structures :
`(A"×"B)"("(a,b),(a"’",b"’")")" = (A(a,a"’"), B(b,b"’"))`
`(a,b)_(A"×"B)(a"’",b"’") = (a_A(a"’"), b_B(b"’"))`
`R` étant un ensemble de couples inclus dans la structure `A"×"B`, on peut en considérer la clôture par composition des couples dans la structure `A"×"B`, que l'on note `"<"R">"` et qui constitue une relation plus vaste.
Une relation `R` de `A` vers `B` est dite morphique, si est seulement si elle est close par composition de couples selon la loi `A"×"B`, c'est à dire, si et seulement si elle vérifie :
`AA(a,a"’")"∈"A^2, AA(b,b"’")"∈"B^2,(aRb" et "a"’"Rb"’") => (aa"’")R(b b"’")`
La notation pour désigner les différents types d'ensembles de relations morphiques est la même que celle pour désigner les différents types d'ensembles de relations. Cela complète le tableau précédent qui ne mentionnait que les relations applicatives. Et on laisse pareillement au contexte le soin de lever l'ambiguité, à savoir si on parle d'ensemble de relations morphiques ou d'ensemble de relations.
D'autre part, il ne faut pas confondre la clôture par composition des couples selon la loi `A"×"B` avec la clôture par composition des relations d'un ensemble de relations, et qui se note pareillement en entourant des relations ou ensembles de relations entre crochet `"<...>"`. Par exemple l'ensemble `{R}` qui ne comprend que la relation `R` admet une clôture par composition de relation qui se note également `"<"R">"` et qui ne constitue pas une relation mais un ensemble de relations :
`"<"R">"={R,R^2, R^3,...R^n,...}`
Et cela n'a d'intérêt que si `AnnB` n'est pas vide. Pour rappel nous avons :
`R^2 = {(a,b) "/" EEc, aRc "et" cRb}`
----1 septembre 2019 ----
Il existe un type de structure particulière qu'est la structure libre, qui coïncide avec le langage d'opérateurs et qui s'obtient grace à la clôture par emboitement. Exemple :
`Omega = {f,g,h}^•`
`Omega` est une structure libre. La loi de composition générale est l'emboitement `Omega`, et c'est un emboitement labelisée `Omega`. De la même façon qu'il est possible de créer des éléments nouveaux, il est possible de créer des structures libres nouvelles sur de mêmes éléments générateurs, utilisant une loi générale de composition différente mais toujours basée sur le même principe de construction par emboitement. La différence tiendra dans le label, dans le nom de la loi et donc dans le nom de la structure qui porte le nom de la loi. Par exemple :
`Phi = {f,g,h}^•`
Ainsi par exemple le terme `f(g)(f,g(h))` se notera explicitement par `f_Omega(g)_Omega(f,g_Omega(h))` ou par `f_Phi(g)_Phi(f,g_Phi(h))` selon que la composition est faite dans `Omega` ou dans `Phi`. Assurement nous aurons :
`{f,g,h}sube Omega nn Phi`
Les structures libres sont complètement caractèrisées à isomorphisme près, par leur nombre minimum de générateurs, c'est à dire leur type, qui peut varier de `1` à `oo` compris. Les structures libres de type `oo` sont engendrée par une suite énumérable de générateurs. Pour chaque type on utilise une structure libre servant de modèle :
`Omega_1 = {1}^•` `Omega_2 = {1,2}^•`
`Omega_3 = {1,2,3}^•` `...` `Omega_oo = NN^•`
Quelque soit une structure `n`-gènes `S`, c'est à dire engendré par aux moins `n` générateurs, il existe toujours au moins un morphisme surjectif `s` de la structure libre à `n` générateur `Omega_n` vers `S` que l'on appelle le constructreur de `S` et qui est noté par la même lettre que la structure mais en minuscule. Il associe à chaque entier de `1` à `n`, les `n` générateurs de sa définition constructive.
`s : (({1,2,3,...,n}^•->> S), (1|->s(1)),(2|->s(2)),(3|->s(3)),(...),(n|->s(n)),(x(y"*")|->s(x)(s(y"*"))))`
Dans cette expression, `y"*"` désigne une suite finie d'éléments quelconque de `S`. Nous avons `y"*" = (a,b,c,...)`, et comme `s` appartient à `Omega_n->S`, l'expression `s(y"*")` s'interprète comme étant la suite `(s(a),s(b),s(c),...)`.
On démontre l'existence de ce morphisme surjectif, de la même façon que l'on construit `Omega_n`, c'est à dire de façon récurcive. Ce morphisme surjectif s'appel le constructeur. Chaque structure possède un constructeur qui convertie les éléments de la structure libre en ses éléments. Ce constructeur n'est en général pas unique. La structure libre modèle représente un langage d'opérateurs et constitue le langage de la structure. Les termes du langage sont les éléments de la structure libre modèle. Afin que le langage exprime autre chose que lui-même c'est à dire autre chose qu'une structure libre. On sépare le signifiant, du signifié. On sépare le terme `x` de l'élément qu'il désigne et que l'on note `s(x)`. C'est pourquoi le constructeur `s` porte le même nom que la structure `S` mais en minuscule. Les uns sont regroupés dans le langage, dans son univers `{1,2,3,...,n}^•` qui représente la clôture par emboitement des termes et qui constitue la structure libre modèle, les autres sont regroupés dans une autre structure, la structure liée, dans son ensemble sous-jacent notée `"<"s(1),s(2),s(3),...,s(n)">"` et qui représente la clôture par composition des éléments en son sein.
Et donc à posteriori, quelque soit une structure `n`-gènes `S`, et quelque soit `m>= n`, il existe toujours au moins un morphisme surjectif de `Omega_m->>S`. On appelle également ces morphismes des constructeurs de `S`.
Le constructeur `s` est surjectif, son image couvre son ensemble d'arrrivé. Le constructeur `s` est un morphisme, il respecte les compositions. C'est à dire que pour tout termes `x,y,z,t...` du langage, il respecte cette énumération de propriétés :
`s(x(y)) = s(x)(s(y))` `s(x(y,z)) = s(x)(s(y),s(z))` `s(x(y,z,t)) = s(x)(s(y),s(z),s(t))` `...`
Que l'on note comme suit :
`AAx"∈"Omega_n , AAy"*∈"Omega_n"*", s(x(y"*")) = s(x)(s(y"*"))`
ou avec ellipse :
`AA(x,y,z,t)"∈"Omega_n"×"Omega_n"×"Omega_n"×"Omega_n"×"..., s(x(y,z,t)) = s(x)(s(y,z,t))`
Et si `s` est injective, c'est à dire s'il vérifie :
`x!=y => s(x)!=s(y)`
Alors il est bijectif et constitue un isomorphisme. La structure est libre. Deux termes distincts désignent deux éléments distincts. Il n'est donc considéré aucune équivalence entre termes. Autrement dit la théorie d'égalité de la structure est vide. Et la structure est une copie à l'identique de son langage.
Le premier moyen de simplification consiste à ne considérer qu'une seul application d'arité variable, une loi de composition générale de la forme `S"*"->S`, et à considérer tous les éléments comme étant passifs c'est à dire d'arité nulle. Ce procédé, même s'il réduit toutes les aplications en une seule, n'est pas très intéressant car l'application restante reste toujours d'arité variables.
L'étude informatique du langage d'opérateurs nous amène à rechercher un codage dense des termes, ce qui est équivalent à rechercher une relation d'ordre totale sur l'ensemble des termes. Et en regardant la syntaxe du langage, on s'aperçoit qu'il existe deux opérations binaires de construction des termes. La première correspond à la virgule et est une opération associative qui construit les listes d'opérandes. Elle ajoute des termes dans une séquence de termes qui doit servir d'opérandes. Et la seconde correspond à l'ouverture d'une parenthèse. C'est l'opération qui applique un terme sur une liste d'opérandes.
Ainsi un second moyen nous est apporté par l'analyse syntaxique du langage. Par le même procédé qui transforme un arbre quelconque en un arbre binaire, on peut redéfinir tout langage d'opérateurs d'arité variable en langage d'opérateurs d'arité fixe comprenant deux opérations que l'on présente sous forme de deux opérateurs binaires `+` et `**` avec comme théorie, l'associativité de l'opérateur `+`
Mais une liste de termes n'est pas un terme et ne fait donc pas partie du langage d'opérateurs. On contourne la difficulté en complétant le langage, en incorporant les listes finies d'au moins deux termes qui ne sont pas des listes, et que nous appellons séquences.
Délors, une séquence telle que par exemple `x,y,z` constitue un terme. Et la composition n'a plus besoin de prendre un nombre variable d'opérandes, un seul suffit, puisqu'il peut être à lui seul une séquence de termes. On définie une nouvelle axiomatique, un nouveau langage qu'est le langage d'opérateurs avec séquences.
L'axiomatique du langage d'opérateurs avec séquences est le suivant :
de l'axiomeTout opérateur est un identifiant et possède un nom unique sous forme d'un caractère. Tout opérateur est un terme. Toute liste finie d'au moins deux termes qui ne sont pas des listes forme un terme appelé séquence. Tout terme peut s'appliquer sur un terme appelé opérande pour produire un terme appelé résultat. L'application d'un terme sur une opérande produit un résultat qui est l'emboitement du terme initial appliqué au terme opérande.
L'axiomatique du langage d'opérateurs avec séquences s'obtient à partir de l'axiomatique du langage d'opérateurs en ajoutant un axiome, celui permettant de créer des séquences, et en modifiant l'axiome de composition rendant toute composition binaire, d'un terme appliqué à un terme.
------- 17 septembre 2017 -------
On définie l'opérateur binaire `**` qui applique un terme sur un autre, et l'opérateur binaire `+` qui construit les séquences de termes. Ainsi nous avons par exemple en considérant trois termes quelconque `x,y,z` :
`x**y= x(y)`
`(x**y)**z = x(y)(h)`
`x**(y**z) = x(y(h))`
`x**(y+z) = f(y,z)`
`(x+y)**z = (x,y)(z)`
Notez qu'une séquence d'un seul élément est égale à l'élément qu'il contient. Et que la séquence de plusieurs séquences est égale à la concaténation des séquences. De tel sorte qu'il existe une valuation entière qui asocie à chaque élément, la taille de la séquence applatie qu'il représente.
L'opérateur `+` est associatif :
`AA x,y,z "∈" S^3, (x"+"y)"+"z=x"+"(y"+"z)`
Le langage d'opérateurs avec séquences de présentation `L` se notera par `L^frs`. Ce langage est plus générale que le premier puisqu'il le contient. Tout se passe comme si nous avions ajouté un nouvel opérateur générateur `frs` pour construire les séquences et que nous avions adopté les axiomes suivants qui caractérise cet opérateur :
`AAx, frs(x)"="x`
`AAxAAy"*", x(frs(y"*"))"="x(y"*")`
Conclusion le langage `L^frs`, peut s'obtenir comme une structure à partir du langage `(Luu{frs})^•`, en le quotientant par la théorie `{`AAxAAy"*", frs(x)"="x`, x(frs(y"*"))"="x(y"*")}`. Ainsi il existe un traducteur que l'on note par une barre et qui est une application de : `(Luu{frs})^•->L^frs`
----- 12 Août 2017 -----
Par exemple Etant donné x,y,z des termes de L^
`bar(s(x,y,z) ) = (barx,bary,barz)
`psi( x(y) ) = psi(x)(s(psi(y)))
`psi(`L^¤ = L^• "/" {AAxAAy"*", x(y"*") "=" x(s(y"*"))}`
Puis on établit une autre traduction entre ce langage `L^¤` et le langage d'arité fixe de présentation suivante :
`<f, g, h, **"(.,.)", +"(.,.)"> "/" {"+"` est associatif`}`
ou bien de façon précise :
`{f_E, g_E, h_E, **_((E,E)"→"E), ⊕_((E,E)"→"E)} "/" {+` est associatif`}`
ou bien de façon encore plus explicite :
`{f,g,h,**,+} "/" {`
`f "∈" E, `
`g "∈" E, `
`h "∈" E, `
`** "∈" (E,E)"→"E, `
`+ "∈" (E,E)"→"E, `
`AA(x,y,z) "∈" E ^3 (x"+"y)"+"z"="x"+"(y"+"z)
`}`
Remarquez que dans la présentation d'une structure, on place la théorie au dénominateur. Et il y a deux niveaux de théorie, celle propre au langage qui décrit plus ou moins explicitement la dynamique de construction du langage et celle propre à la structure qui établit les égalités entre termes du langage.
Par exemple le terme (x,y,z(x))(x,y(y)) appartenant à L^¤ où x,y,z sont des termes L^¤, se traduit en le terme (x+y+(z**x))**(x+(y**y)) où x,y,et la traduction constitue une bijectionL^¤
Une présentation de structure regroupe une présentation d'un langage et une théorie d'égalité. En ce sens, une structure est un objet plus complet qu'un langage. Une structure comprend un langage. On évoquera souvent le langage d'une structure. Parcontre si on évoque la structure d'un langage, cela correspondra précisement à la structure composé de la présentation de ce langage et de la théorie d'égalité vide.
La présentation de la structure décrite précédement correspond à :
`{f_E, g_E, h_E, **_((E,E)"→"E), ⊕_((E,E)"→"E)} "/" {`
`f"⊕"x=fx,`
`g"⊕"x=gx,`
`h"⊕"x=hx`
`}`
ou bien de façon explicite :
`{f,g,h,**,+} "/" {`
`f "∈" E, `
`g "∈" E, `
`h "∈" E, `
`** "∈" (E,E)"→"E, `
`+ "∈" (E,E)"→"E, `
`AAx"∈" E, f"⊕"x=fx`
`AAx"∈" E, g"⊕"x=gx`
`AAx"∈" E, h"⊕"x=hx`
`}`
On étend le langage d'opérateurs aux liste non vide de termes.
Prenons par exemple le langage de présentation suivante :
`{f _(E uu E×E*"→"E), g_(E uu E×E*"→"E), h_(E uu E×E*"→"E)}`
ou bien de façon explicite :
`{f,g,h} "/" {f "∈" E^"+""→"E, g "∈" E^"+""→"E, h "∈" E^"+""→"E}`
Ce langage d'opérateurs d'arité variable peut être remplacé avantageusement par une structure basée sur un langage d'arité fixe comme suit : On définie l'opérateur binaire `**`, noté par absence de symbole, qui applique un terme sur un autre, et l'opérateur binaire `⊕` qui ajoute une opérande dans un terme appliqué à une liste d'opérandes. Ainsi nous avons par exemple :
`fg= f(g)`
`f(g)h = f(g)(h)`
`f(g)"⊕"h = f(g,h)`
On remarque que l'opération `f"⊕"g` n'est pas définie, et on la définie égale à `f(g)` pour que cela corresponde à l'ajout d'une opérande à la liste vide d'opérande d'un opérateur. Et donc on la définie égale à `fg`. Le cas se produit à chaque fois que le premier opérande de `"⊕"` est un opérateur générateur. Ainsi quelque soit deux termes `x,y` du langage, si `x` est un opérateur générateur alors `x"⊕"y=xy`. La présentation du langage d'opérateurs correspondante est :
`{f_E, g_E, h_E, **_((E,E)"→"E), ⊕_((E,E)"→"E)}`
ou bien de façon explicite :
`{f,g,h,**,+} "/" {`
`f "∈" E, `
`g "∈" E, `
`h "∈" E, `
`** "∈" (E,E)"→"E, `
`+ "∈" (E,E)"→"E, `
`}`
Une présentation de structure regroupe une présentation d'un langage et une théorie d'égalité. En ce sens, une structure est un objet plus complet qu'un langage. Une structure comprend un langage. On évoquera souvent le langage d'une structure. Parcontre si on évoque la structure d'un langage, cela correspondra précisement à la structure composé de la présentation de ce langage et de la théorie d'égalité vide.
La présentation de la structure décrite précédement correspond à :
`{f_E, g_E, h_E, **_((E,E)"→"E), ⊕_((E,E)"→"E)} "/" {`
`f"⊕"x=fx,`
`g"⊕"x=gx,`
`h"⊕"x=hx`
`}`
ou bien de façon explicite :
`{f,g,h,**,+} "/" {`
`f "∈" E, `
`g "∈" E, `
`h "∈" E, `
`** "∈" (E,E)"→"E, `
`+ "∈" (E,E)"→"E, `
`AAx"∈" E, f"⊕"x=fx`
`AAx"∈" E, g"⊕"x=gx`
`AAx"∈" E, h"⊕"x=hx`
`}`
Remarquez que dans la présentation d'une structure, on place la théorie au dénominateur. Et il y a deux niveaux de théorie, celle propre au langage qui décrit la dynamique de construction du langage et celle propre à la structure qui établit les égalités entre termes du langage.
Et il existe une traduction qui permet de passer d'un terme du premier langage à un terme du second langage et réciproquement, tel que cette traduction correspond à une bijection entre les deux structures. Par exemple dans le premier langage `f(f,g,h(f,g))` se traduit dans le second langage par `((ff)"⊕"g)"⊕"((hf)"⊕"g)`. On conclue donc que le langage d'opérateurs d'arité variable n'apporte pas de pouvoir d'expression plus important qu'un langage d'opérateurs d'arité fixe du moment que celui-ci posséde au moins deux opérateurs binaires. C'est pourquoi on se restreindra par la suite à n'étudier que les langages d'opérateurs d'arité fixe.
Notez que dans ce second langage d'opérateurs d'arité fixe, il existe des opérateurs binaires qui ne possèdent pas l'arité nulle et donc qui ne constituent pas des termes du langages et ne désignent donc pas des éléments de la structure quoique participant à la construction du langage. Et il existe des opérateurs n'ayant qu'une unique arité nulle et qui sont donc des termes du langage et qui désignent des éléments de la structure mais qui n'opèrent pas. Ils peuvent constituer des opérandes mais il n'opèrent pas.
Par convention d'écriture, on note l'application d'un terme `x` à une séquence `frs(y,z,t,...)` comme suit :
`x(frs(y,z,t,...)) = x(y,z,t)`
La règle s'écrit ne manière exacte par :
`AA x "∈" S, AAy"*∈" S"*", x(frs(y"*")) = x(y"*")`
Qu'est-ce qu'une théorie d'égalité ? nous ne répondrons pas tout de suite à cette question mais nous donnerons quelques éléments de construction. Le langage d'opérateurs va s'enrichire et donner naissance à un langage de proprosition qui nous permettra d'écrire bon nombre de théories d'égalité.
La première étape dans la construction de ce langage de proposition est l'égalité entre termes. Mais les propositions ne s'appliquent pas qu'a un langage d'opérateurs, elles doivent pouvoir s'appliquer à n'importe quelle structure `S`. C'est pourquoi on considère le langage d'opérateurs `S^•` et un évaluateur `s`
`s : ((S^•->> S), (t|->s(t)))`
L'évaluateur `s` évalue un terme `t` composé d'éléments de `S`, en un élément de `S`. Une théorie de dimension zéro, est un ensemble finie d'égalité entre terme `S^•`. Par exemple considérons trois éléments `f,g,h` appartenant à `S`. Et considérons la théorie `T` suivante :
`T = {f(g)"="h, g(f)"="h, f(h)(g)"="g, h(g)"="f}`
La théorie d'égalité `T` définie une relation d'équivalence sur `S^•` que l'on note de trois façons différentes :
`x=_Ty` `x=y [T]` `T|--x=y`
Deux termes `x` et `y` de `S^•` sont équivalents si et seulement si on peut passer de l'un à l'autre en appliquant une série de substitutions de sous-termes autorisées par la théorie `T`, c'est à dire ici les égalités énumérées par `T`.
Par exemple le terme `g(h(g))` est équivalent au terme `f(f(h)(g))`, ce qui se note de trois façons possibles :
`g(h(g)) =_T f(f(h)(g))` `g(h(g)) = f(f(h)(g)) [T]` `T|--g(h(g))"="f(f(h)(g))`
Cette expression signifie que la théorie `T` démontre l'égalité `g(h(g))"="f(f(h)(g))`.
La relation d'équivalence est transportée sur `S` par le morphisme surjectif `s` et on utilise la même notation avec les éléments de `S`.
Ainsi avons-nous présenté un type de théorie d'égalité que sont les théories d'égalité de dimension zéro, avec les règles de déduction suffisantes.
Une théorie est un ensemble fini ou énumérable de propositions. Et il n'y a pas de différence entre théorie et proposition. Car l'ensemble des parties énumérables de `NN` est énumérable.
Une partie de `NN` est énumérable s'il existe un programme qui l'énumère. Les programmes étant par principe de taille finie, il existe un énumérateur de tous les programmes. Et donc il existe un énumérateur de toutes les parties énumérables de `NN`.
Les élémentariens utilise les mêmes notations que celle de la théorie des ensembles de Zermelon, mais la signification change. Ainsi `ccP(NN)` représente l'ensemble des partie énumérable de `NN`.
Une bijection de `ccP(N)` vers `N` est un objet mathématique riche de paradoxes. Il révèle le versant informatique du théorème d'incomplétude de Godel qu'est l'impossibilité de prévoir dans le cas générale si un programme va s'arréter ou ne jamais s'arréter. Cantor construit une nouvelle partie de `NN` par le procédé de la diagonale de Cantor, en utilisant une fonction de choix qui n'est pas calculable, pour démontrer qu'il ne peut pas exister de telle bijection lorsque l'on admet l'axiome du choix, et ainsi démontre l'existence de la puissance du continu dans la théorie des ensembles de Zermelon. L'équivalent en logique intuitionniste ou élémentarienne prouve, par construction, l'existence de l'ensemble des parties énumérables de `NN`, qui est lui-même énumérable. L'axiome du choix est un moyen de construction supplémentaire. On peut concevoir des moyens de construction non calculables intermédiaires, plus faible que l'axiome du choix, qui n'opèrent une infinité de choix que dans un cas précis et d'une façon précise, plus précise qu'un choix libre mais moins précise qu'une fonction calculable, telle une fonction de choix non calculable pour un cas précis que la nature pourrait nous montrer par exemple. L'opinion de church ne concerne que les fonctions calculables. Au delà, cette opinion ne s'applique pas.
Le langage de propostition choisie crée un ensemble énumérable de toutes les propositions possibles et qui correspond exactement à l'ensemble de toutes les théories possibles exprimable dans ce langage. On crée une structure `S` sur cet ensemble des propositions en le dotant d'une loi de composition telle que un élément `b` est engendré par `a` ce qui se note `b"∈<"a">"`, si et seulement si `a` démontre `b` ce qui se note `a"⊢"b`.
Puis on transcrit dans la structure les principes de base du raisonnement en procédant par étape. On ajoute l'opération de conjonction notée `et"(...)"` et les 5 axiomes :
| L'opérateur et`"(.,.)"` est invariant : | `A "et" A = A` |
| L'opérateur et`"(.,.)"` est commutatif : | `A "et" B = B "et" A` |
| L'opérateur et`"(.,.)"` est associatif : | `A "et" (B "et" C) = (A "et" B) "et" C` |
| Définition de la théorie vide `Ø` : | `A "et" Ø = A` |
| Démontrabilité du contenu : | `A in "<"A "et" B">"` |
paradigme conjonctif .... ddddd
Puis on définie la conjonction. C'est une application notée `"et"(...)` devant vérifier les deux propriétés suivantes :
`"et" : ((ccP(S)->S),(A|->ET_(x in A) x ))`
`"et"({}) = Ø`
`"et"({x}) = x`
`"et"(S) = "⊥"``"<"Ø">" = {Ø}`
`"<"⊥">" = S`
C'est la notion générale d'engendrement qui définie la notion générale de déduction. Ce qui est déduit logiquement est engendré dans la structure `S`.
Chaque proposition est un élément de la structure `S`. Ainsi `S` est l'ensemble de toutes les propositions exprimables. `S` représente un langage de propriété choisi.
La pré-logique est une logique sans négation. La négation, en tant qu'application qui permet d'écrire la négation d'une proposition et donc de la construire, n'est pas encore présente. Une théorie `T` pré-logique est équivalent à une grammaire, elle ne connait pas la négation mais va engendrer une partie de la structure :
`"<"T">⊆" S`
Néanmoins l'incohérence est définie comme la capacité de tout démonter. Une théorie `T` est incohérente si et seulement si `T` démontre toutes les propositions c'est à dire si elle engendre `S`.
`T` incohérente `<=> "<"T">=" S`
Définition du faux et du vrai `"⊥","⊤"`
Pour que notre étude soit celle de la logique et non seulement celle des langages, il faut ajouter les valeurs de vérité vrai et faux, et ce qu'est la négation, une symétrie qui permet de passer de l'une à l'autre, c'est à dire la capacité totale de dire « non ».
Il existe un moyen intérieur au langage pour définir de façon absolue, le faux, grâce au concept d'incohérence. Une théorie `T` est dite incohérente si et seulement si `T` démontre tout, `"<"T">"=S`. Et donc elle est dite cohérente si et seulement si il existe au moins une proposition `A` que `T` ne peut pas démontrer `T⊬A`.
On définie le faux comme une proposition incohérente, et on définie le vrai comme une proposition nécessaire. Ainsi nous avons :
Une proposition sera dite fausse si et seulement si elle démontre tout.
Une proposition sera dite vrai si et seulement si elle est démontrée par toute proposition.On définie la proposition `"⊥"` avec comme seul définition d'être fausse c'est à dire telle que quelque soit une proposition `A`, la proposition `"⊥"` démontre la proposition `A`, ce qui se note :
`AA A, "⊥⊢"A`
`"<"⊥">"=S`
On définie la proposition `"Ø"` avec comme seul définition d'être vrai c'est à dire telle que quelque soit une proposition `A`, la proposition `A` démontre la proposition `"Ø"`, ce qui se note :
`AA A, A"⊢⊤"`
`AA A, Ø in "<"A">"`
La proposition vide `Ø` est démontrée par toutes les propositions, et la proposition pleine `S` démontre tous les autres propositions. Donc nous avons :
`"⊥"= S`
`"⊤"= Ø`Au stade pré-logique, il existe donc déjà le vrai et le faux.
`AA A, "⊥⊢"A` `AA A, A"⊢⊤"` `"<⊥>"=S` C'est l'ensemble des propositions. `"<⊤>"` C'est l'ensemble des tautologies. `AA A, "<"A">" sub "<⊥>"` `AA A, "<⊤>" sub "<"A">"` Le faux `"⊥"` est ainsi défini intérieurement au langage comme étant l'incohérence, et représente la borne supérieure d'un treillis.
Le vrai `"⊤"` est ainsi défini intérieurement au langage comme engendrant le nécessaire c'est à dire l'ensemble des tautologies, et représente la borne inférieure d'un treillis.
Conventionellement, l'expresssion `"⊢"A` correspondra à l'expression `Ø"⊢"A`. Et comme la proposition vide correspond à la proposition vrai notée `"⊤"`, l'expression `"⊢"A` correspondra à l'expression `"⊤⊢"A`.
Puis on définie la négation. C'est une application notée `¬(.)` devant vérifier les deux propriétés suivantes ::
`¬ : ((S->S),(x|->¬x))`
`AA x, ¬¬x=x`
`AA x, "<"x,¬x">"=S`
On modélise les théories pré-logiques comme suit :
- Chaque proposition est un élément de la structure `S`.
- Un ensemble fini de propositions correspond à la conjonction des propositions et est donc égale à une proposition.
- Une théorie est un ensemble énumérable de propositions.
- Etant donné une théorie `T`, la cloture par composition `"<"T">"` est l'ensemble de toutes les propositions démontrables par la théorie `T`.
- La théorie `T` est incohérente si et seulement si elle démontre tout, c'est à dire si et seulement si `"<"T">"=S`.
A ce stade, nous avons défini une pré-logique. Elle est dite pré-logique car la négation, en tant qu'application qui permet d'écrire la négation d'une proposition et donc de la construire, n'est pas encore présente. Néanmoins l'incohérence est définie comme démontrant tout