La quantification « Quelque soit `x` nous avons ... » ou « Il existe `x` tel que ... », ce qu'elle signifie précisément, est une question majeure de la philosophie logique.
Le langage logique du premier ordre n'utilise qu'un seul type de variable, d'où son nom de « premier ordre ». Et ce type de variable est le type élément. Une variable `x` désigne un élément. Mais une difficultée persiste. C'est que la variable `x` ne désigne pas un élément parmi un ensemble d'éléments pré-établi, où l'ensemble en question satisferait une théorie des ensembles..., elle désigne un élément parmi quelque chose de plus vaste qu'un ensemble d'éléments et que nous appelons la catégorie des éléments.
Cette catégorie des éléments se définie par la potentialité du langage et par la potentialité du démonstrateur. Pour quelle raison ? parceque qu'il est inutile de chercher à exprimer ce qui par principe ne peut pas s'exprimer, ni à démontrer ce qui par principe ne peut pas se démontrer. Cette potentialité se traduit par le choix des mondes dénombrables que l'on peut construire à l'aide d'une infinité énumérable d'extensions élémentaires pour réaliser les théories du premier ordre valides, ce qui est toujours possible grâce au théorème de Löwenheim-Skolem. L'infini potentiel représente la capacité infinie de construction et de démonstration de l'homme, et c'est le plus petit des infinis que l'on nomme de façon savante, aleph, `aleph`, et qui est le cardinal de `NN`.
En optant pour une option philosophique matérialiste davantage exigente comme quoi il ne peut exister d'infini dans notre univers, on est en droit de se demander s'il n'existe pas une sémantique plus pertinente associée à un théorème équivalent à celui de Löwenheim-Skolem mais restreint aux seuls mondes finies ?
Les élémentariens ne franchissent pas le pas, mais formalisent l'infini potentiel. Ils définissent la sémantique d'une théorie comme étant l'ensemble des mondes, pouvant être infinis, mais de quantité d'information finie, satisfaisant la théorie en question. Ils intègrent donc bien l'infini dans la construction des mondes, mais en gardant une exigence de finitude sur la quantité d'information, et formalisent ainsi la notion d'infini potentiel.
Un langage logique du premier ordre se définit en présentant un ensemble `L` d'opérateurs non instanciés mais d'arité définie et un ensemble `M` de prédicats non instanciés mais d'arité définie, auxquels on ajoute le prédicat binaire d'égalité `"="` qui, lui, est déjà instancié d'une certaine façon et joue un rôle spécial exposé plus loin.
Le premier ordre impose qu'il n'existe qu'un seul type d'élément variable. Ainsi une variable `x` désigne un élément. Dire que cet élément n'est pas limité à un ensemble signifie qu'il est limité à un ensemble `E` non encore instancié (où ce que l'on entend par ensemble, satisfait une théorie du second ordre avec quelques variantes possibles). On décompose ainsi le caractère variable de la variable `x`. Elle désigne un élément inconnue appartenant à `E`, et la variable `E`, qui constitue une variable du second ordre, désigne un ensemble inconnue. Puis comme nous nous intéressons aux seuls structures qui constitue des ensembles, l'ensemble `E` constitue alors l'ensemble sous-jacent de la structure, qui est associée au langage. Et ainsi une première instantiation s'est opérée, celle du choix de cet ensemble sous-jacent pris comme paramètre.
Les opérateurs `n`-aire agissent sur cet ensemble `E` c'est à dire sont de type `E^n"→"E`. Et les opérateurs zéro-aire sont de type `E` c'est à dire désignent des éléments de `E`.
La notion d'opérateur peut se généraliser et englober celle de prédicat, et dans cet esprit, un prédicat est simplement un opérateur de type différent. Les prédicats `n`-aire sont de type `E^n"→"{0,1}`. Et les prédicats zéro-aire sont de type booléen, `{0,1}`, c'est à dire désignent des valeurs booléennes.
Un opérateur non instancié signifie qu'il ne possède aucune définition autre que son type caractérisé par son ensemble de départ et son ensemble d'arrivé. Et donc, un opérateur non instancié se comporte comme un opérateur inconnu que l'on évoquerait pour la première fois. Les espaces de nom permettent d'utiliser un même symbole pour désigner des éléments différents selon où est placé le symbole. Ainsi lorsque l'on déclare un langage en désignant des opérateurs, ceux-ci sont par définition considérés non instanciés, c'est à dire comme n'ayant jamais été utilisés avant. Et cela s'obtient en créant un espace de nom qui va masquer les espaces parents.
Conventionnellement les opérateurs sont notés en minuscule et les prédicats en majuscule, et on précise leur type de deux façons courantes, soit par un suffixe indiquant l'arité ; absence de suffixe pour l'arité nulle, suffixe `"(.)"` pour unaires, suffixe `"(.,.)"` pour binaires, suffixe `"(.,.,.)"` pour ternaire, etc., soit par un type explicite plaçé en exposant.
Par exemple considérons le langage suivant défini par un ensemble d'opérateurs et un ensemble de prédicats :
`L = { a, f"(.)", g"(.,.)"} = {a, f^(E->E), g^(E->E->E) }`
`M = {A"(.)"} = {A^(E->{0,1}) }`
Le langage comprend un élément `a`, un opérateur unaire `f`, un opérateur binaire `g`, un prédicat unaire `A`, auquel on ajoute le prédicat binaire d'égalité `"="`. Le langage peut être présenté sous forme d'un ensemble d'opérateurs et de prédicats que l'on qualifie de générateurs, `{a, f, g, A}`.
Le langage veut signifier autre chose que lui-même. Une théorie écrite dans ce langage désignera un ensemble de mondes possibles. L'univers représente l'ensemble des mondes que peut désigner le langage. C'est la sémantique du langage.
Le langage logique du premier ordre comprend un langage plus simple appelé le langage des termes, ou domaine de Herbrand. Les termes du langage sont les compositions closes d'opérateurs générateurs et forment l'ensemble des éléments dits calculables. Ils forment le domaine de Herbrand qui désigne tous les éléments calculables, et qui constitue la structure libre du langage, un monde canonique nu et infini. On le note entre crochet, ou bien à l'aide du symbole de cloture qui est le petit rond en exposant `°` :
`"<"L">" = "<"a, f, g">" = {a, f, g}"°" = L"°"`
`"<"L">" = " {a, f(a), g(a,a),f(f(a)),g(f(a),a), g(a,f(a)),...}`
Les termes forment le squelette de l'univers associé au langage.
La composition d'un prédicat générateur ou du prédicat d'égalité, avec des termes, produit un littéral affirmatif. Ces littéraux constituent les briques élémentaires de l'univers, qui est associé au langage. Le produit `"<"L">" (M "∪" {"="})` en notation française, désigne les compositions des prédicats appartenant à `M "∪" {"="}` avec des termes appartenant à `"<"L">"`. C'est l'ensemble des littéraux affirmatifs.
`{A(a), A(f(a)), a"="a, a"="f(a), A(g(a,a)), f(a)"="f(a), g(a,a)"="a, f(a)"="g(a,a), ...}`
L'ensembles des littéraux s'obtient en ajoutant leur négation :
`{A(a), "¬"A(a), A(f(a)), "¬"A(f(a)), a"="a, a"≠"a, a"="f(a), a"≠"f(a), A(g(a,a)), "¬"A(g(a,a)), ...}`
Les prédicats restreint à l'ensemble sous-jacent, désignent des ensembles. Le prédicat `A` désigne un ensemble que nous nommons avec le même nom. De cette façon nous définissons un nouvel opérateur dit d'appartenance `"∈"`, et l'expression logique `A(x)` est équivalente à `x"∈"A`, et l'expression logique `"¬"A(x)` est équivalente à `x"∉"A`. Mais on n'ajoute pas cet opérateur au langage de la structure, on l'utilise uniquement par commodité comme seconde écriture.
La détermination booléenne de tous les littéraux affirmatifs va déterminer précisément un monde. Mais dans le cas infini, cette détermination n'est pas toujours totalement calculable.
On considére six opérations binaires booléennes, appellées connecteurs booléens.
`x` `y` `x"⇔"y` `x"⇒"y` `x"⇍"y` `x "et" y` `x "ou" y` `x "⇎" y` 0 0 1 1 0 0 0 0 0 1 0 1 1 0 1 1 1 0 0 0 0 0 1 1 1 1 1 1 0 1 1 0
Afin d'éviter un usage trop intensif de parenthèses emboités, on fixe une priorité syntaxique à ces connecteurs selon l'ordre suivant :
`"⇔", "⇒", "⇍", "et", "ou", "⇎"`
L'égalité entre booléens est posé de priorité syntaxique inféieure à l'équivalence qui est posé inférieure à celle de l'implication et de la non implication réciproque qui sont inférieures à celle de la conjonction et de la disjonction qui sont inférieures à celle de l'alternative. Puis on fixe leur priorité syntaxique inférieure à celle de l'égalité entre termes, et aussi inférieure à celle de la négation.
`"=", "⇔", "⇒", "⇍", "et", "ou", "⇎", "=", "¬"`
Ainsi par exemple, considérons l'expression suivante :
`¬x "et" y⇎¬y⇒x`
Celle-ci correspond à :
`((¬x) "et" y)⇎((¬y)⇒x)`
On définie une symétrie sur les connecteurs binaires booléens, appelée dualité. Etant donné un connecteur `"∗"`, on définit son dual `hat"∗"` comme suit :
`¬(x "∗" y) = ¬x hat"∗" ¬y`
Connecteur Connecteur dual `"et"` `"ou"` `"⇒"` `"⇍"` `"⇔"` `"⇎"`
Autrement dit nous avons :
`"¬"(x "et" y) <=> ¬x "ou" "¬"y`
`"¬"(x "ou" y) <=> ¬x "et" "¬"y``"¬"(x"⇒"y) <=> ¬x"⇍¬"y`
`"¬"(x"⇍"y) <=> ¬x"⇒¬"y``"¬"(x"⇔"y) <=> ¬x"⇎"¬y`
`"¬"(x"⇎"y) <=> ¬x"⇔"¬y`
D'autre part les connecteurs `"⇔", "⇎"` que l'on note parfois `"=", "≠"` sont dits "de logique symétrique" ou encore "de logique d'égalité", et satisfont :
`x"⇔"y<=> "¬"x"⇔¬"y`
`x"⇎"y<=> "¬"x"⇎¬"y``"¬"(x"⇔"y) <=> x"⇎"y`
`"¬"(x"⇎"y) <=> x"⇔"y`
La dualité établie les règles de déplacement de la négation vers les littéraux booléens. Il s'en suit, pour chaque connecteur associé à son dual, une notion d'engendrement et de forme spécifique, ne contenant pas de négation puisque déplacée dans les littéraux.
Cela définie deux formes, l'une composée que de `"et"`, de `"ou"` et de littéraux booléens, l'autre composée que de `"⇒"`, de `"⇍"` et de littéraux booléens.
Un système de traduction permet de passer d'une forme à l'autre. Le signe `->` correspond l'équivalence logique, mais précise en plus, un sens de la traduction souhaité :
Forme Règles de déplacement de la négation Traduction `{"et", "ou"}`
`"¬"(x "et" y)` `->``"¬"x "ou" "¬"y` `"¬"(x "ou" y)` `->``"¬"x "et" "¬"y`
`x"⇒"y` `->``"¬"x "ou" y` `x"⇍"y` `->``"¬"x "et" y` `{"⇒", "⇍"}`
`"¬"(x"⇒"y)` `->``"¬"x"⇍¬"y` `"¬"(x"⇍"y)` `->``"¬"x"⇒¬"y`
`x "et" y` `->``"¬"x"⇍"y` `x "ou" y` `->``"¬"x"⇒"y`
Forme Traduction de l'équivalence et de l'alternative `{"et", "ou"}`
`x"⇔"y` `->``(x "et" y) "ou" ("¬"x "et" "¬"y)` `x"⇎"y` `->``(x "ou" y) "et" ("¬"x "ou" "¬"y)` `x"⇔"y` `->``("¬"x "ou" y) "et" (x "ou" "¬"y)` `x"⇎"y` `->``("¬"x "et" y) "ou" (x "et" "¬"y)` `{"⇒", "⇍"}`
`x"⇔"y` `->``(x"⇒¬"y)"⇒"(x"⇍¬"y)` `x"⇎"y` `->``("¬"x"⇍"y)"⇍"("¬"x"⇒"y)` `x"⇔"y` `->``(x"⇍"y)"⇍"(x"⇒"y)` `x"⇎"y` `->``(x"⇒"y)"⇒"(x"⇍"y)`
D'autre part, les connecteurs `"et", "ou"` sont commutatifs, et les connecteurs `"⇒", "⇍"` sont anticommutatifs. Ainsi, nous avons les règles de tranformations suivantes :
`x "et" y -> y "et" x`
`x "ou" y -> y "ou" x``x"⇒"y -> "¬"y"⇒¬"x`
`x"⇍"y -> "¬"y"⇍¬"x`
Et la dualité assure que :
`x "et" y -> "¬"("¬"x "ou" "¬"y)`
`x "ou" y -> "¬"("¬"x "et" "¬"y)``x"⇒"y -> "¬"("¬"x"⇍¬"y)`
`x"⇍"y -> "¬"("¬"x"⇒¬"y)`
Les deux connecteurs booléens `"et", "ou"`, sont commutatif, associatifs et sont distributifs l'un par rapport à l'autre. Ces propriétés caractérises à une permutation près complètement ces connecteurs booléens.
Quelles sont les propriétés remarquables satisfaites par les deux autres connecteurs booléens `"⇒", "⇍"`, qui les caractèriseraient complètement à une permutation près ? (Voir les axiomes d'Hilbert).
L'ensemble des connecteurs de type `{0,1}^n→{0,1}` est obtenu par composition générale de connecteurs générateurs tel que `"¬", "et", "ou"`, ce que l'on note en utilisant le symbole de composition générale qui est l'étoile en exposant `{"¬", "et", "ou"}^"∗"`
L'ensemble des propositions sans quantificateurs s'obtient alors par le produit en notation française suivant :
`"<"L">" (M "∪" {"="}) {"¬", "et", "ou"}^"∗"`
C'est l'ensemble des connecteurs de type `{0,1}^n→{0,1}` composés avec des littéraux affirmatifs.
Le langage du premier ordre est un langage contextuel, c'est à dire que l'interprétation d'une sous-proposition `P` dépend du contexte où se trouve cette sous-proposition. Les contextes sont créés par des déclarations de variables, par exemple `x`, quantifiée soit universellement `AAx`, ou soit existentiellement `EEx`. Sous la porté du quantificateur, le langage utilisé est augmenté de la variable `x` en question (et si celle-ci est déjà utilisée alors elle est masquée par cette nouvelle variable homonyme). Les propositions utilisant cette nouvelle variable définissent des fonctions propositionnelles que l'on note sous forme fonctionnelle, fonction de la variable rajoutée au langage, c'est à dire ici `P(x)`. La proposition a alors l'une des formes suivantes :
`AAx, P(x)`
`EEx, P(x)`
Ainsi le quantificateur se présente comme un opérateur spécial à deux arguments. La virgule sépare les deux arguments. Le premier argument est le nom d'une nouvelle variable, et le second argument est une proposition écrite dans le langage augmenté de cette nouvelle variable et qui correspond donc à une fonction propositionnelle fonction de cette nouvelle variable.
On attribut une priorité syntaxique la plus faible au quantificateur vis-à-vis de son second argument. Autrement dit, la porté du quantificateur s'étend jusqu'à la fermeture d'une parenthèse ouverte avant le quantificateur. Ainsi par exemple, considérons l'expression suivante :
`T "et" AAx, Q(x) "ou" R(x) => EEy, S(x,y) "et" R(y)`
Cette expression signifie :
`T "et" (AAx, Q(x) "ou" R(x) => (EEy, S(x,y) "et" R(y)))`
Une proposition est dites sous forme prénexe si tout ses quantificateurs sont regroupés au début. Toute proposition admet une forme prénexe équivalente. Le langage logique permet facilement d'exprimer la forme prénexe d'une proposition, par un procédé récurcif, en appliquant des règles de déplacement des quantificateurs :
`"¬"AA x, P(x)` `->` `EE x, "¬"P(x)` `"¬"EE x, P(x)` `->` `AA x, "¬"P(x)`
`(AA x, P(x)) "et" Q` `->` `AA x, P(x) "et" Q` `(EE x, P(x)) "et" Q` `->` `EE x, P(x) "et" Q` `Q "et" (AA x, P(x))` `->` `AA x, P(x) "et" Q` `Q "et" (EE x, P(x))` `->` `EE x, P(x) "et" Q`
`(AA x, P(x)) "ou" Q` `->` `AA x, P(x) "ou" Q` `(EE x, P(x)) "ou" Q` `->` `EE x, P(x) "ou" Q` `Q "ou" (AA x, P(x))` `->` `AA x, P(x) "ou" Q` `Q "ou" (EE x, P(x))` `->` `EE x, P(x) "ou" Q`
On en déduit par traduction :
`(AA x, P(x))"⇒"Q` `->` `EE x, P(x)"⇒"Q` `(EE x, P(x))"⇒"Q` `->` `AA x, P(x)"⇒"Q` `Q"⇒"(AA x, P(x))` `->` `AA x, P(x)"⇒"Q` `Q"⇒"(EE x, P(x))` `->` `EE x, P(x)"⇒"Q`
`(AA x, P(x))"⇍"Q` `->` `EE x, P(x)"⇍"Q` `(EE x, P(x))"⇍"Q` `->` `AA x, P(x)"⇍"Q` `Q"⇍"(AA x, P(x))` `->` `AA x, P(x)"⇍"Q` `Q"⇍"(EE x, P(x))` `->` `EE x, P(x)"⇍"Q`
`(AA x, P(x))"⇔"Q` `->` `EEx,AAy,(Q "et" P(y)) "ou" ("¬"Q "et" "¬"P(x))` `(EE x, P(x))"⇔"Q` `->` `EEx,AAy,(Q "et" P(x)) "ou" ("¬"Q "et" "¬"P(y))` `Q"⇔"(AA x, P(x))` `->` `EEx,AAy,(Q "et" P(y)) "ou" ("¬"Q "et" "¬"P(x))` `Q"⇔"(EE x, P(x))` `->` `EEx,AAy,(Q "et" P(x)) "ou" ("¬"Q "et" "¬"P(y))`
`(AA x, P(x))"⇎"Q` `->` `EEx,AAy,(Q "ou" P(y)) "et" ("¬"Q "ou" "¬"P(x))` `(EE x, P(x))"⇎"Q` `->` `EEx,AAy,(Q "ou" P(x)) "et" ("¬"Q "ou" "¬"P(y))` `Q"⇎"(AA x, P(x))` `->` `EEx,AAy,(Q "ou" P(y)) "et" ("¬"Q "ou" "¬"P(x))` `Q"⇎"(EE x, P(x))` `->` `EEx,AAy,(Q "ou" P(x)) "et" ("¬"Q "ou" "¬"P(y))`
Voici un exemple de proposition sous forme prénexe :
`AAx, AAy, AAz, AAt, R(x,z) "et" R(z,y) "et" R(x,t) "et" R(t,y)) => "¬"R(z,t)`
Notez que la conjonction est associative et commutative et que la priorité syntaxique de la conjonction est supérieur à celle de l'implication
Cette proposition signifie textuellement : Quelque soit les sommets `x,y,z,t`, si le graphe `R` admet des arcs passant de `x` à `z` et de `z` à `y` et de `x` à `t` et de `t` à `y` alors il n'admet pas d'arc passant de `z` à `t`.
Le langage logique permet facilement d'exprimer la négation syntaxique d'une proposition, par un procédé récurcif, en inversant les quantificateurs `AA`, `EE` dans l'entête puis en négativant la fonction propositionnelle sur laquelle ils portent, ou bien en inversant les deux symboles `"et"`, `"ou"` et en négativant leurs arguments, ou bien en inversant les deux symboles `"⇔"`, `"⇎"` et en laissant inchangés leurs arguments, ou bien en remplaçant l'expressions de la forme `A"⇒"B` directement par `A "et" "¬"B`. Cela se définit formellement dans le langage logique utilisant les connecteurs booléens `¬`, `"et"`, `"ou"`, `"⇒"`, `"⇔"`, `"⇎"`, à l'aide de ces 8 règles de substitutions, où `x` représente une variable de nom quelconque, où `P(x)` représente une fonction propositionnelle quelconque appliquée à `x`, et où `Q` et `R` représentent des propositions quelconques :
`"¬"(AA x, P(x))` `->` `EE x, "¬"P(x)` `"¬"(EE x, P(x))` `->` `AA x, "¬"P(x)` `"¬"(A "et" B)` `->` `"¬"A "ou" "¬"B` `"¬"(A "ou" B)` `->` `"¬"A "et" "¬"B` `"¬"(A"⇒"B)` `->` `"¬"A"⇍¬"B` `"¬"(A"⇍"B)` `->` `"¬"A"⇒¬"B` `"¬¬"A` `->` `A` `"¬"(A"⇔"B)` `->` `A"⇎"B` `"¬"(A"⇎"B)` `->` `A"⇔"B`
Par exemple, reconsidérons notre proposition :
`AAx, AAy, AAz, AAt, R(x,z) "et" R(z,y) "et" R(x,t) "et" R(t,y)) => "¬"R(z,t)`
La négation s'obtient ainsi :
`¬AAx, AAy, AAz, AAt, R(x,z) "et" R(z,y) "et" R(x,t) "et" R(t,y) => "¬"R(z,t)`
`EEx, ¬AAy, AAz, AAt, R(x,z) "et" R(z,y) "et" R(x,t) "et" R(t,y) => "¬"R(z,t)`
`EEx, EEy, ¬AAz, AAt, R(x,z) "et" R(z,y) "et" R(x,t) "et" R(t,y) => "¬"R(z,t)`
`EEx, EEy, EEz, ¬AAt, R(x,z) "et" R(z,y) "et" R(x,t) "et" R(t,y) => "¬"R(z,t)`
`EEx, EEy, EEz, EEt, ¬(R(x,z) "et" R(z,y) "et" R(x,t) "et" R(t,y) => "¬"R(z,t))`
`EEx, EEy, EEz, EEt, R(x,z) "et" R(z,y) "et" R(x,t) "et" R(t,y) "et" "¬¬"R(z,t))`
`EEx, EEy, EEz, EEt, R(x,z) "et" R(z,y) "et" R(x,t) "et" R(t,y) "et" R(z,t)`
On choisie un système de déduction, c'est à dire l'ensemble des seuls règles syntaxiques que nous utiliserons pour construire les démonstrations.
Le langage veut signifier autre chose que lui-même. Et c'est le choix du système de déduction qui va déterminer ce qu'il désigne, qui va définir la sémantique du langage.
Le système de déduction se ramène toujours à un procédé mécanique, un programme qui énumère toutes les démonstrations. A partir de ce programme, on construit d'autres programmes :
Notez que les théories ou propositions, les démonstrations ainsi que les programmes sont par définition de taille finie.
On définit une logique étendue en introduisant un nouveau connecteur dit de déduction `"⊢"` et jouant un rôle spécial bien défini. Étant donnée une proposition `P` quelconque, l'expression `"⊢"P` signifie qu'il existe une démonstration de `P` avec notre système de déduction, autrement dit, que `P` est une tautologie, c'est à dire que notre système de déduction - l'énumérateur des tautologies - produit `P` en un temps fini.
Ce connecteur `"⊢"` est déterminé par le système de déduction choisi. Cela signifie que pour une proposition quelconque, la proposition étendue `"⊢"P` possède une valeur logique `0` ou `1` bien déterminée. Mais pour obtenir de façon sûr la valeur logique `0`, il peut arrivé qu'il soit nécessaire de se placer à la fin des temps, c'est pourquoi on dira plus précisement que le connecteur de déduction `"⊢"` est déterminé à la fin des temps par le système de déduction choisi.
Bien entendu si une telle démonstration de `P` existe, alors `P` est vrai, d'où l'axiome : `("⊢" P) => P`.
Par convention, on fixe la priorité syntaxique du connecteur de démonstration comme étant la plus faible. Ainsi, l'expression `⊢ P "et" Q` signifie `⊢(P "et" Q)`.
La proposition étendue `"¬"("⊢" P)` que l'on note par `"⊬"P` signifie qu'il n'existe pas de démontration de `P`. Et la proposition étendue `"¬"("⊢¬"P)` que l'on note `"⊬¬"P` signifie qu'il n'existe pas de démontration de `"¬"P`. Apparait alors les prémisses d'une logique ternaire :
On définie par commodité le connecteur d'indécidabilité `¿` comme suit. L'expression `¿P` signifie que `P` est indécidable c'est à dire qu'il n'existe pas de démonstration de `P` ni de démonstration de `"¬"P`. Par définition :
`¿P <=> ("⊬"P) "et" ("⊬¬"P)`
Notez que l'équivalence comme l'égalité entre booléens est définie avec une priorité syntaxique plus faible que les autres opérateurs faisant que dans cette expression il n'est pas utile d'entourer de parenthèse la conjonction.
Les propositions `"⊢"P, "⊢¬"P, ¿P` ont chacune à la fin des temps une valeur logique binaire `0` ou `1` bien déterminée. Et nous avons l'axiome trilogique suivant qui dit que pour toute proposition `P` nous avons toujours une et une seule expression vrai sur les trois, `"⊢"P , "⊢¬"P, ¿P`, les deux autres étant fausses. Ce constat fait apparaître les prémisses d'une logique ternaire. On définit la valeur ternaire d'une proposition `P` comme valant `0,1,oo` respectivement dans les cas `"⊢"P, "⊢¬"P, ¿P`
Pour des raisons assez simples à établir, décrites par Godel et Turing, toute théorie suffisament complexe pour contenir l'arithmétique est incomplète, c'est à dire qu'il existe toujours des propositions exprimables dans le langage de la théorie, qui sont indécidables. Et l'ensemble de ces propositions indécidables ne peut être énuméré. On peut bien en exhiber une infinité d'entre elles, mais il n'existe aucun programme capable de toutes les énumérés.
La définition du connecteur de déduction s'applique aussi aux propositions étendues. Ainsi, l'expression `"⊢"("⊢"P)` signifie qu'il existe une démonstration de l'existence d'une démonstration de `P`. Les démonstrations étant énumérables, nous avons l'équivalence `"⊢"("⊢"P) <=> ("⊢"P)` et donc `"⊬"("⊢"P) <=> ("⊬"P)`. Parcontre nous avons `"⊢"("⊬"P) => ("⊬"P)` mais la réciproque n'est pas valable. Si `P` n'est pas démontrable, il n'y a pas forcement de démonstration comme quoi `P` n'est pas démontrable. Car la non démontrabilité se traduit par une éxecution sans fin du programme de vérité qui ne peut donc constituer une démonstration puisque de taille non fini.
Qu'est ce que désigne une proposition `P` appartenant à un langage logique du premier ordre ? autrement dit qu'elle est sa sémantique ?. Pour répondre à cela, on définit la notion d'univers associé au langage, et la notion de monde qui est une instanciation de cet univers.
Dans le cas fini, l'univers se résume en un ensemble fini de mémoires contenant des valeurs booléennes que valent les littéraux affirmatifs du langage et qui forme une table de vérité. Les mondes considérés sont complets. Chaque littéral affirmatif doit y posséder une valeur booléenne `0` ou `1` qu'elle mémorise dans la table de vérité du monde. Le monde se définit donc comme une intanciation complète de l'univers, et dans lequel toute proposition `P` est nécessairement soit vérifiée ou soit infirmée. La logique est complète.
Dans le cas infini, comme il est matériellement impossible de considérer une mémoire infinie, celle-ci est remplaçée par une mémoire contenant un programme qui est par principe de taille finie. Et c'est ce programme qui détermine une infinité de valeurs et que l'on appelle programme de vérité. On choisit comme programme de vérité un énumérateur de proposition qui intègre dans son processus énumératif le système de déduction choisi, et qui possèdent la propriété de ne pas se contredire c'est à dire qui n'énumère jamais une proposition `P` et sa négation `"¬"P`. Notez que cette dernière contrainte constitue dans le cas général un oracle nécessitant un temps infini pour être vérifiée.
Dans cette approche purement mécanique, la seule à satisfaire les sceptiques, et encore, sur la base d'une mécanique classique, on définit l'univers calculable associé au langage comme étant l'ensemble des mondes calculables dont le programme de vérité peut calculer la valeur logique de toutes les propositions du langage. Mais le calcul peut ne pas s'arréter, et produire une valeur oracle qu'est l'infini de Turing `oo`. L'adjectif calculable ne veut pas dire totalement calculable. La vérité s'obtient par un calcul mais celui-ci peut ne pas s'arréter et ne jamais donner de réponse. La conséquence de cela est qu'un monde calculable engendre une logique ternaire où toutes propositions `P` possède trois états exclusif et exhaustif que sont : `"⊢"P , "⊢¬"P, ¿P`, et qui correspond à la valeur ternaire de la proposition P parmi `{0,1,oo}`.
Dans un monde calculable, chaque proposition `P` du langage y possède une valeur ternaire `0` ou `1` ou l'infini de Turing `oo`, déterminés par le programme de vérité, sachant que l'infini de Turing correspond au cas où le programme de vérité ne s'arrête pas et ne donne jamais de réponse. Le monde se définit ainsi comme une instanciation de l'univers par un programme de vérité, et dans lequel donc toute proposition est calculable par le programme de vérité c'est à dire, vérifiée s'il retourne `1`, infirmée s'il retourne `0` et indécidé s'il retourne `oo`.
Notez que le programme de vérité du monde constitue la théorie du monde, que l'éxecution du programme de vérité appliqué à une proposition `P` et retournant `1` constitue une démonstration de `P`, que l'éxecution du programme de vérité appliqué à une proposition `P` et retournant `0` constitue une démonstration de `"¬"P`, mais que parcontre l'éxecution du programme de vérité appliqué à une proposition `P` et ne s'arrétant jamais, c'est à dire produisant l'infini de Turing `oo`, ne constitue pas une démonstration de `¿P` car une démonstration doit être de taille finie.
La définition des mondes calculables définit une nouvelle logique dite incomplète ou ternaire, dans laquelle chaque propositions `P` a une valeur logique ternaire parmi `{0,1,oo}`. Les mondes incalculables, eux, tranchent la question en effectuant une infinité de choix arbitraires afin de compléter la théorie et le monde, faisant que toutes propositions est soit vrai ou soit fausse, et possède donc une valeur logique binaire parmi `{0,1,oo}`.
Si on n'exige pas la cohérence du système de déduction, c'est à dire que celui-ci devient un système de production quelconque intégrant le système de déduction et pouvant se contredire. Alors on associe à toutes proposition du langage, les deux valeurs booléennes que sont `"⊢"P` et `"⊢¬"P`, proposant ainsi 4 alternatives exclusives. L'alternative supplémentaire ajoutée à la trilogie précédement décrite, est le cas `("⊢"P) "et" ("⊢¬"P)` qui indique que le système de déduction est incohérent relativement à `P`.
Tous se passe comme s'il existait un monde calculable incomplet et un monde incalculable qui le complète. On définie la valeur logique ternaire d'une proposition `P` comme égale à une valeur ternaire parmi `{0,1,oo}` selon le cas `"⊢"P, "⊢¬"P, ¿P`. Et on définit la valeur logique binaire de la proposition `P` comme égale à une valeur ternaire parmi `{0,1}` selon le cas `P, "¬"P`.
Pour éviter les confusions on utilisera le signe `"=="` pour indiquer que c'est la valeur trilogique qui est considérée.
Expression Egalité logique et trilogique `P` `P=1` `"¬"P` `P=0` `"⊢"P` `P "==" 1` `"⊢¬"P` `P "==" 0` `¿P` `P "==" oo`
Dans une certaine mesure, les connecteurs logique s'étendent à la logique incomplète comme suit :
`P` `Q` `P "et" Q` `P "ou" Q` `P=>Q` `P<=>Q` `P⇎Q` `0` `0` `0` `0` `1` `1` `0` `0` `oo` `0` `?` `1` `?` `?` `0` `1` `0` `1` `1` `0` `1` `oo` `0` `0` `?` `?` `?` `?` `oo` `oo` `?` `?` `?` `?` `?` `oo` `1` `?` `1` `1` `?` `?` `1` `0` `0` `1` `0` `0` `1` `1` `oo` `?` `1` `?` `?` `?` `1` `1` `1` `1` `1` `1` `0`
Dans le cas où `P "==" oo` et `Q "==" oo`, nous avons assurement `("⊢"P) "et" ("⊢"Q) = 0`. Mais par contre nous ne pouvons rien conclure sur `⊢ P "et" Q`. On définie alors la notion d'indépendance. Et si P et Q sont indépendant alors `P "et" Q "==" oo`.
---- 20 Juillet 2020 ----
Deux propositions `P` et `Q` sont indépendantes relativement à une théorie `T` si et seulement si T et P
. , c'est à dire si la détermination de l'une n'a pas d'influence sur la détermination de l'autre, alors dans ce cas nous avons `⊢P "et" Q = oo`. Mais si elles sont dépendantes entre elles alors tous les réultats `{0,oo,1}` peuvent être possibles, ce que nous notons par le signe `?`.
`"⊢"P` `"⊢"Q` `⊢P "et" Q` `⊢ P "ou" Q` `⊢P=>Q` `⊢P<=>Q` `⊢P⇎Q` `0` `0` `0` `0` `1` `1` `0` `0` `oo` `0` `?` `1` `?` `?` `0` `1` `0` `1` `1` `0` `1` `oo` `0` `0` `?` `?` `?` `?` `oo` `oo` `?` `?` `?` `?` `?` `oo` `1` `?` `1` `1` `?` `?` `1` `0` `0` `1` `0` `0` `1` `1` `oo` `?` `1` `?` `?` `?` `1` `1` `1` `1` `1` `1` `0`
---- 18 juillet 2020 ----
Mais parcontre nous ne pouvons rien conclure sur `⊢ P "et" Q`. Sauf si `P` et `Q` sont deux propositions indépendantes, c'est à dire si la détermination de l'une n'a pas d'influence sur la détermination de l'autre. Dans ce cas nous avons également `⊢P "et" Q = oo`.
Pour une opération quelconque de la forme `⊢ P"∗"Q`, le résultat `?` signifie que, si les propositions `P` et `Q` sont indépendantes entre elles, alors la valeur logique de `⊢ P"∗"Q` est `oo`, mais si elles sont dépendantes entre elles alors tous les réultats `{0,oo,1}` peuvent être possibles.
Dans un monde totalement calculable, toutes les propriétés vrais sont démontrables. Affirmer `P` comme ayant une valeur logique égale à `1`, c'est affirmer qu'il existe une démonstration de `P`. Mais cela n'est valable que pour les propositions non étendues. Ainsi par exemple, affimer `¿P`, c'est à dire affirmer l'indécidabilité de `P`, ne signifie pas affirmer l'existence d'une démonstration de l'indécidabilité de `P`. Ainsi les deux expressions `¿P` et `"⊢"¿P` ne sont pas logiquement égale.
En logique ternaire, l'axiome du tiers exclus n'est plus valable. Il se peut que l'expression `⊢P "ou" "¬"P` soit fausse. C'est le cas lorsque `P` n'est pas décidé, ce qui s'écrit en utilisant la négation globale, notée `!`, comme suit :
`¿P = !(P "ou" "¬"P)`
Il y a donc deux négations, l'une syntaxique notée `"¬"` qui ne s'applique qu'aux propositions, et qui inverse la valeur booléenne des propositions décidés, et qui laisse indécidé les propositions indécidés, l'autre globale notée `!` qui s'applique à toutes les propositions même étendues, définie comme suit :
`!P = "¬"P "ou" ¿P`
`!"¬"P = P "ou" ¿P`
`!¿P = P "ou" "¬"P`
Ces axiomes s'appliquent quelque soit la proposition étendue `P`. On en déduit :
`P` `"¬"P` `¿P``"¬"¿P` `!P` `"¬"!P` `!"¬"P` `"¬"!"¬"P` `0` `1` `0` `1` `1` `0` `0` `1` `oo` `oo` `1` `0` `1` `0` `1` `0` `1` `0` `0` `1` `0` `1` `1` `0`
Dans un monde calculable nous avons ces égalités trilogiques :
`P = "⊢"P`
`"¬"P = "⊢¬"P`
`¿P = ("⊬"P) "et" ("⊬¬"P)``!P = "¬"P "ou" ¿P`
`!P = "⊬"P`
La sémantique d'une proposition `P` est alors l'ensemble des mondes satisaisant `P` c'est à dire tel que le programme de vérité appliqué à `P` produit `1` en un temps fini. Mais pour éviter les confusions, on désignera la proposition en question explicitement par `"⊢"P`, et on appellera cette sémantique, la sémantique de `"⊢"P`.
La même problèmatique calculatoire se transcrit au niveau de la sémantique, donnant lieu à la définition d'une sémantique étendue. La sémantique étendue d'une proposition `P` sera le partitionnement de l'ensemble des mondes entre ceux qui satisfont `P`, ceux qui ne décident pas `P` et ceux qui satisfont `"¬"P`. Mais pour éviter les confusions, on désignera la proposition en question explicitement par le couple de propositions `(("⊢"P),("⊬"P))`, et on appellera cette sémantique, la sémantique de `(("⊢"P),("⊬"P))`.
Dans le cas d'une sémantique fini, les mondes considérés sont complets, le prédicat d'égalité appliqué à deux termes doit produire en un temps fini une valeur booléenne `0` ou `1` pour ainsi construire complètement l'ensemble fini des termes d'un monde. Le monde se définie donc comme une instance de la structure libre du langage des termes. Mais le prédicat d'égalité impose une contrainte spécifique s'appliquant à lui-même, à savoir l'axiome d'égalité appliqué aux littéraux d'égalité :
Si deux termes sont égaux selon le prédicat d'égalité alors ils peuvent être permutés dans tout littéral d'égalité où ils apparaisent comme sous-terme ou terme, sans que cela ne change la valeur du littéral d'égalité en question.
Cet axiome traduit le transport de l'égalité par l'égalité tel que décrit dans le chapitre II) Structures d'égalité. Et cette contrainte s'étend à tous les prédicats générateurs, et devient l'axiome d'égalité appliqué aux littéraux affirmatifs :
Si deux termes sont égaux selon le prédicat d'égalité alors ils peuvent être permutés dans tout littéral affirmatif où ils apparaisent comme sous-terme ou terme, sans que cela ne change la valeur du littéral affirmatif en question.
Cet axiome traduit le transport de l'égalité par tous les prédicats générateurs tel que décrit dans le chapitre II) Structures d'égalité. Et cette contrainte s'étend à tous les propositions, et devient l'axiome d'égalité appliqué aux propositions :
Si deux termes sont égaux selon le prédicat d'égalité alors ils peuvent être permutés dans toute proposition où ils apparaisent comme sous-terme ou terme, sans que cela ne change la valeur de la proposition.
Dans le cas fini, cette contrainte peut de façon évidente toujours être appliquée et la cohérence peut de façon évidente toujours être établie. Les mondes finis considérés sont toujours complets. Ce qui n'empêche pas de concevoir une notion de monde incomplet. Un monde incomplet correspond à une disjonction de mondes dans un même univers, analogue à une superposition d'états en mécanique quantique.
Un monde fini se veut être l'object le plus concret. C'est un langage muni d'une mémoire finie appelée table de vérité, ou d'un programme d'arrêt sûr, appelé programme de vérité, calculant la valeurs de chaque littéraux affirmatifs en respectant l'axiome d'égalité.
Le choix de cet axiome découle de ce que l'on veut que désigne le langage logique. Ainsi, on fait le choix de n'étudier que les systèmes de déduction qui respecte l'axiome d'égalité.
La quantité d'information d'un message se définit de façon absolu relativement au choix d'un langage de programmation. C'est la taille minimal des programmes qui produisent ce message. La quantité d'information d'un monde se définie comme étant la taille minimal des programmes qui calculent la valeurs des littéraux affirmatifs de ce monde.
Dans le cas infini, les mondes considérés sont dans une situation où ils sont nécessairement incomplets, et où la logique est ternaire. Le programme de vérité n'est plus d'arrêt sûr, et Turing démontre qu'il existe des cas où l'arrêt est imprévisible, c'est à dire nécessite un temps infini pour être résolue.
Chaque monde est une instanciation de bas niveau de la structure libre, non pas par une table de vérité finie, un ensemble finie de couples (littérale affirmatif - valeur booléenne), mais par un programme de vérité qui détermine non seulement les littéraux mais toutes les proposition du langage. Chaque littéral doit posséder une valeur booléenne `0` ou `1`, ou l'infini de Turing `oo`, cette dernière valeurs se produisant lorsque le programme de vérité ne s'arrête jamais. De même pour chaque proposition.
Le programme de vérité définit le monde et constitue une instanciation de l'univers. Mais le prédicat d'égalité semble imposer une contrainte spécifique plus forte encore que dans le cas fini. Pour la dévoiler, on doit décrire les effets de la logique ternaire sur l'égalité. Etant donné deux éléménts `a,b`, la logique étant ternaire, il existe 3 cas exclusifs :
`"⊢"a"="b` ÉgauxIl existe une démonstration de l'égalité entre `a` et `b`. `"⊢"a"≠"b` DistinctsIl existe une démonstration de l'inégalité entre `a` et `b`. `("⊬" a"="b) "et" ("⊬" a"≠"b)` IndécidésIl n'existe pas de démonstration de l'égalité ni de l'inégalité de `a` et `b`.
On dira que `a` et `b` sont Fusionnables (ou peuvent être rendu égaux) si et seulement s'il n'existe pas de démonstration de l'inégalité entre `a` et `b`. Et on dira qu'ils sont Séparables (ou peuvent être rendu inégaux) si et seulement s'il n'existe pas de démonstration de l'égalité entre `a` et `b`.
`"⊢"a"="b` Égaux `"⊢"a"≠"b` Distincts `("⊬" a"="b) "et" ("⊬" a"≠"b)` Indécidés `"⊬" a"="b` Fusionnables `"⊬" a"≠"b` Séparables
--- 19 juin 2020 ---
Considérons deux éléments `a` et `b` Indifférentiables c'est à dire tel qu'il n'existe pas de démonstration de `a≠b`.
à savoir l'axiome d'égalité étendue.
S'il n'existe pas de démonstration prouvant l'inégalité de deux termes selon le prédicat d'égalité alors ils peuvent être permutés dans toute proposition où ils apparaisent comme sous-terme ou terme, sans que cela ne change la valeur ternaire `{0,1,oo}` de la proposition en question.En effet le défaut
Un élément est calculable si et seulement si
Un opérateur est dit calculable s'il existe un programme qui peut le calcul
La récurrence est consubstantielle à la notion de structure.
on commence par définir ce qu'est la récurrence générale à partir d'une fonction propositionnelle unaire `P"(.)"` choisie arbitrairement :
On dit qu'un élément `x` respecte une proposition unaire `P"(.)"`, si et seulement si `P(x)` est vrai.
On dit qu'un opérateur respecte une proposition unaire `P"(.)"` si et seulement si, lorsqu'il est appliqué qu'à des éléments respectant `P"(.)"`, il produit un élément respectant `P"(.)"`.Etant donné un ensemble `L` d'opérateurs et d'éléments respectants une proposition unaire `P"(.)"`, la clôture par composition close notée `"<"L">"` ou `L"°"` est un ensemble d'éléments respectant `P"(.)"`.
En logique du premier ordre le groupe en notation multiplicative se définit comme suit :
`"Groupe"(G,"∗") <=> ( (AAxAAyAAz"," (x"∗"y"∗")z"="x"∗"(y"∗"z)),(EE1AAxEEy"," x"∗"1"="x"," 1"∗"x"="x"," yx"="1"," xy"="1))`
Ce qui se traduit littéralement par : L'ensemble sous-jacent `G` est muni d'une loi de composition interne `"∗(.,.)"`, qui admet un élément neutre et qui admet pour chaque élément un inverse.
La théorie `"Groupe"(G,"∗")` a dans son langage qu'un seul opérateur binaire qu'est le produit `"∗"`. La théorie de groupe peut enrichir son langage avec un nouvel opérateur `1` rendu définissable de façon unique par la structure. Mais cet élément `1` ne fait pas partie du langage de la structure. Il peut ne pas être calculable par la structure. D'une certaine façon la structure ne le connait pas, mais sait qu'il existe et qu'il est unique.
De même, la théorie du groupe permet de définir un unique opérateur d'inversion que l'on peut nommer `frI"(.)"`. Délors, la théorie de groupe enrichie son langage avec cet opérateur `frI` rendu définissable de façon unique par la structure. Mais cet élément `frI` ne fait pas partie du langage de la structure. Et on verra en étudiant la notion de calculabilité des opérateurs, qu'il peut ne pas être calculable par la structure. D'une certaine façon la structure ne le connait pas, mais sait qu'il existe et qu'il est unique.
On définit une structure de groupe, en notation multiplicative, en logique du second ordre comme suit. Cette nouvelle définition se distingue de la précédente en ce qu'elle affirme explicitement l'existence d'un opérateur d'inversion `frI"(.)"` sans pour autant l'introduire dans son langage.
`"Groupe"(G,"∗") <=> ( ( AAxAAyAAz"," (x"∗"y"∗")z"="x"∗"(y"∗"z) ) , ( EE1EE frI"(.)"AAx"," x"∗"1"="x"," 1"∗"x"="x"," xfrI(x)"="1"," frI(x)x"="1 ) ) `
La nuance parait faible. En fait, les éléments du langage désignent des applications que la structure peut apppliquer est évaluer. Comme si ces applications étaient déjà implémentées dans une couche logicielle mise à disposition de la structure et étaient en mesure de produire toujours un résultat. Mais le caractère calculable de ses applications n'est pas supposées, seuls leur mise à disposition de la structure et l'assurance qu'elle donne un résultat est posée. De tel sorte que le langage de la structure agrémenté des mécanismes généraux de programmation détermine tout ce que la structure peut calculer.
Pour interpréter correctement cette théorie du second ordre, il convient d'étudier l'équivalence de Skolem que nous présentons en deux parties. La première partie s'appelle la spécialisation :
Etant donné une fonction propositionnelle binaire quelconque `P"(.,.)"`, nous avons :
Spécialisation `EE frI"(.)"AAx, P(x,frI(x))` `=>` `AAx EEi, P(x,i)`
Cette propriété de spécialisation est toujours valide. Elle signifie que si nous avons la preuve qu'il existe une application `frI"(.)"`, même si nous ne sommes pas capable de la calculer, qui satisfait la proposition `AAx, P(x,frI(x))`, alors nous pouvons conclure que pour tout `x` nous avons la preuve qu'il existe un élément `i`, l'élément défini par `i"="frI(x)`, même si nous ne sommes pas capable de le calculer, qui satisfait la proposition `P(x,i)`.
On considère ainsi des éléments définissables mais non calculables. Définissable signifie que la théorie prouve leur existence, tandis que calculable signifie être désigné par au moins un terme clos du langage d'opérateurs.
La seconde partie s'appelle la définition d'application, c'est la réciproque :
Définition
d'application `AAx EEi, P(x,i)` `=>` `EEfrI"(.)"AAx, P(x,frI(x))`
Cette propriété définissant une application est équivalente à l'axiome du choix. C'est l'affirmation qu'il est possible de procéder à une infinité de choix arbitraires et ainsi de définir une application `frI"(.)"` sur un domaine pouvant être de cardinalité infini.
Mais certaines opinions récusent cet axiome du choix et n'admète à la place qu'un axiome plus faible n'autorisant qu'un nombre fini de choix arbitraires, ne représentant qu'une quantité finie d'information, et appelé définition finie d'application. Tous ces choix arbitraires sont regroupés dans la définition de la fonction propositionnelle `P` qui est de talle finie. Et l'axiome du choix se réduit en l'axiome du choix fini en ajoutant la condition d'unicité :
Définition
finie
d'application `AAx EE!i, P(x,i)` `=>` `EEfrI"(.)"AAx, P(x,frI(x))`
Où l'expression `EE!x` signifie qu'il existe un et un seul élement `x`. C'est à dire :
Définition
finie
d'application `EEi, P(x,i) "et" AAj, P(x,j)"⇒"(i"="j)` `=>` `EEfrI"(.)"AAx, P(x,frI(x))`
Mais lorsque l'ensemble sous-jacent est fini, cette distinction n'a plus lieu d'être, puisqu'il n'y a forcement qu'un nombre fini de choix possibles à faire. L'équivalence de Skolem devient assurement valide, et donc cette deuxième définition du groupe devient exactement équivalente à la première.
La structure de groupe dans le langage `"<"1,frI,"∗>"{"="}` possède la théorie d'égalité universelle suivante :
`AAxAAyAAz, (x"∗"y)"∗"z"="x"∗"(y"∗"z)`
`AAx, x"∗"1"="x`
`AAx, 1"∗"x"="x`
`AAx, xfrI(x)"="1`
`AAx, frI(x)x"="1`
On s'intérresse au langage `"<"1,frI,"∗>"{"="}` et à un ensemble sous-jacent de `n` éléments `G=⟅ e_1,e_2,e_2,...,e_n ⟆` servant à construire les mondes d'au plus `n` éléments. Ce sont `n` éléments qui peuvent être rendus égaux, et qui constituent la base de construction des mondes d'au plus `n` éléments.
Une distinction doit s'opérer entre le modèle et le groupe en tant que monde fini. Le modèle est la structure comprenant le langage `(G,"∗")` et comprenant la théorie précédente. Tandis qu'un groupe est une réalisation du modèle. Un groupe d'au plus `n` éléments est une théorie complète dont le langage est `(e_1,e_2,e_2,...,e_n,"∗")`, et l'ensemble sous-jacent n'est pas mentionné puisqu'il est énuméré en un sac `⟅ e_1,e_2,e_2,...,e_n ⟆`. Le monde ainsi défini a donc une connaissance complète de lui-même, ce qui n'est pas le cas du modèle. Le monde peut calculer tous ses éléments.
On procéde ainsi à une extension élémentaire en ajoutant au langage les éléments `e_1,e_2,e_3,...,e_n` et en ajoutant au cadre théorique la restriction que tous les opérateurs et prédicats évoqués soient définis dans cet ensemble sous-jacent `G` ou dans ses dérivés `G"→"G`, `G"→"(G"→"G)`, `(G"→"G)"→"G`, ...
Cela constitue un univers où chaque instantiation cohérente de bas niveau constitue un monde d'au plus `n` éléments.
Ainsi nous définissons deux niveaux de langage emboités. Un premier niveau dit langage de l'univers `"<"1,frI,"∗>"{"="}` et un second niveau, le bas niveau, dit langage des mondes possédant au plus `n` éléments, `"<"1,e_1,e_2,e_3,...,e_n, frI,"∗>"{"="}`, et en ajoutant au cadre théorique la restriction que l'ensemble sous-jacent est `⟅e_1,e_2,e_3,...,e_n⟆`.
Chaque proposition `P` écrite dans le langage de haut niveau `"<"1,frI,"∗>"{"="}` aura une signification spécifique dans chaque monde fini `G` décrit dans le langage de bas niveau `"<"1,e_1,e_2,e_3,...,e_n, frI,"∗>"{"="}`. Si la proposition `P` est vrai dans le monde `G`, nous dirons que `P` se réalise dans `G`, ou que `G` réalise `P`, ou que `G` satisfait `P`, et nous noterons `G"⊨"P`.
Chaque proposition `P` écrite dans ce langage `"<"1,frI,"∗>"{"="}` constitue un paramètre macroscopique. Tandis que chaque littéral de `"<"1,e_1,e_2,e_3,...,e_n,frI,"∗>"{"="}` constitue un paramètre microscopique. Le nombre de mondes complets d'au plus `n` éléments satisfaisant la proposition `P` représente le nombre d'états microscopiques possibles d'au plus `n` éléments pour la théorie `P`. La quantité d'information que représente le choix d'un tel monde en est le logarithme en base `2` et s' exprime en nombre de bits.
On définit récursivement une structure de groupe en présentant des opérateurs générateurs qui vont construire tous les éléments de la structure libre, et une théorie d'égalité qui va quotienter la structure libre pour produire tous les éléments du groupe. Par exemple voici le groupe bigène libre :
`G="Groupe"("∗",1,frI,a,b)`
Le premier argument du patron `"Groupe"` est sa loi de composition interne `"∗"`, le second argument est l'élément neutre `1`, le troisième argument est l'opérateur d'inversion `frI`, et les arguments suivants sont des éléments générateurs `a,b`. Dans cet exemple il y a que deux éléments générateurs. Les éléments de la structure sont construits à partir des opérateurs de la présentation. Puis, à charge de ces affectations mise en oeuvre par l'appel, le patron `"Groupe"` transporte la théorie du groupe suivante :
`AAxAAyAAz, (x"∗"y"∗")z"="x"∗"(y"∗"z)`
`AAx, x"∗"1"="x`
`AAx, 1"∗"x"="x`
`AAx, xfrI(x)"="1`
`AAx, frI(x)x"="1`
Les éléments du groupe sont les classes d'équivalences de la relation d'équivalence définie comme suit : `x` et `y` étant deux termes quelconques appartenant à la structure libre `"<∗",1,frI,a,b">"`, ils sont équivalents si et seulement si la théorie du groupe le démontre, ce qui se note, `G|--x"="y`. On remarque que le symbole `G` peut désigner le groupe, ou simplement la théorie du groupe, ou simplement l'ensemble-sous-jacent du groupe. Et c'est contexte et le typage par inférence auxquels revient la charge de lever l'ambiguité.
La structure `G` comprend une théorie que l'on peut bommé par une autre lettre `T` et qui est écrite dans ce langage `"<∗", 1, frI">"{"="}`. La structure s'obtient en quotientant la structure libre du langage `"<∗", 1, frI">" par la théorie `T` :
`G = ("<∗", 1, frI">")"/"T`
Les éléments de la structure sont les classes d'équivalences de la relation d'équivalence définie comme suit : `x` et `y` étant deux termes quelconques appartenant à la structure libre `"<∗",1,frI,a,b">"`, ils sont équivalents si et seulement si la théorie de la structure le démontre, ce qui se note, `T|--x"="y`.
Une distinction doit s'opérer entre le langage du groupe `"<∗", 1, frI">"{"="}` qui est le même pour tous les groupes, et qui est celui du modèle, et la définition du groupe qui instancie d'une certaine façon les opérateurs et prédicats du modèle. Puis, si nous définissons plusieurs groupes, en utilisant les même symboles d'opérateurs que ceux du modèle, `G"=Groupe"("∗",1,frI,a,b)` et `H"=Groupe"("∗",1,frI,a,b)`, alors on pourra spécifie ces opérateurs à l'aide d'un indice pour savoir à quelle groupe ils font référence : `"∗"_G`, `1_G`, `frI_G`, `a_G`, `b_G`, `"∗"_H`, `1_H`, `frI_H`, `a_H`, `b_H`.
Ces groupes utilises un même langage `"<∗", 1, frI">"{"="}`. Ainsi toute proposition `P` écrite dans ce langage aura une signification précise pour chacun de ces groupes. Si la proposition `P` est vrai dans la structure `G`, nous dirons que `P` se réalise dans `G`, ou que `G` réalise `P`, ou que `G` satisfait `P`, et on notera `G"⊨"P`.
---- 1 mars 2020 ----
On définit formellement le langage à l'aide d'une grammaire que l'on décrit en utilisant le méta-symbole de production `->` et le méta-symbole de l'alternative `"|"`. Dans notre exemple, le langage d'opérateurs se définit par la grammaire suivante. Le symbole non-terminal `bbT` désigne un terme :
`bbT -> a "|" f(bbT) "|" g(bbT,bbT)`
Le langage des littéraux affirmatifs se définit par la grammaire suivante. Le symbole non-terminal `bbA` désigne un littéral affirmatif :
`bbA -> A(bbT) "|" bbT "=" bbT`
Puis afin de simplifier la grammaire, on utilise des aspects de protocole de bas niveau. La négation d'une égalité s'écrit de deux façons `"¬"(a"="b)` ou `a"≠"b`. De tel sorte que l'on peut établir un aspect. Lorsque on fait agire la négation `"¬"` sur une égalité `a"="b` celle-ci se réécrit `a≠b`. Avec ce mécanisme, on peut simplifier la grammaire formelle comme suit : Le langage des littéraux se définit par la grammaire suivante où l'on met en oeuvre l'aspect décrit précédement, où le symbole non-terminal `bbA` désigne un littéral affirmatif, et où le symbole non-terminal `bbL` désigne un littéral :
`bbL -> bbA "|" ¬bbA`
Le langage des propositions sans quantificateurs :
`bbS -> bbA "|" "¬"bbS "|" bbS "et" bbS "|" bbS "ou" bbS "|" bbS"⇒"bbS "|" bbS"⇔"bbS "|" bbS"⊕"bbS`
L'introduction des déclarations de variables quantifiés va créer un jeu de contexte emboité :
`bbP -> bbS "|" "¬"bbP "|" bbP "et" bbP "|" bbP "ou" bbP "|" bbP"⇒"bbP "|" bbP"⇔"bbP "|" bbP"⊕"bbP
`bbP -> AA alpha bbP "|" "¬"bbP "|" bbP "et" bbP "|" bbP "ou" bbP "|" bbP"⇒"bbP "|" bbP"⇔"bbP "|" bbP"⊕"bbP
On se place dans un groupe `G`. Un morphisme `f` est une application qui respecte les opérateurs du groupe, c'est à dire satisfaisant les trois règles suivantes :
`AAxAAy`
`f(1)=1`
`f(xy) =f(x)(y)`
`f(x^("-"1))=f(x)^("-"1)`
L'image `f(G)` constitue un groupe qui est un sous-groupe de `G`.
Dans la littérature classique, on appelle ce genre de morphisme, un endomorphisme. Mais pour les mêmes raisons que précédement, une application est par défaut définie de l'ensemble sous-jacent de la structure vers l'ensemble sous-jacent de la structure, un morphisme sera par défaut définie de l'ensemble sous-jacent de la structure vers l'ensemble sous-jacent de la structure. Un morphisme sera par défaut un endomorphisme de la structure.