Logique du second ordre

1) Introduction

En décrivant l'algèbre et en voulant la formaliser par le biais du raisonnement par récurrence notamment, on définit un langage logique du second ordre c'est à dire admettant deux types de variables que sont les éléments et les fonctions au sens général.

En parallèle à la descritption des premières structures algébriques, il convient de décrire deux types de relations que sont les relations d'équivalence et les relations d'ordre, ainsi que les liens canoniques qu'il speuvent avoir avec les premières structure algébrique.

2) Préordre

Le magma `(E,"+")` engendre un préordre "≤" définie comme suit ;

`AAxAAy, x<y <=> EEz, y=x+z "ou" y=z+x`

2) Le magma bigène

Comment écrire formellement la propriété qu'un magma `(E,"+")` soit engendré par deux éléments `a,b`. Cette propriété d'engendrement n'est pas du premier ordre. On la note comme suit :

`E= "<"a,b,"+(.,.)>"`

La propriété d'engendrement à pour conséquence la règle de récurrence sur `E` suivante :

`AAP"(.)",( (P(a)),(P(b)),(AAx"," P(x) => P(x"+"a) "et" P(a"+"x) "et" P(b"+"x) "et" P(a"+"b))) => AAx, P(x)`

La propriété qui entraine cet engendrement reprend ce mécanisme mais à l'envers :

`AAxEEyEEz, (x"="f(y) "et" x">"y) "ou" (x"="g(y,z) "et" x">"y "et" x">"z) "ou" x"="a "ou" x"="b`

---- 25 mars 2024 ----

5) Structure libre et langage d'opérateurs

(extrait de http://mabboux.net/informatique/Metamath3.htm )

Une structure libre se présente par une liste d'opérateurs générateurs d'arité fixe constituant sa présentation, tel que par exemple `S="<"a,b,f"(.)",g"(.,.)>"`. Et il n'y a pas de différence entre une structure libre et un langage d'opérateurs d'arité fixe. La structure libre est définie par ce qu'elle peut construire à partir de ses opérateurs générateurs, sans évaluation des opérateurs générateurs.

Les éléments de la structure libre sont les compositions close d'opérateurs générateurs, sans évaluation des opérateurs générateurs. Et ils sont par construction tous distincts, leur égalité correspondant à l'égalité de leur arbre de composition d'opérateurs générateurs.
Les opérateurs de la structure sont les programmes d'arrêt sûr, programmés à partir des opérateurs générateurs de la structure libre.

On étend notre langage mathématique pour pouvoir exprimer la propriété de structure libre dans le cas général. Cela se fait en 7 points :

On note en minuscule les variables désignant un élément (opérateurs nullaires).
On note en majuscule les variables désignant un opérateur (opérateurs non-nullaires).
On introduit un deuxième type de variable qu'est la séquence d'arguments et on la note avec un tilda. Ainsi `tilde x` désigne une séquence d'éléments attendue par une fonction.
On met en oeuvre l'inférence de type, faisant qu'un opérateur `n`-aire appliqué à une séquence `tilde x` fait que la séquence `tilde x` est de taille exactement égale à `n`.
On définit ce qu'est l'égalité de deux opérateurs générateurs. Il ne s'agit pas de l'égalité fonctionnelle, mais de l'égalité d'identité relative à leur nom dans la présentation, permettant ainsi d'avoir deux fonctions distinctes, car de nom différent, produisant de mêmes résultats.
On note la quantification sur la structure à l'aide des symboles `AA, EE`. Ainsi `AAx, P(x)` signifie que tout élément de la structure satisfait le prédicat `P"(.)"`. Et `AA tilde x, P(tilde x)` signifie que toute séquence d'éléments de la structure, séquence de taille permise par l'arité de `P`, satisfait le prédicat `P`. Et `AA A, P(A)` signifie que tout opérateur programmable de la structure satisfait le prédicat `P"(.)"`.
On note la quantification sur la présentation de la structure à l'aide des symboles `barAA, barEE`. Ainsi `bar AAx, P(x)` signifie que tout élément générateur de la structure satisfait le prédicat `P"(.)"`. Et `bar AA A, P(A)` signifie que toute opérateur générateur de la structure satisfait le prédicat `P"(.)"`.

Un élément est identifié par un mot du langage, qui s'apparente à son nom, et qui corrrespond à la composition close d'opérateurs générateurs qui l'a construit, sans évaluation des opérateurs générateurs. Exemple, l'élément `g(a,f(a))`. Etant donnés deux variables `x,y` désignant des éléments, l'expression `x"="y` signifie qu'ils ont un même nom, qu'ils sont identifiés par un même mot du langage, par une même composition close d'opérateurs générateurs, sans évaluation des opérateurs générateurs. Et réciproquement, l'expression `x"≠"y` signifie qu'ils ont des noms différents, qu'ils sont désignés par deux compositions closes différentes d'opérateurs générateurs, sans évaluation les opérateurs générateurs.

La théorie de la structure libre s'écrit :

`bar AA A bar AA B AA tilde u AA tilde v,`

`(A"≠"B) "ou" (tilde u"≠" tilde v) => (A(tilde u)"≠"B(tilde v) )`

Elle stipule que si les opérateurs générateurs ont des noms distincts dans la présentation ou que les séquences d'arguments sont distinctes dans la structure alors l'application des opérateurs sur ces séquences d'arguments doit produire nécessairement des éléments distincts dans la structure, ce qui est assuré en identifiant l'élément à la composition close qui l'a construit, sans évaluation les opérateurs générateurs. La contraposée peut aussi être utile :

`bar AA A bar AA B AA tilde u AA tilde v,`

`(A(tilde u)"="B(tilde v) ) => (A"="B) "et" (tilde u"=" tilde v)`

Cela signifie textuellement : « Quelque soit des opérateurs générateurs `A,B`, quelque soit des séquences d'arguments `tilde u, tilde v`, si `A(tilde u)"="B(tilde v)` alors `A` et `B` désignent le même opérateur générateur identifié par un même nom dans la présentation, et les séquences d'éléments sont égales dans la structure, `tilde u "=" tilde v` ».

6) L'évaluation du langage

Afin que le langage exprime autre chose que lui-même, on sépare le signifiant d'avec le signifié, le mot d'avec l'élément désigné par le mot, l'élément de la structure libre d'avec l'élément réel qu'il désigne. Il en découle que plusieurs mots peuvent désigner le même élément. Le mot est un élément de la structure libre, notons le, `x`. L'élément désigné par `x` est un élément du monde réel, noté `sigma(x)`. C'est un élément image d'une application d'évaluation `sigma`.

Chaque élément représenté ici par la variable `x` est un opérateur nullaire. Mais `x` est une variable, donc il y a une première évaluation de variable qui expose ce qu'elle contient, une composition close d'opérateurs générateurs sans évaluation des opérateurs générateurs. Et cette évaluation de variable est implicite et est repétée à chaque fois, faisant que l'on manipule le nom de la variable au lieu de son contenant.

Puis il y a une seconde évaluation qui elle, est explicite. C'est l'évaluation du langage, produisant ce que désigne un mot du langage. L'élément `x` qui n'est qu'une composition clause d'opérateurs générateurs sans évaluation, désigne un élément réel noté `sigma(x)`. L'élément `x` s'évalue en un élément image `sigma(x)` qui représente l'élément réel qu'il désigne.

La structure libre n'est qu'un langage. L'élément `x` n'est qu'un nom, une composition d'opérateurs générateurs sans évaluation. La variable `x` contient ce nom. Prenons par exemple l'élément `f(a)`. C'est un opérateur nullaire non-générateur. Il s'évalue en un élément image `sigma(f(a))` qui est l'élément réel qu'il désigne, et `f(a)` constitue son nom dans la structure libre. Et, il se peut que des noms distincts désignent le même élément réel. L'évaluation est une application `sigma` de la structure libre `S` vers le monde réel `M`. Considérons deux éléments, représentés par les variables `x, y`. Chacune de ces variables contient un élément de la structure libre, qui est un mot du langage, une composition close d'opérateurs générateurs sans évaluation. Il y a deux sortes d'égalité, l'une dans la structure libre `S` qui se note `x=y`, et l'autre dans le monde réel `M` qui se note `sigma(x)=sigma(y)`.

Ainsi l'évaluation du langage introduit un ensemble d'égalités entre des éléments de la structure libre. On appel théorie d'égalité, un ensemble d'égalités.

Dans l'approche constructive, la désignation est une construction. Si un opérateur générateur nullaire `x` désigne quelque chose autre que lui-même, c'est qu'il peut s'évaluer, tel l'exécution d'un programmealors cela défini une évaluation appelé concrétisation. Les éléments nullaires `x` peuvent être évalués par concrétisation. Et pour distinguer l'élément de la structure libre et sa concrétisation, on note `x` l'élément de la structure libre et `x()` sa concrétisation.

et sous forme de conjonction de clauses prénexes :

`AAP"(.)","¬"P(a) "ou" "¬"P(b) "ou" "¬"(AAx,P(x) => P(x"+"a) "et" P(a"+"x) "et" P(b"+"x)"et" P(x"+"b)) "ou" AAx,P(x)`

`AAP"(.)","¬"P(a) "ou" "¬"P(b) "ou" (EEx,P(x) "et" ("¬"P(x"+"1) "ou" "¬"P(1"+"x)) "ou" AAx,P(x)`

`AAP"(.)","¬"P(a) "ou" "¬"P(b) "ou" (EEx,P(x) "et" "¬"P(x"+"1)) "ou" (EEx, P(x) "et" "¬"P(1"+"x)) "ou" AAx,P(x)`

`AAP"(.)"EEx,"¬"P(1) "ou" (P(x) "et" "¬"P(x"+"1)) "ou" (P(x) "et" "¬"P(1"+"x)) "ou" AAy,P(y)`

`AAP"(.)"EExAAy,`
`"¬"P(1) "ou" P(x) "ou" P(y)`
`"¬"P(1) "ou" P(x) "ou" "¬"P(1"+"x) "ou" P(y)`
`"¬"P(1) "ou" "¬"P(x"+"1) "ou" P(x) "ou" P(y)`
`"¬"P(1) "ou" "¬"P(x"+"1)) "ou" "¬"P(1"+"x) "ou" P(y)`

et à l'extérieur de `E` comme suit :

`AAP"(.)", ( (P(1)),(AAx"∈"E"," P(x) => P(x"+"1) "et" P(1"+"x))) => AAx"∈"E, P(x)`

et sous forme de conjonction de clauses prénexes :

`AAP"(.)","¬"P(1) "ou" "¬"(AAx,E(x) "et" P(x) => P(x"+"1) "et" P(1"+"x)) "ou" AAx,E(x) => P(x)`

`AAP"(.)","¬"P(1) "ou" (EEx,E(x) "et" P(x) "et" ("¬"P(x"+"1) "ou" "¬"P(1"+"x))) "ou" AAy,"¬"E(y) "ou" P(y)`

`AAP"(.)"EExAAy,"¬"P(1) "ou" (E(x) "et" P(x) "et" ("¬"P(x"+"1) "ou" "¬"P(1"+"x))) "ou" "¬"E(y) "ou" P(y)`

`AAP"(.)"EExAAy,"¬"P(1) "ou" (E(x) "et" P(x) "et" "¬"P(x"+"1)) "ou" (E(x) "et" P(x) "et" "¬"P(1"+"x)) "ou" "¬"E(y) "ou" P(y)`

`AAP"(.)"EExAAy,`
`"¬"P(1) "ou" E(x) "ou" "¬"E(y) "ou" P(y)`
`"¬"P(1) "ou" E(x) "ou" P(x) "ou" "¬"E(y) "ou" P(y)`
`"¬"P(1) "ou" E(x) "ou" "¬"P(1"+"x) "ou" "¬"E(y) "ou" P(y)`
`"¬"P(1) "ou" P(x) "ou" E(x) "ou" "¬"E(y) "ou" P(y)`
`"¬"P(1) "ou" P(x) "ou" "¬"E(y) "ou" P(y)`
`"¬"P(1) "ou" P(x) "ou" "¬"P(1"+"x) "ou" "¬"E(y) "ou" P(y)`
`"¬"P(1) "ou" "¬"P(x"+"1) "ou" E(x) "ou" "¬"E(y) "ou" P(y)`
`"¬"P(1) "ou" "¬"P(x"+"1) "ou" P(x) "ou" "¬"E(y) "ou" P(y)`
`"¬"P(1) "ou" "¬"P(x"+"1) "ou" "¬"P(1"+"x) "ou" "¬"E(y) "ou" P(y)`

3) Le magma monogène libre

Comment écrire formellement la propriété qu'un magma monogène `(E,"+",1)` doit vérifier pour être libre ? C'est une propriété qui n'est pas du premier ordre, et qui comprend deux propriétés :

L'engendrement : `E= "<"1,"+(.,.)>"`
L'extension libre : `x"+"y=扎`

Si le demi-groupe est monogène alors il est abelien. La démonstration est faite au chapitre 9. On exprime la propriété d'extension libre `"+(.,.)" ` commutative en utilisant conjointement une relation d'ordre `"⩽"` définie comme suit :

`AAxAAyAAz,`
     `x"⩽"x,`                               Réflexif
     `x"⩽"y "et" y"⩽"x=>x"="y,` Antisymétrique
     `x"⩽"y "et" y"⩽"z => x"⩽"z` Transitif

qui vérifie la propriété suivante :

`AAx, x ⩽ x"+"1`

En conclusion :

`"Magma monogène"(E,"+",1) <=>`
      `AAP"(.)", ( (P(1)),(AAx "∈" E"," P(x) => P(x"+"1) ),(AAx "∈" E "," P(x) => P(1"+"x) )) => AAx "∈" E, P(x)`

`"Magma monogène libre "(E,"+",1) <=>`
      `AAP"(.)", ( (P(1)),(AAx"," P(x) => P(x"+"1) ),(AAx"," P(x) => P(1"+"x) )) => AAx, E(x)"⇒"P(x)`
      `EE⩽ in (E×E->{0,1})`
      `AAxAAyAAz,`
      `x"⩽"x,`                               Réflexif
      `x"⩽"y "et" y"⩽"x=>x"="y,` Antisymétrique
      `x"⩽"y "et" y"⩽"z => x"⩽"z` Transitif
      `x ⩽ x"+"1`

---- 24 mars 2024 ----

19) Relation de prés-ordre

Dominique Mabboux-Stromberg