Logique d'ordre supérieur

1) Introduction

On part du plus petit langage d'opérateurs possible engendrant un espace de Herbrand infini. C'est le langage composé d'un élément et d'une fonction unaire `L ={a, s"(.)"}` et qui représente d'une certaine façon les entiers naturel.

Puis on posera petit à petit les règles de déduction et leurs axiomes lorsque leur apparition sera nécessaire comme par évidence intuitive.

On définie le langage logique par des règles de construction tel une grammaire. Et on commence par choisir les opérateurs qui nous sont indispenssables. Un terme est une composition close du langage d'opérateurs `{a, s"(.)"}`. Ce langage peut être augmenté de variables élémentaires telles que par exemple `x, y` ou fonctionnelles tel que par exemple `f"(.)"` pour former le langage d'opérateurs `{a, s"(.)", x, y, f"(.)"}`. Voici des exemples de termes :

`a, s(a), s(s(a)), s(x), s(f(x)), f(f(a))...`

Puis on choisit les prédicats qui nous sont indispenssables, et le seul qui nous soit indispenssable à ce stade est l'égalité `=`. Un littéral affirmatif est la composition close d'un prédicats parmis `{"=(.,.)"}` avec des termes du langage d'opérateurs `{a, s"(.)"}`. Le langage des prédicats peut aussi être augmenté de variables prédicatives telles que par exemple `X, P"(.)", Q"(.,.)"` pour former le langage de prédicats `{"=(.,.)", X, P"(.)", Q"(.,.)"}`. Le prédicat `X` d'arité nulle est simplement une valeur booléenne inconnue. Voici des exemples de littéraux affirmatifs :

`a=s(a), a=s(x), x = s(f(a)), P(x), Q(s(x),f(x)),...`

Un littéral peut en plus être négativé par l'opérateur logique `¬` tel que par exemples `x!=y, ¬P(x)`

Une expression logique est une combinaison de littéraux à l'aide d'opérateurs logiques.

Une clause est une disjonction de littéraux.

Toute expression logique se ramène à une conjonction de clauses. En effet, prenez par exemples l'expression logique `(X =>Y) => Z` `X, Y, Z` sont trois valeurs logiques, cette expression logique est équivalente à `(X  "ou"  Z)  "et"  (¬Y  "ou"  Z)`.

2) Quantification

Une proposition simple est une expression logique.

Une proposition unidimensionnelle quantifie une variable. Elle possède une tête et un corps séparé par une virgule. La tête quantifie la variable à l'aide d'un opérateur `AA` ou `EE` et le corps est une expression logique dans le langage augmenté de cette variable. Voici un exemple de proposition avec une variable élémentaire :

`EE x, x!=a`

La variable quantifiée peut être fonctionnelle. Voici un exemple de proposition avec une variable fonctionnelle unaire :

`EE f"(.)", f(a) != a`

Par symétrie, on conçoit qu'il est posssible de quantifier des variables prédicatives. Voici un exemple d'une proposition avec une variable prédicative unaire :

`EE P"(.)", P(a)`

Le corps d'une telle proposition peut également être constitué par une autre proposition unidimensionnelle, auquel cas le résultat est une proposition bidimensionnelle. Et cela peut se répéter, formant ainsi des propositions de dimension `n`, c'est à dire utilisant `n` variables qui sont soient élémentaires, fonctionelles ou prédicatives. Voici un exemple de proposition de dimension 3 utilisant une variable prédicative unaire et deux variables élémentaires, et qui correspond à un axiome de l'égalité :

`AA P"(.)", AA x, AAy, (x=y) => (P(x)<=>P(y))`

Nous avons ainsi définie un langage logique d'une grande puissance expressive.

3) Aspect calculatoire

Sémantiquement, et selon l'approche intuitionniste, une variable élémentaire interne représente un élément calculable du modèle, un terme de l'espace de Herbrand, ou autrement dit un élément de la structure libre `"<"a,s"(.)>"`. De même une variable fonctionnelle représente une fonction calculable du modèle, et une variable prédicative représente une fonction logique calculable dans le modèle.

Selon le principe élémentarien, les éléments du modèle sont énumérables comme tout ce qui est calculable. Les fonctions et prédicats calculable sont énumérables.

Et il n'y a pas de différence essentielle entre une fonction et un prédicat, juste une question accessoire sur la forme du résultat. C'est pourquoi on n'adopte pas d'écriture spécifique pour différentier une variable fonctionnelle d'une variable prédicative, sachant que l'usage qui en est fait après, tranche nécessairement la question.

Le modèle dans lequel les propositions sont réalisées ou non est l'espace de Herbrand munie des fonctions et prédicats calculable.

4) Négation

Considérons une variable élémentaire `x` et un prédicat unaire `P"(.)"`. Considérons la proposition `AA x, P(x)`. Le quantificateur `AA` appliqué à la variable `x` correspond à un `"et"` intégré sur l'ensemble des valeurs calculables de `x`. L'opérateur `"et"` est représenté par le symbole `^^` (tel que l'intersection) . L'ensemble des éléments de l'espace de Herbrand est représenté par `Omega`. Nous avons :

`AA x, P(x)       <=>     ^^^_(x in Omega) P(x)`

L'ensemble des valeurs possible de `x`, noté `Omega`, est par principe énumérable. Cela entraine que la proposition `AA x, P(x)` est réfutable en un temps fini dans le cas où celle-ci serait fausse. Et il s'agit là d'une périssologie car on définie justement la valeur logique fausse de cette proposition par le fait qu'elle doit être réfutée en un temps fini. Parcontre elle n'est pas assurement affirmable en un temps fini dans le cas où elle ne serait pas fausse. C'est pourquoi l'affirmation d'une telle proposition est parfois appellée un oracle.

En tant qu'idée mathématique sans contrainte matériel d'aucune sorte, on peut se placer à l'infini et ainsi connaître l'oracle. Mais il faut en quelque sorte, être immortel dans un monde immortel et de surcroit régit par la mécanique classique, somme-toute, des présupposés assurement faux, mais qui à notre échelle sont approximativement vrai..

Si on adopte ce principe qui correspond au présuposé des mathématiques, à savoir que le monde dans le quel est développé cette mathématique perdure éternellement et est régis par la mécanique classique, et que nous pouvons nous placer abstraitement à l'infini et ainsi connaitre la valeur logique de la proposition, alors toutes les propositions exprimables dans notre langage ont une valeur logique bien définie.

La négation d'une propostion unidimensionnelle s'obtient alors simplement en inversant le quantificateur de la tête et en négativant le corps.

`¬(AA x, P(x))   <=>   (EE x, ¬P(x))`
`¬(EE x, P(x))   <=>   (AA x, ¬P(x))`

Le quantificateur `EE` appliqué à la variable `x` correspond à un `"ou"` intégré sur l'ensemble des valeurs calculables de `x`. L'opérateur `"ou"` est représenté par le symbole `vv` (tel que l'union). L'ensemble des éléments de l'espace de Herbrand est représenté par `Omega`. Nous avons :

`EE x, P(x)       <=>     vvv_(x in Omega) P(x)`

On convient que cette règle de calcul de la négation s'applique quelque soit le type de variable, élémentaire, fonctionnelle ou prédicative d'arité quelconque.

Il est alors nécessaire, pour respecter la sémantique, pour respecter notre vision intuitive des fonctions et des prédicats, d'introduire dans le langage d'opérateurs l'ensemble des moyens nécessaires pour calculer toutes les fonctions et tous les prédicats considérés comme possibles.

Dans les cas dégénérés où nous n'avons pas cette propriété, la signification de la proposition `AA P(.), P(a)` change du sens habituel. Car elle signifie : « Quelque soit la fonction logique `P(.)` que nous pouvons construire avec les moyens qui nous sont données, nous avons la propriété `P(a)` ».

5) Élémentarisation

Puis on opère une élémentarisation des fonctions et des prédicats. Deux fonctions `f"(.)", g"(.)"` sont dites égales ssi `AA x, f(x)=g(x)`. Deux prédicats `R"(.)", S"(.)"` sont dits égaux ssi `AAx, R(x)<=>S(x)`. Et de même pour des fonctions et prédicats d'arité supérieur. Il est alors possible de créer pour chaque fonction et pour chaque prédicat modulo l'égalité ainsi définie, un élément qui le désigne. On obtient ainsi une deuxième catégorie d'éléments.

Il est alors possible de définir des variables (élémentaires, fonctionnelles ou prédicative) typées. Le type booléen se note `0`. Le type élément se note `1`. Le type élément de deuxième catégorie se note `2`. Le type `1->0` désigne celui d'un prédicat unaire, le type `(1,1)->1` désigne celui d'une fonction binaire, le type `(2,2)->0` désigne celui d'un prédicats opérant sur deux éléments de deuxième catégorie, le type `(1,2)->1` désigne celui d'une fonction opérant sur un élément de première catégorie et un élément de deuxième catégorie pour produire un élément de première catégorie, etc...

Les fonction et prédicats créés par ce procédé peuvent à leur tour être élémentarisés de la même façon et former les éléments de troisième catégorie, et ainsi de suite.

On cherche à étendre la capacité d'expression du langage, et on veut choisir une voie dans laquelle le langage obtenu permettra d'exprimer de façon simple une opération de raisonnement jugée fondamentale qu'est la récurrence générale.

6) Fonctionnisation et prédicarisation

Puis on opère une fonctionnisation des termes avec varibiable. Un terme avec une variable `x` libre, tel que par exemple `g(g(x,v),x)`, permet de créer une nouvelle fonction `h"(.)"` définie par `h(x) = g(g(x,v),x)` et qui peut alors être ajoutée au langage d'opérateurs. On notera :

`h   =   x |-> g(g(x,v),x)`

Puis on opère une prédicarisation des propositions avec varibiable. Une proposition avec une variable `x` libre, tel que par exemple `AA v, g(x,v)=g(v,x)`, permet de créer un nouveau prédicat `N"(.)"` définie par `N(x) <=> AA v, g(x,v)=g(v,x)` et qui peut alors être ajouté au langage de prédicats. On notera :

`N   =   x |-> (AA v, g(x,v)=g(v,x))`

 

--- 13 septembre 2015 ---

 

3) Logique respectueuse de l'indépendance

On enrichie le langage logique à l'aide de la notion d'indépendance entre quantificateur `AA` et `EE`, et plus finement encore, entre quantificateur `AA` et opération logique `"ou"`, et symétriquement aussi entre quantificateur `EE` et opération logique `"et"`.

Considérons deux variables élémentaires `x, y` et deux prédicats binaires `A"(.,.)", B"(.,.)"`. Considérons la proposition suivante :

`AAx, AAy, A(x,y)  "ou"  B(x,y)`

Cela signifie que quelque soit `x` et `y`, il y a toujours une des deux propositions `A(x,y)` ou `B(x,y)` qui est vrai. Maintenant, considérons qu'il existe un prédicat unaire `D"(.)"` tel que nous ayons :

`AAx, AAy, (A(x,y)  "et"  D(x) )  "ou" ( B(x,y)  "et"  ¬D(x))`

Le modèle est alors plus simple, puisque l'alternative se fait indépendament de la valeur de `"y"`. On notera ce `"ou"` indépendant de `AAy` avec la notation de Hintikka et Sandu. Les deux propositions suivantes sont équivalentes :

`AAx, AAy, A(x,y)  ("ou/"AAy)  B(x,y)`
`EE D"(.)", AAx, AAy, (A(x,y)  "et"  D(x))  "ou"  (B(x,y)  "et"  ¬D(x))`

Le `EEz` se ramenant à une opération logique `"ou"`, la même qualité d'indépendance à l'égard de `AAy` peut se produire. Auquel cas les 4 propositions suivantes sont équivalentes :

`AAx, AAy, (EEz"/"AAy)  W(x,y,z)`
`AAx, AAy, W(x,y,z_1) ("ou/"AAy) W(x,y,z_2) ("ou/"AAy) W(x,y,z_3) ("ou/"AAy) ...`
`EE D_1"(.)",EE D_2"(.)",EE D_3"(.)", AAx, AAy,`
        `(W(x,y,z_1)  "et"  D_1(x)  "et"  ¬D_2(x)  "et"  ¬D_3(x)  "et"  ...)`
      `"ou"(W(x,y,z_2)  "et"  ¬D_1(x)  "et"  D_2(x)  "et"  ¬D_3(x)  "et"  ...)`
      `"ou"(W(x,y,z_3)  "et"  ¬D_1(x)  "et"  ¬D_2(x)  "et"  D_3(x)  "et"  ...)`
      `"ou" ...`
`EEf(.), AAx, AAy,  W(x,y,f(x))`

--- 6 septembre 2010 ---

 

 

2.2) le typage

On utilise parfois, après la quantification d'une variable, le symboles ` / ` qui signifie "tel que" pour préciser le domaine où s'étend la quantification. Ainsi l'expression suivante :

`AAx "/" x in A "et" x in B,  x in C`

signifie quelque soit `x` tel que `x` appartenant à `A` et que `x` appartient à `B`, nous avons `x` appartient à `C`. Cette formule est équivalente à chacune des expressions suivantes :

`AAx "/" x in A,  x in B => x in C`
`AAx,  (x in A "et" x in B) => x in C`

`AAx,  x !in A "ou" x !in B "ou" x in C`
   x !in A "ou" x !in B "ou" x in C`

`AAx in A nn B,  x in C`

 

sur un ensemble au sens large c'est à dire sur un terme du langage non augmenté de cette variable,

Axiome d'extensionnalité : Si deux ensembles ont les mêmes éléments, alors ils sont égaux. ( entraine Axiome de l'ensemble vide : Il existe un ensemble sans élément. (<=schéma d'axiomes de compréhension))

 


 

Axiome de la paire : Si x et y sont deux ensembles, alors il existe un ensemble contenant x et y et eux seuls comme éléments. (<=schéma de remplacement)

Axiome de la réunion : Pour tout ensemble X, il existe un ensemble R dont les éléments sont précisément ceux des éléments de X et eux seuls.

Axiome de l'ensemble des parties : Pour tout ensemble E, il existe un ensemble dont les éléments sont précisément les sous-ensembles de E.

Axiome de l'infini : Il existe un ensemble W dont \varnothing est élément et tel que pour tout x appartenant à W, x \cup \{x\} appartient aussi à W. On peut ensuite définir par compréhension l'intersection de tous les ensembles contenant \varnothing et clos par cette opération : il s'agit de l'ensemble des nombres entiers tels que définis par von Neumann.

Schéma d'axiomes de compréhension ou de séparation : pour tout ensemble A et toute propriété P exprimée dans le langage, il existe un ensemble dont les éléments sont les éléments de A vérifiant P. Le schéma de compréhension est conséquence du schéma de remplacement qui suit.

Schéma d'axiomes de remplacement : Pour tout ensemble A et toute relation fonctionnelle P, formellement définie comme une proposition P(x,y) et telle que P(x,y) et P(x,z) impliquent que y = z, il existe un ensemble contenant précisément les images par P des éléments de l'ensemble d'origine A.

Axiome de fondation : Tout ensemble X non vide contient un élément y tel que X et y sont des ensembles disjoints (qui n'ont aucun élément en commun), ce qui se note X \cap y = \varnothing. Cet axiome n'est pas toujours ajouté à Z ou ZF. On peut construire assez facilement comme sous-classe d'un modèle quelconque de ZF, un modèle de ZF vérifiant l'axiome de fondation. Les ensembles utiles au développement des mathématiques usuelles appartiennent à cette sous-classe, et donc cela a peu d'importance d'ajouter celui-ci ou non à la théorie pour ces développements.

L'axiome de fondation n'est par exemple pas mentionné dans le livre de Halmos9, dont le but est de présenter les aspects de la théorie des ensembles utiles pour le mathématicien non spécialiste de ce domaine. L'axiome de fondation est par contre très utile dans le domaine spécialisé de la théorie des ensembles, il permet de hiérarchiser l'univers ensembliste, de définir un rang ordinal (voir l'article axiome de fondation) ...Des théories des ensembles, extensions de ZF sans fondation, ont par ailleurs été développées, qui introduisent un axiome d'anti-fondation (il en existe plusieurs variantes) qui contredit directement l'axiome de fondation. L'anti-fondation est une idée assez ancienne (Dimitri Mirimanoff 1917, Paul Finsler 1926), mais ces théories ont connu un regain d'intérêt pour leur lien avec l'informatique théorique10.

Axiome du choix : (version de Zermelo) Étant donné un ensemble X d'ensembles non vides mutuellement disjoints, il existe un ensemble y (l'ensemble de choix pour X) contenant exactement un élément pour chaque membre de X. L'axiome du choix reste controversé pour une minorité de mathématiciens. Des formes faibles existent, comme l'axiome du choix dépendant, très utile pour le développement de l'analyse réelle.

des variables préalablements déclarée par un quantificateur `AA` ou `EE`.

 

La négation d'une formule s'obtient en remplaçant les quantificateurs `AA` par `EE` et reciproquement, en laissant intacte les expressions sous les symboles ` / ` et en négativant l'expression logique.

Remarquez que l'expression logique `AA x in Ø,  P(x)` est identiquement vrai quelque soit `P` tandis que l'expression logique `EE x in Ø,  P(x)` est identiquement faut quelque soit `P`.

 

Puis on opère une unification des objets. Deux fonctions `f"(.)", g"(.)"` sont dites égales ssi `AA x, f(x)=g(x)`. Deux prédicats `R"(.)", S"(.)"` sont dits égaux ssi `AAx R(x)<=>S(x)`. Il est alors possible de définir pour chaque fonction et pour chaque prédicat modulo l'égalité ainsi définie, un élément qui le désigne. On obtient ainsi une deuxième catégorie d'éléments.

Il est alors possible d'étendre les opérateurs et prédicats à ses nouveaux éléments, faisant que le terme `f(f)` est un sens.

Cela n'engendre pas le paradoxe de Russel "l'ensemble des ensembles qui ne se contiennent pas se contient-il ?" car l'existence de l'ensemble n'est pas obligé. Ainsi la proposition suivante est simplement contraditoire :

`EE P"(.)", AA R"(.)", P(R) <=> R(¬R)`


Dominique Mabboux-Stromberg