La logique formelle

1) Introduction

Le raisonnement pour être incontestable doit pouvoir s'effectuer mécaniquement comme un programme informatique ou une machine idéale en mécanique classique, et nous décrirons ces procédés mécaniques en portant notre attention moins sur la construction des démonstrations dont la mise en cause sera laissée à la charge des contradicteurs, que sur la construction des objects mathématiques eux-mêmes qui portent davantage l'intuition. Nous décrirons la logique formelle d'un point de vue constructif c'est à dire en réfutant l'axiome du choix, autrement dit en utilisant uniquement les langages d'opérateurs et la programmation finie des fonctions et prédicats. Aussi, les concepts classiques d'ensembles et de modèles sont en partie réfutés. Seuls leur versions constructibles par langage d'opérateurs et par progammations finies sont utilisés.

2) Calcul propositionnel (logique d'ordre zéro)

On définie la valeur logique par un booléen. Ce choix simple va nous permettre de séparer le calcul booléen du calcul des équations booléennes qui correspond au calcul propositionnel, puis de séparer le calcul propositionel du calcul propositionnel d'ordre supérieur et du calcul des prédicats.

Une équation est composée de deux termes égaux. Mais s'agissant de booléens, on considère que ce qui est affirmé est affirmé vrai, c'est à dire que le deuxième terme est implicitement le booléen `1`. Se faisant, une propostion correspond exactement à une équation booléenne. C'est pourquoi le calcul propositionnel correspond exactement au calcul des équations booléennes.

Le calcul propositionnel utilise des variables `A, B, C` qui représentent des valeurs booléennes inconnues (c'est à dire soit `0` ou soit `1`). Ces variables sont utilisées implicitement pour désigner n'importe quelle valeur booléenne, c'est à dire en tant que variable quantifiée universellement au sense où elles peuvent être unifiées librement à d'autres variables ou valeurs booléennes. Le calcul propositionnel utilise les opérations booléennes que sont la négation `¬`, la conjontion `"et"`, la disjonction `"ou"`. Notez que toutes les autres opérations booléennes peuvent se définir à partir de ces 3 opérations `¬, "et", "ou"`.

Ces 3 variables `A, B, C`, et ces 3 opérations `¬, "et", "ou"`, constituent un langage, appelé schéma, noté sous forme de structure libre comme suit :

`"<"A, B, C, ¬"(.)", "et(.,.)", "ou(.,.)>"`

L'arité des opérations est précisée à l'aide des symboles (.) pour unaire et (.,.) pour binaire. Ce langage permet décrire des propositions c'est à dire des équations booléennes. L'intérêt d'utiliser un schéma, un langage précis, tient dans la connaissance de son pouvoir d'expression. Il permet d'exclure les propositions qui ne sont pas exprimables dans le langage et il permet de déterminer ce qu'il faut ajouter au schéma pour les rendre exprimables.

Dans la mesure où les variables `A, B, C`, sont dans le schéma, ce ne sont pas à proprement parler des variables mais des constantes du langage. Comme elles sont inconnues cela revient au même. Cependant, pour la clarté du débat, nous ne les désignerons pas comme des variables mais comme des constantes.

Un littéral est composé d'une éventuelle négation `¬` suivie d'une variable booléenne du schéma. Le littéral est dit négatif ou affirmatif selon qu'il utilise ou non le symbole de négation. Exemple : `¬A, B, ¬B`

Une clause est une disjonction de littéraux. Exemple : `¬A "ou" B`

Un état est une conjonction de littéraux. C'est aussi la négation d'une clause. Exemple : `A "et" ¬B`

Une proposition est un mot du langage. Exemple : `A "et" (B "ou" ¬(A "ou" ¬B))`

La proposition est d'ordre zéro car elle ne possède pas de variables quantifiés. Elle ne possède que des constantes et des opérations appartenant au schéma. C'est pourquoi le calcul prospositionnelle est une logique d'ordre zéro.

Le calcul propositionnel obéït à 4 lois (1_ Tier exclu, 2_ Associativité et commutativité, 3_ De Morgan, 4_ Distributivité) que l'on peut vérifier sans difficulté :

1) Loi du tier exclu : La négation d'une négation constitue une affirmation. C'est un présupposé du calcul booléen. Un booléen est soit `0` ou soit `1` et n'est ni les deux à la fois ni aucun des deux à la fois :

` ¬¬A = A`

C'est pour cette raison que l'on ne considére que deux sortes de littéraux, les affirmatifs et les négatifs.

2) Loi d'associativité et de commutativité : Les opérations booléennes `"et"`, `"ou"` sont associatives et commutatives :

`(A "et" B) "et" C = A "et" (B "et" C)` `(A "ou" B) "ou" C = A "ou" (B "ou" C)`
`A "et" B = B "et" A` `A "ou" B = B "ou" A`

De tel sorte qu'ils peuvent opèrer sur un ensemble fini d'arguments sans se soucier de leur nombre ni dans quel ordre ils sont disposés. Cela permet d'exprimer les conjonctions sous forme d'ensemble fini telle que par exemple :

`"et{"A,B,C"}" = A "et" B "et" C`

Et cela permet d'exprimer les disjonctions sous forme d'ensemble fini telle que par exemple :

`"ou{"A,B,C"}" = A "ou" B "ou" C`

3) Loi de De Morgan : La négation d'une disjonction d'arguments est équivalente à la conjonction des négations des arguments. Et symétriquement, la négation d'une conjonction d'arguments est équivalente à la disjonction des négations des arguments.

`¬(A "et" B) = ¬A "ou" ¬B`
`¬(A "ou" B) = ¬A "et" ¬B`

Il s'en suit qu'une proposition écrite avec comme seuls opérations logiques `{¬, "et", "ou"}` et des variables booléennes `A,B,C...`, se négative simplement en remplaçant chaque littéral par sa négation et en intervertissant les conjonctions `"et"` avec les disjonctions `"ou"` et réciproquement. Par exemple, considérons la proposition suivante :

`(A "ou" B "ou" ¬C) "et" ((¬A "et" B) "ou" C)`

La négation de cette proposition peut être obtenue comme suit :

`(¬A "et" ¬B "et" C) "ou" ((A "ou" ¬B) "et" ¬C)`

4) Loi de distributivité :

Les opérations booléennes `"et", "ou"` sont distributives chacune par rapport à l'autre :

`A "et" (B "ou" C) = (A "et" B) "ou" (A "et" C)` `A "ou" (B "et" C) = (A "ou" B) "et" (A "ou" C)`
`(A "ou" B) "et" C = (A "et" C) "ou" (B "et" C)` `(A "et" B) "ou" C = (A "ou" C) "et" (B "ou" C)`

De tel sorte que toute propositions se décompose de façon unique en une conjonction de clauses. Et cette décomposition est unique à l'ordre près des clauses dans chaque conjonction, et à l'ordre près des littéraux dans chaque clause. Exemple :

`(¬A "et" B) "ou" (A "et" C) = (¬A "ou" A) "et" (¬A "ou" C) "et" (B "ou" A) "et" (B "ou" C)`

3) Calcul propositionnel d'ordre supérieur

On quantifie des variables soit universellement ou soit existentiellement. Étant donné le schéma `"<"A,¬"(.)", "et(.,.)", "ou(.,.)>"`, voici un exemple de propositon unidimensionnelle du permier ordre :

`AAX, A "ou" X`

Une proposition unidimensionnelle quantifie une seul variable. Elle possède une tête `AAX` et un corps `A "ou" X` 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. Ainsi `X` est une variable quantifiée du premier ordre qui est ajoutées au schéma par le biais du quantificateur `AA` pour permettre d'écrire le corps de la proposition. Le schéma n'est donc pas le même à l'extérieur de la proposition et dans le corps de la proposition.

La proposition est dite du premier ordre car elle quantifie une variable `X` du premier ordre. Entendez par là un premier type de variable. Mais il s'agit là d'un pseudo-ordre, car la sémantique, ne proposant qu'un nombre fini d'états possibles, nous ramène toujours à une logique d'ordre zéro, la logique booléenne.

La proposition `AAX, A "ou" X` signifie simplement `A "ou" X` est vrai quelque soit la valeur de `X`, autrement dit, en ajoutant `X` au schéma, ce que l'on peut toujours faire, la proposition du premier ordre `AAX, A "ou" X` est équivalente à la proposition `(A "ou" X) "et" (A "ou" ¬X)` qui ne possède pas de variable quantifiée et qui est donc d'ordre zéro. Noter que dans ce cas `A` et `X` ne sont pas des variables mais des constantes du schéma. En ajoutant les constantes booléennes `0, 1`, dans le schéma, ce que l'on peut toujours faire, la propostion `AAX, A "ou" X` est équivalente à la proposition `(A "ou" 0) "et" (A "ou" 1)`. Symétriquement la proposition `EEX, A "et" X` signifie simplement `A "et" X` est vrai pour au moins une valeur de `X`, autrement dit, en ajoutant `X` au schéma, la proposition du premier ordre `EEX, A "et" X` est équivalente à la proposition `(A "et" X) "ou" (A "et" ¬X)`. En ajoutant les constantes booléennes `0, 1`, dans le schéma, la propostion `EEX, A "et" X` est équivalente à la proposition `(A "et" 0) "ou" (A "et" 1)`.

Une proposition est dite du premier ordre si elle ne contient, comme variables quantifiées, qu'un seul type de variable qui sont les variables booléennes et qui sont appellées variables du premier ordre. Mais ce premier ordre est un pseudo ordre car chaque proposition du premier ordre peut se développer en une proposition d'ordre zéro c'est à dire sans variable quantifiée.

Une fonction propositionnelle est une proposition écrite dans le langage augmenté de quelques variables booléennes `X,Y,Z...` qui joueront le rôle d'arguments de la fonction propositionnelle. Étant donné le schéma `"<"A,¬"(.)", "et(.,.)", "ou(.,.)>"`, voici des exemples de définition de fonction propositionnelle, sans quantification et avec quantification :

`(X,Y,Z)  ->  (X "ou" ¬Y "ou" A) "et" (Y "ou" ¬Z ) "et" (Z "ou" ¬X "ou" ¬A)`

`X  ->  AAY, EEZ, (Y "ou" ¬Z) "et" (¬Y "ou" Z "ou" A)`

Une proposition fonctionnelle est dite du premier ordre si elle contient des variables quantifiées du premier ordre. Mais il s'agit d'un pseudo-ordre, puisque les quantificateurs peuvent se développer.

Sémantiquement, une proposition fonctionnelle d'arité `n` représente une application de `"{"0,1"}"^n -> "{"0,1"}"` et il y en a exactement `2^(2^n)`.

Syntaxiquement, les quantifications `AA` et `EE` pouvant être développées, une proposition fonctionnelle d'arité n peut s'écrire sans quantificateur, c'est à dire en un mot du langage augmenté de n variables `X_1, X_2, X_3, ..., X_n`, qui jouerons le rôle d'arguments de la fonction propositionnelle.

Les variables booléennes constituent un premier type de variable. On introduit d'autres types de variable représentant des fonctions propositionnelles d'arité fixée. Ces variables sont dites de second ordre. Chaque arité `n` introduit un nouveau type de variable représentant une fonction propositionnelle d'arité `n` quelconque, c'est à dire un mot du langage augmenté de n variables. Ces types sont dit d'ordre supérieur, mais il s'agit là d'un pseudo-ordre supérieur car la sémantique, ne proposant pour chaque arité `n`, qu'un nombre fini de fonctions propositionnelles possibles, nous ramène toujours à une logique d'ordre zéro, la logique booléenne, comme on peut le voir ci-dessous :

On quantifie ces variables de second type soit universellement ou soit existentiellement. Étant donné un schéma `"<"A, ¬"(.)", "et(.,.)", "ou(.,.)>"`, voici des exemples de proposition du second ordre :

`AAP"(.)", P(A)`

`AAP"(.)", AAX, P(X) "ou" ¬P(X)`

Noter que `P"(.)"` est une variable du second ordre qui est ajoutées au schéma par le biais d'un quantificateur pour permettre d'écrire le corps de la proposition.

En reprenant le codage des opéateurs booléens décrit au chapitre Logique, la proposition `AAP"(.)", P(A)` signifie simplement que `P(A)` est vrai pour toutes les fonctions propositionnelles unaire, c'est à dire pour `P = 00`, pour `P = 01`, pour `P = 10` et pour `P = 11`. Autrement dit, en ajoutant les opérations booléennes `00, 01, 10, 11`, dans le schéma, ce que l'on peut toujours faire, la propostion `AAP"(.)", P(A)` est équivalente à la proposition `00(A) "et" 01(A) "et" 10(A) "et" 11(A)`.

On peut donc toujours transcrire ces propositions du second ordre en proposition logique d'ordre zéro, c'est à dire sans variable quantifiée. C'est pourquoi il s'agit de pseudo-ordre supérieur. Néanmoins le nombre de cas croissant de façon doublement exponentielle avec l'arité des opérations, il s'avère toujours pertinent d'utiliser ces types de variables de pseudo-ordre supérieur.

Une proposition fonctionnelle du second ordre est une proposition du second ordre écrite dans le langage augmenté de quelques variables booléennes et fonctionnelles `X, P"(.)", Q"(.,.)"`, c'est à dire représentant des opérations booléennes d'arité fixé, qui joueront le rôle d'arguments de la fonction propositionelle. Étant donné le shéma `"<"A, ¬"(.)", "et(.,.)", "ou(.,.)>"`, voici un exemple de définition d'une fonction propositionnelle du second ordre :

`Q"(.,.)" -> AAP"(.)", EEX, Q(X,P(X)) "et" ¬Q(P(X),X)`

Le type de cette fonction propositionnelle est :

`(B^2->B)->B`

Le type d'une fonction propositionnelle se définie précisement dans un langage de type engendré par `"{"B, "×", ->"}"`,`B` représente le type booléen c'est à dire l'ensemble `"{"0,1"}"`, l'opérateur binaire `"×"` représente le produit directe, et l'opérateur binaire `->` représente le constructeur d'aplication.

On définie les types modulo la currifiaction. Se faisant, le type `B->(B->B)` est équivalent au type `(B×B)->B`.

Nous avons utilisé les quantificateurs les plus simples, mais il est possible de définir d'autres quantificateurs. En voici quelques uns :

`EE! x, K(x)` Il existe un unique élément `x` tel que `K(x)`
`EE^nx, K(x)` Il existe exactement `n` éléments `x` tel que `K(x)`
`EE^"Pair"x, K(x)` Il existe exactement un nombre pair d'éléments `x` tel que `K(x)`
`EE^"Impair"x, K(x)` Il existe exactement un nombre impair d'éléments `x` tel que `K(x)`
`EE^"Maj"x, K(x)` Il existe une majorité d'éléments `x` tel que `K(x)`

Il y a une contrainte syntaxique dans ces expressions. Le type de `x` doit correspondre au type attendu par `K"(.)"`. Mais le langage des types s'apparente à un langage d'opérateurs. Il est donc possible d'y ajouter des variables, qui représenteront alors des types variables. Et il est alors possible de définir un prédicat opérant sur des arguments de type variables.

4) Calcul prédicatifs

Jacques Herbrand, mathématicien et logicien français (Paris 12 février 1908 - France 27 juillet 1931), définie les langages d'opérateurs d'arité fixé.

Un langage d'opérateurs est un ensemble fini d'opérateurs d'arité fixé, avec au moins un opérateur d'arité nulle permettant de construire des compositions closes d'opérateurs. Par exemple le langage `"{"a, b, f"(.)", g"(.,.)}"` comprend deux opérateurs d'arité zéro `a` et `b`, un opérateur unaire `f`, et un opérateur binaire `g`.

Un mot de ce langage est une compositions closes d'opérateurs. Par exemple le mot `g(a,f(a))` est un mot du langage d'opérateurs `"{"a, b, f"(.)", g"(.,.)}"`. On dit aussi que ce mot est engendré par le langage d'opérateurs `"{"a,b,f"(.)", g"(.,.)}"` ou qu'il appartient à `"<"a,b,f"(.)",g"(.,.)>"`.

L'univers de Herbrand est l'ensemble des mots engendrés par le langage d'opérateurs. C'est une structure libre que l'on désigne en énumérant ses opérateurs générateurs entre crochets `"< >"`.

`"<"a, b, f"(.)", g"(.,.)>" = "{"a, b, f(a), f(b), g(a,a), g(a,b), g(b,a), g(b,b), g(a,f(a)), g(a,f(b)), g(b,f(a)), ..."}"`

La structure libre contient tous les mots du langage. Chaque mot du langage désigne un élément de la structure libre. Deux mots distincts désignent nécessairement deux éléments distincts de la structure libre.

L'égalité est une relation binaire particulière. C'est pourquoi avant de définir l'égalité, on définie les prédicats d'arité fixé.

Un prédicat d'arité nulle représente simplement une constante booléenne inconnue, c'est à dire soit `0` ou soit `1`.

Un prédicat unaire est une application qui appliquée à un élément de l'univers de Herbrand retourne une valeur booléenne. Un prédicat unaire correspond à un ensemble. Les éléments de l'ensemble sont les éléments qui satisfont le prédicat.

Un prédicat binaire correspond à une relation binaire. C'est une application qui appliquée à un couple d'éléments retourne une valeur booléenne. La relation binaire correspond à un 1-graphes c'est à dire à un graphe orienté dans lequel, pour chaque couple de sommets `(x,y)`, il y a soit zéro ou soit un arcs orienté permettant de passer de `x` à `y`. Les sommets sont les éléments et les arcs orientés sont les relations valides entre éléments.

Un langage logique est un langage d'opérateurs avec une liste de prédicats de base définie sur ce langage d'opérateurs. Par exemple le langage logique `"(<"a, b, f"(.)", g"(.,.)>", V, P"(.)", R"(.,.))"` comprend un univers de Herbrand `"<"a, b, f"(.)", g"(.,.)>"`, un prédicat d'arité nul `V`, un prédicat unaire `P` et un prédicat binaire `R`. Ces trois prédicats sont définies sur l'ensemble `"<"a, b, f"(.)", g"(.,.)>"`.

Un littéral est composé d'une éventuelle négation `¬` suivie d'un prédicat de base avec ses arguments qui sont des mots de l'univers de Herbrand. Par exemple si nous avons les 3 prédicats de base suivants : `V, P"(.)", R"(.,.)"` et si le langage d'opérateurs est le suivant `"<"a, b, f"(.)", g"(.,.)>"` alors les 3 expressions suivantes sont des littéraux :

`¬V`
`¬P(f(a))`
`R(a,b)`

Le littéral est dit négatif ou affirmatif selon qu'il utilise ou non le symbole de négation. L'ensemble des littéraux possibles est énumérable, et la présentation regroupant les opérateurs générateurs et les prédicats de base constitue le schéma énumérateur de tous les littéraux possibles.

Une clause est une disjonction de littéraux. Exemple : `¬R(a,b) "ou" R(b,a)`

Un état est une conjonction de littéraux. C'est aussi la négation d'une clause. Exemple : `R(a,b) "et" ¬R(b,a)`

Une formule simple est une combinaison logique booléenne de littéraux.

Au stade où nous sommes de la description du langage logique, les propositions n'ont pas encore de variable quantifiée. Une formule simple est une expression logique ne comportant pas de variable quantifiée.

3) La calculabilité et les mondes

Par exemple considérons le langage d'opérateurs `"{"a, b, f"(.)", g"(.,.)}"`. C'est une structure libre `"<"a, b, f"(.)", g"(.,.)>"` engendrée par les 4 générateurs `a, b, f, g`. Cette structure contient tous les mots qu'il est possible de construire par composition close. Cette structure constitue l'univers de Herbrand.

Une structure libre engendrée par un nombre fini de générateurs est énumérable. Cela signifie qu'il existe un programme de taille finie qui énumère tous les éléments. Le mécanisme de cloture par composition close constitue cet énumérateur des mots et donc des éléments de la structure libre. On choisie un ordre d'énumération des mots selon la taille, le niveau ou la complexité de composition des mots (voir Langage d'opérateurs ).

Le produit directe de telles structures est encore énumérable, autrement dit, les couples d'éléments de l'univers de Herbrand sont énumérables, c'est à dire qu'il existe un programme de taille finie qui les énumère.

De même, les suites finies d'éléments de l'univers de Herbrand son énumérables.

Davantage encore, les suites infinies calculables sont énumérable comme le sont les programmes de taille finie qui les énumère. On entend par suite calculable, une suite infinie de valeurs telles qu'il existe un programme de taille finie qui les énumère.

On peut étendre ces structures libres en ajoutant une liste infinie énumérable de générateurs. Une structure libre engendrée par un ensemble énumérable de générateurs est encore énumérable.

Un monde est un ensemble de présuposés permettant de trancher toutes les formules simples, c'est à dire de déterminer leur valeur logique `0` ou `1`.

Pour formaliser les mondes, un moyen simple consiste à utiliser l'axiome du choix. C'est à dire la capacité d'effectuer une infinité de choix arbitraires. Cette capacité nous permet de définir les suites formelles de valeurs, c'est à dire de poser une infinité de valeurs arbitraires, et nous permet de définir les états formels c'est à dire une conjonction infinie de littéraux arbitraires.

Un état formel est dit cohérent s'il ne contient jamais à la fois un littéral et sa négation, et il est dit complet si chaque littéral possible y apparait au moins une fois de façon soit affirmative ou soit négative. Il est calculable à la place de formel s'il existe un programme de taille fini qui énumère tous ses littéraux. Il est dit affirmatif si tous ses littéraux sont affirmatifs. Il est dit négatif si tous ses littéraux son négatifs.

Un monde détermine tous les littéraux c'est à dire tous les prédicats de base pour tous les éléments possibles. Chaque prédicat de base peut être définie sous forme d'une suites formelles qui passe en revue la liste de tous les éléments (ou la liste de tous les couples d'éléments dans le cas d'un prédicat binaire) pour lui affecter une valeur booléenne décidée par le prédicat. Et cela revient au même de définir chaque prédicat de base par un état formel complet et cohérent dans le langage logique restreint au seul prédicat en question, et qui attribut à chaque élément (ou à chaque couples d'éléments dans le cas d'un prédicat binaire) une valeur booléenne décidée par le prédicat.

Exemples de prédicats définis par des suites formelles, cela correspond à leur graphe :

`V=0`
`P=((a,1),(b,0),(f(a),1),(f(b),1),...)`
`R=((a,a,0),(a,b,0),(b,a,1),(b,b,0),(a,f(a),1),...)`

Même exemple de prédicats définis par des états formels :

` ¬V`
`P(a) "et" ¬P(b) "et" P(f(a)) "et" P(f(b)) "et" ... `
`¬R(a,a) "et" ¬R(a,b) "et" R(b,a) "et" ¬R(b,b) "et" R(a,f(a)) "et" ... `

Dés lors un monde correspond à un état formel complet et cohérent.

Tout est bien qui finit bien dans le meilleur des mondes me direz-vous..., à part que cela ne convient pas, car nous avons utilisé un outils qui ne nous appartient pas, un oracle que seul les dieux peuvent nous conférer, celui d'effectuer une infinité de choix arbitraires, celui d'utiliser de façon effective une fonction non calculable, et donc qui est rendu calculable par magie en quelque sorte, somme-toute une chose qui n'existe pas.

Un monde qui contiendrait une quantité d'information infinie est quelque chose de physiquement absurde. De surcroît, aucun procédé calulatoire de pourrait exploiter cette infinitée. Le monde serait capable de trancher tout littéral mais selon un moyen non calculable, selon un moyen trancsendant...

Si on adopte une approche constructive, plus paresseuse et plus prudente, il convient alors de se restreindre aux seuls objects que l'on peut construire. La règle en la matière est :

« Parmis les suites comprenant une infinité de valeurs, on ne peut construire et donc utiliser que les suites calculables c'est à dire dont les valeurs sont énumérés par un programme de taille finie ».

Un prédicat unaire est calculable ssi il existe un programme de taille finie, dont l'arrêt est sûr, qui appliqué à n'importe qu'elle mot de l'univers de Herbrand donne comme résultat la réponse du prédicat. Et cela revient au même de définir le prédicat par un état calculable complet et cohérent dans le langage logique restreint au seul prédicat en question.

Dés lors un monde calculable correspond à un état calculable complet et cohérent.

Pour définir un monde calculable, il faut définir son schéma c'est à dire le langage logique dans le quel il s'inscrit, par exemple le langage `"(<"a, b, f"(.)", g"(.,.)>", V, P"(.)", R"(.,.))"`. Puis il faut programmer chaque prédicat de base par un programme de taille finie et dont l'arrêt est sûr. Cela consiste à programmer `V`, `P"(.)"`, et `R"(.,.)"` mais de telle sorte que l'arrêt soit sûr. Et nous voyons bien que, construisant la logique à partir des programmes, il est nécessaire de formaliser la programmation avant de pouvoir formaliser la logique, ce que nous verrons au chapitre 12.

Un prédicat unaire `P` correspondra à un programme qui prendra comme entré un élément `x` c'est à dire un mot de l'univers de Herbrant, et qui retournera en un temps fini la valeur logique de `P(x)` qui dervra être `0` ou `1`.

L'étude de la programmation nous apprend qu'un tel programme est équivalent à deux programmes, deux énumérateurs, que sont l'énumérateur des éléments valides et l'énumérateur des éléments invalides, c'est à dire, à deux énumérateurs tels que aucun éléments n'est énuméré par les deux énumérateurs à la fois et tous les éléments sont énumérés par l'un ou l'autre des deux énumérateurs.

C'est pourquoi un prédicat unaire est calculable ssi il est capable d'énumérer tous ses éléments valides et d'énumérer tous ses éléments invalides.

Dans un monde calculable, un littéral est toujours évaluable en un temps fini, et donc une formule simple est toujours évaluable en un temps fini.

On se restreint à ne considérer que les seuls objects que l'on peut construitre. Mais il n'y a pas de contrainte sur la nature des objects, la seul contrainte est qu'ils soient constructibles. On peut donc construire qu'une moitier d'objet, formant en quelque sorte des demi-objects, des demi-prédicats ou prédicats incomplets, et des demi-mondes ou mondes incomplets.

L'introduction de la notion de calculabilité dans la logique ajoute une troisième valeur logique qu'est l'infini de Turing noté `oo`. Cette valeur correspond à la non réponse d'un programme, au fait que le programme ne s'arrête jammais. Une opération logique est un programme. Une valeur logique est le résultat d'un programme ou son non-résultat. Mais on ne peut pas utiliser de façon effective des opérations logiques non calculables tel que celle qui convertirait l'infini de Turing `oo` en une réponse Oui ou en une réponse Non.

Si on s'en tient qu'aux suites calculables selon les préceptes intuitionnistes, on se doit d'abandonner pour un prédicat unaire sa valeur logique transcendante, au profit d'une valeur logique calculable. Tout prédicat unaire comprend deux énumérateurs, un énumérateur des éléments valide et un énumérateur des éléments invalides. Et il peut alors exister des éléments ni valides ni invalides, appellés éléments indécis. Cela constitue une troisième valeur logique qu'est l'infini de Turing, notée `oo`.

Noter que dans certain cas cette valeurs ne peut pas être déduite dans notre monde puisqu'il faut se placer à la fin des temps pour produir cette réponse qui est alors appelé un oracle.

---- 3 novembre 2015 ----

Si on veut s'en tenir à une position calculable pure, l'infini de Turing ne peut pas être invoqué. Il est remplacé par un entier A qui n'a de pertinence que si il est trés grand. Il signifie la non réponse parmis les A premières énumérations. Et il convient d'avancer deux tels entiers A et N qui signifient la non affirmation parmis les A premières énumérations des éléments valides, et la non réponse parmis les N premières énumérations des éléments invalides

 

 

 

 

Il en va de même pour déduire l'existence d'un éléments à la fois affirmé et réfuté par le prédicat, dans le cas où le prédicat serait incohérent.

 

Et il convient aussi d'envisager le cas où le prédicat est incohérent, c'est à dire, affirme à la fois pour un élément sa validité et son invalidité.

 

Pour tout prédicat, chaque élément est soit valide ou invalide par contre il peut exister des éléments ni affirmables ni réfutables. On les appelle éléments indécis. Et cela constitue une troisième valeur logique qu'est l'infini de Turing, notée `oo`.

 

 

 

 

 

Le prédicat détermine de façon calculable ses éléments affirmables et ses éléments réfutables, et il peut être amené à déterminer de façon non calculable ses éléments valides et ses éléments invalides. Du point de vu intuitionniste seul les deux premières notions existent.

 

 

**

On définit constructivement tout prédicat unaire comme composé de deux énumérateurs, un énumérateur des éléments affirmés et un énumérateurs des éléments réfutés. Le prédicat est calculable si la réunion des deux énumérateurs constitue un énumérateur de tous les éléments c'est à dire si la réunion des éléments affirmés et des éléments réfutés par le prédicat couvre l'ensemble de tous les éléments, autrement dit s'il n'y a pas d'élément indécis. Le prédicat est non-calculable s'il existe des éléments ni affirmables ni réfutables, appellés éléments indécis.

Un monde calculable est un monde où chaque prédicat de base est complet et calculable. Le monde calculable définie chaque prédicat de base par un programme de taille finie dont l'arrêt est sûr et qui donne la valeur du prédicat pour tous les mots de l'univers de Herbrand. Un monde calculable correspond à un état calculable complet et cohérent.

 

Un monde affirmatif est un monde où chaque prédicat de base est affirmatif. Un prédiciat affirmatif est un énumérateur des éléments affirmables. Le monde affirmatif définie chaque prédicat de base par un programme de taille finie qui énumère leurs éléments affirmables.

Symétriquement, un monde négatif est un monde où chaque prédicat de base est affirmatif. Un prédiciat négatif est un énumérateur des éléments réfutables. Le monde négatif définie chaque prédicat de base par un programme de taille finie qui énumère leurs éléments réfutables.

--- 24 octobre 2015 ---

 

 

2) Variables élémentaires

Une variable élémentaire est un opérateur variable d'arité zéro.

Une variable élémentaire peut être vue de deux façons différentes, soit comme une inconnue qui possède une valeur précise mais que l'on ne connait pas, ou bien soit comme une mémoire informatique susceptible d'évoluer et d'être partagée.

La variable élémentaire est ajoutée au langage d'opérateurs comme un nouvel opérateur d'arité zero. Cela constitue une extension élémentaire du langage d'opérateurs. Et il existe deux types d'extensions possibles :

L'extension élémentaire est dite intérieur, si on pose que les valeurs possibles de la variable sont les mots de l'univers de Herbrand avant l'extension.

L'extension élémentaire est dite extérieur si on pose que les valeurs possibles de la variable ne sont pas les seuls mots de l'univers de Herbrand avant l'extension mais puissent être aussi une nouvelle valeur en dehors de l'univers de Herbrand avant extension désignée justement par son nom.

Lorsque la variable désigne un élément en dehors de l'univers de Herbrand avant extension, cet élément est désigné par le symbole même du nouvel opérateur libre constant ainsi ajouté. Cela peut se faire car ce nouvel opérateur est par définition lié à rien et peut donc convenir à toute nouvelle définition.

L'extension extérieur va nécessiter d'étendre la définition des prédicats de bases pour tenir compte de ce nouvel opérateur générateur. Cela va démultiplier les mondes possibles.

Par défaut une extension est extérieur, et s'il y a une restriction, celle-ci doit être précisée. Prenons un exemple. Les entiers relatifs sont définis selon la notation programmative et la notation linguistique par (voir Structures fondamentales ) :

ℤ = Groupe monogène (+, 0, -, 1)
ℤ = <0, 1, -, +> / {+ est associatif, 0 est l'élément neutre pour +, - est l'opposé pour atteindre 0 avec +}

L'extension élémentaire intérieur est définie par :

ℤ = Groupe monogène (+, 0, -, 1)[a] / {a∈<0,1,-,+>}
ℤ = <0, 1, a, -, +> / {+ est associatif, 0 est l'élément neutre pour +, - est l'opposé pour atteindre 0 avec +, a∈<0,1,-,+>}

L'extension élémentaire exterieur est définie par :

ℤ[a] = Groupe monogène(+, 0, -, 1)[a]
ℤ[a] = <0, 1, a, -, +> / {+ est associatif, 0 est l'élément neutre pour +, - est l'opposé pour atteindre 0 avec +}

L'extension élémentaire intérieur ne change pas la structure mais augmente le pouvoir d'expression du langage logique de la structure. Parcontre l'extension élémentaire extérieur va dans de nombreux cas agrandire la structure en ajoutant un opérateur générateur.

3) Fonctions et prédicats, calculabilité et définissabilité

L'introduction de variables élémentaires crée de facto la notion de fonction. Un terme quelconque T dans le langage d'opérateurs augmenté de quelques variables x, y constitue une fonction T(x,y) opérant dans le langage d'opérateurs avant extension. Néanmoins on ne conservera cette expression que si T dépend bien de x et de y. Ainsi par exemple, en considérant le langage d'opérateurs <a, b, f(.), g(.,.)>, le terme g(g(x,a),y) est bien une fonction de (x,y) par contre le terme g(g(x,x),a) n'est fonction que de x. Et, si nous avons cette connaissance sur T nous opérerons de suite la simplification d'écriture en considérant la fonction T(x) et non T(x,y), qui précise que T est indépendant de y.

Dans le cadre d'extensions intérieurs, c'est à dire en utilisant des variables élémentaires à valeurs dans l'univers de Herbrand avant extension, on peut définir des fonctions opérant sur ces variables. Ainsi par exemple, on peut définir une fonction T comme suit :

T(x,y) = g(g(x,a),y)

T est à la fois un terme de <a, b, f(.), g(.,.), x, y> et une fonction binaire dans <a, b, f(.), g(.,.)>

La construction de fonction se fait sur le calcul des termes. Le même procédé peut se faire sur le calcul logique booléen. On parlera alors de fonction propositionnelle ou de prédicat. Ainsi par exemple, on peut définir une fonction propositionnelle F comme suit :

F(x,y) = R(x,x) et R(x,y)

F est à la fois une proposition de (<a, b, f(.), g(.,.), x, y>, V, P(.), R(.,.)) et un prédicat binaire définie sur <a, b, f(.), g(.,.)> ou autrement dit, une fonction binaire de <a, b, f(.), g(.,.)> vers {0,1}, où {0,1} représente l'ensemble des valeurs booléennes possibles, 0 pour le faux, 1 pour le vrai.

4) Intégration et quantification

Un mot de l'univers de herbrand désigne un élément. Dans le cadre d'une extension intérieur, c'est à dire en utilisant une variable élémentaire, un mot contenant des variables peut désigner un ensemble si on fait varier ces variables sur toutes les valeurs possibles de l'univers de Herbrand avant extension. Par exemple, considérons la variable x. Le mot g(x,a) va décrire un ensemble lorsque x décrira l'univers de Herbrand. On introduit l'opérateur d'intégration int x, T(x) qui regroupe les termes T(x) en un ensemble comme suit :

int x, g(x,a) = {g(a,a), g(b,a), g(f(a),a), g(f(b),a), g(g(a,a),a),...}

L'intégration se fait sur le calcul des termes. Le même procédé peut se faire sur le calcul logique booléen. On parlera alors de quantification. Considérons un prédicat P(.), et une variable élémentaire x. On définie la quantification ∀x  comme étant l'opération ( ET ) intégrée sur toutes les valeurs possibles de x, c'est à dire sur tous les mots du langage. Et on définie la quantification ∃x comme étant l'opération ( OU ) intégrée sur tous les valeurs possibles de x, c'est à dire sur tous les mots du langage.

∀x, P(x) = P(x0) et P(x1) et P(x2) et P(x3) et ...
∃x, P(x) = P(x0) ou P(x1) ou P(x2) ou P(x3) ou ...

où {x0, x1, x2, x3, ...} représente l'univers de Herbrand. Le domaine du quantificateur, qui doit être énumérable, couvre tous les mots du langage (avant extension).

Les quantificateurs classiques veulent intégrer sur tous les éléments. Or cela n'est pas constructif car nous ne manipulons pas directements les éléments. on choisit une autre définition des quantificateurs plus prudente et aussi plus restrictive. Les quantificateurs intégrent seulement sur l'ensemble des éléments exprimables par le langage, c'est à dire sur l'univers de Herbrand qui est un ensemble énumérable. Cette définition a l'avantage d'être constructive, et s'appuie sur le mécanisme d'énumération des mots de l'univers de Herbrand. Noter alors que toute modification ultérieur du langage d'opérateurs va modifier le sens des quantificateurs.

D'une manière générale on doit pouvoir préciser le domaine sur le quel s'applique le quantificateur, et la première façon qui vient à l'esprit de définir ce domaine consiste à le définir comme un langage d'opérateurs. On utilisera le symbôle , sans avoir besoin d'utiliser la notion d'ensembles, en utilisant seulement un énumérateur, l'énumérateur d'une structure libre associée à un langage d'opérateurs. Nous avons :

(∀x∈<a, s(.)>, P(x)) <=> (P(a) et P(s(a)) et P(s(s(a))) et ...)

Le langage dans lequel est exprimé la proposition ∀x∈<a, s(.)>, P(x) est (<a, s(.)>, P(.)). La proposition est de dimension 1, cela veut dire qu'elle utilise une variable dite muette, ne figurant pas dans le langage, car x possède une portée limitée à la proposition et ne constitue pas une variable globale.

Il est possible de définir d'autres quantificateurs. En voici quelques uns :

∃!x, P(x) Il existe un unique élément x tel que P(x)
nx, P(x) Il existe exactement n éléments x tel que P(x)
Finix, P(x) Il existe exactement un nombre fini d'éléments x tel que P(x)
Pairx, P(x) Il existe exactement un nombre fini pair d'éléments x tel que P(x)
Impairx, P(x) Il existe exactement un nombre fini impair d'éléments x tel que P(x)
oox, P(x) Il existe exactement une infinité d'éléments x tel que P(x)
Majx, P(x) Il existe une majorité d'éléments x tel que P(x)
=x, P(x) Il existe une bijection entre les éléments x tel que P(x) et les éléments y tel que ¬P(y)

Une proposition simple est une expression logique sans variable.

Une proposition unidimensionnelle quantifie une variable élémentaire. 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 d'opérateurs augmenté de cette variable. Voici un exemple de proposition avec une variable élémentaire :

`EE x, P(x)`

Le corps d'une telle proposition peut également contenir une autre proposition unidimensionnelle, auquel cas le résultat est une proposition qui peut être bidimensionnelle. Et cela peut se répéter, formant ainsi des propositions de dimension `n`, c'est à dire utilisant `n` variables élémentaires.

Nous avons ainsi définie le langage logique du premier ordre. Le langage est dit du premier ordre car il n'utilise qu'un seul type de variable que sont les variables élémentaires dont les valeurs possibles sont dans l'univers de Herbrand.

5) 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 possibles 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 auront une valeur logique bien définie.

Les fonctions propositionelles exprimables, entendez par là définissables, pourront alors constituer des prédicats non calculbales tout en étant bien définies.

La négation d'une propostion unidimensionnelle s'obtient 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 possibles 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)`

Loi de De Morgan : Si une proposition est écrite avec comme seuls opérations logiques {0, 1, ¬, et, ou} alors sa négation s'obtient simplement en remplaçant chaque littéral par sa négation, en intervertissant les "et" avec "ou", et en intervertissant les quantificateurs ∀ avec ∃ avec leur même domaine, Par exemple :

 T     =  (∀x ∃y  R(x,y)  ou ¬R(y,x) ) et  (∃x ∀y  R(x,y)  ou P(x) )
¬T    =  (∃x ∀y ¬R(x,y) et  R(y,x) )  ou  (∀x ∃y ¬R(x,y) et ¬P(x) )

La difficulté d'une preuve en cette matière tient dans la manipulation des disjonctions et conjonctions infinies énumérables qui découlent de l'interpretation constructive des quantificateurs. On remplace ces quantificateurs, qui correspondent à des énumérations infinis, par des programmes de taille fini, qui énumèrent.

 

6) Calculablité et définissabilité

Même si le prédicat unaire P(.) est calculable, la proposition AA x, P(x) n'est pas forcement calculable. Même si le prédicat binaire R(.,.) est calculable, le prédicat unaire définie par la fonction propositionelle x --> AA y, R(x,y) n'est pas forcement calculable.

Dans un monde calculable les prédicats de base sont calculables mais les prédicats qui sont des fonctions propositionnelles ne le sont pas forcement. Ils sont définissables dans le langage logique mais ils ne sont pas toujours calculables. D'où l'apparition d'une notion de définissabilité plus vaste que la notion de calculabilité.

Considérons la proposition bidimensionnelle suivante :

AA x, EE y, R(x,y)

Cette proposition affirme qu'à chaque x, il existe au moins un y vérifiant R(x,y). L'axiome du choix nous permet d'effectuer ce choix un nombre infini de fois, de choisir un tel y pour chaque x, et ainsi de construire une fonction de choix x-->y que l'on note plus explicitement par x-->y(x). Autrement dit, on admet l'existence d'une fonction unaire y(.) non nécessairement calculable telle que AAx, R(x,y(x)). La pproposition est alors équivalente à :

EE y(.), AAx, R(x,y(x))

où le graphe de la fonction y(.) constitue une suite formelle. Parcontre si on rejète cette axiome, on ne peut pas construire de suite formelle seullement des suites calculable, on ne peut effectuer un nombre infini de choix arbitraire seulement effectuer un choix par le

procéder ainsi

Un moyen simple consisterait à limiter la puissance du quantificateur existanciel, et à considérer que le choix doit être fait par un programme de taille finie. On considére l'énumération des valeurs de x et on cherche un programme de taille fini qui effectue le choix d'un y dépendant de x c'est à dire qui effectue le calcul de y(x). Autrement dit, on admet encore l'existence d'une fonction unaire y(.) vérifiant AAx, R(x,y(x)), mais celle-ci doit être calculable.

EE y(.), AAx, R(x,y(x))

 

 

 

De même les opérateurs spéciaux de construction de fonction, qui seront utilisés plus tard, permettront de définir des fonctions non calculables. On pourra alors construire des fonctions définissables qui ne seront pas nécessairement calculables.

Selon le principe élémentarien, les éléments du modèle sont énumérables comme tout ce qui est calculable et davantage encore, comme tout ce qui est définissable. Les fonctions et prédicats calculables sont énumérables puisque ce sont des programmes de taille finie. Les fonctions et prédicats définissables sont énumérables puisque ce sont des définitions de taille finie.

Le monde dans lequel les propositions sont évaluées, et se réalisent ou non, est constitué de l'univers de Herbrand et de prédicats de base calculables sur cette univers. Il est appelé monde calculable. On conçoit un monde un peu plus vaste appelé monde définissable qui est constitué de l'univers de Herbrand et de prédicats de base définissables.

 

6) Syntaxe et sémantique

La syntaxe d'une proposition A est son expression dans le langage logique prédéfini. On veut déterminer les règles du raisonnement. Ces règles font partie de la syntaxe.

On veut donner un sens plus profond aux propositions. Ce sens est constitué par les mondes où sont satisfait ces propositions. La sémantique d'une proposition A est l'ensemble des mondes où A est satisfait. A priori on peut considérer deux niveaux de sémantiques l'une calculable contenant l'ensemble des mondes calculables où A est satisfait, l'autre définissable contenant l'ensemble des mondes définissables où A est satisfait.

On construit un métalangage en ajoutant un deuxième type d'éléments que sont les mondes. Soit M un monde et A une proposition. La propriété que la proposition A soit satisfaite dans le monde M se notera :

M |= A

Si la proposition A est vrai dans le monde M, alors la méta-proposition M |= A est vrai.

La proposition A est dite infaillible si et seulement si elle est satisfaite dans tous les mondes, ce qui se note :

∀M, M |= A

On réserve le concept de tautologie aux propositions qui se démontre d'elle-même. Une tautologie est infaillible mais une proposition infaillible n'est pas forcement une tautologie. Elle peut ne pas être démontrable, en particulier cela se produit si notre système de règles de démonstrations est trop faible.

Puis, on soumet le raisonnement au procédé constructif. On restreint la portée du quantificateur universelle ∀M aux seuls mondes calculables. Ainsi le qualificatif Infaillible signifie satisfait dans tous les mondes calculables.

Dans l'antiquité on ne considéraient pas l'implication comme une opération booléenne mais plutôt comme un lien de cause à effet. Et cela change la nature du lien. Un lien de semi-coïncidence (ou de semi-corrélation) n'est pas un lien de cause à effet. On note le lien de semi-coïncidence entre A et B par la proposition A => B, et cela signifie que lorsque A est vrai, B l'est aussi. Si dans tous les mondes possibles M nous avons cette semi-coïncidence, c'est à dire la propriété A => B, une propriété infaillible, cela se note alors :

∀M, M |= (A=>B)

Et on le notera plus simplement par :

A |= B

Cela signifie que la semi-coïncidence est toujours vrai, qu'elle est infaillible, que dans tous les mondes où A est vrai, B est vrai. Mais cela ne remet pas en cause le sens du lien qui reste un lien de semi-coïncidence tant que l'on a pas exhibé la raison qui en constitue la preuve.

On introduit les symboles de satisfaction infaillible |= et de satisfaction possible ¦= qui opèrent sur deux propositions quelconques A, B, comme suit :

A |= B A satisfait infailliblement B ∀M / M |= A, M |=B Tout monde satisfaisant A satisfait B
A ¦= B A satisfait possiblement B ∃M / M |= A, M |=B Il existe au moins un monde satisfaisant A qui satisfait B

7) Démontrabilité

Dans l'antiquité on considéraient l'implication davantage comme un lien de cause à effet. Le lien de cause à effet entre A et B se note comme suit :

A |- B

Ce lien signifie qu'il existe une démonstration utilisant A comme hypothèse pour prouver B.

On considère un système de règles de déduction, et on note A |- B ssi il existe une succession de déductions qui part de A pour aboutire à B, et que nous appellons démonstration. Cette démonstration doit être valable dans tous les mondes puisque qu'elle doit s'appliquer pareillement dans tous les mondes possibles. La connaissance de A |- B, la connaissance du lien de cause à effet entre A et B, la connaissance d'une démonstration partant de A pour aller à B, entraine la semi-coïncidence infaillible entre A et B, ce que se note :

∀A, ∀B, (A |- B) => (A |= B)

Noter que l'on a pas précisé le type des variables A, B. Le type des variables est déterminés par l'usage qui en est fait dans le corps de la proposition. Il s'agit ici de propositions quelconques.

Le système de règles de déduction doit obéire à ce principe dit de cohérence.

Une autre propriété recherchée mais qui peut ne pas être atteignable, s'appelle la complétude, à savoir, que toutes les semi-coïncidences infaillibles doivent constituer des liens de causes à effets c'est à dire doivent pouvoir être démontrés, ce qui se note :

∀A, ∀B, (A |= B) => (A |- B)

Ainsi le principe de complétude du système de déduction correspond à la réciproque du principe de cohérence du système de déduction.

8) forme prénexe respectueuse de l'indépendance

 

 

 

Andreas.Herzig, cours, "Introducion à la Logique", Université Paul Sabatier, IRIT-LILaC

 

Plus tard nous considérerons des variables fonctionnelles représentant des fonctions et des variables prédicatives représentant des prédicats. 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.

 

 

Un opérateur d'arité zéro dans le langage peut jouer plusieurs rôles à la fois, celui d'élément, celui de variable élémentaire et celui d'autre variable élémentaire.... En faite, le rôle de variable élémentaire peut être attribué arbitrairement à tout opérateur d'arité nulle du langage, sans que cela interdise sa signification en tant qu'élément générateur ou en tant qu'autre variable élémentaire à d'autres endroits. Tout se passe comme si le quantificateur appliqué localement à l'opérateur masquait son éventuelle valeur ou rôle qu'il pouvait posséder, pour lui conférer un rôle localisé de variable élémentaire. Ainsi par exemple dans le langage logique (<a, s(.)>, P(.)), l'expression  ∀a, P(a)  =  P(a) et P(s(a)) et P(s(s(a))) et ..., et vous remarquerez que l'opérateur a dans l'argument de gauche est une variable élémentaire, alors que l'opérateur a dans l'argument de droite est une constante du langage. Ce procédé de masquage est nécessaire pour définir des constructions récursives. Un même nom de variable doit pouvoir désigner de multiple variables localisées à différents endroits.

A priori on peut considérer deux niveaux de sémantiques l'une calculable contenant l'ensemble des mondes calculables où A est satisfait, l'autre définissable contenant l'ensemble des mondes définissables où A est satisfait.

 

 

Le prédicat d'égalité est un prédicat particulier qui possède des propriétés supplémentaires par rapport aux autres prédicats. Ces propriétés font partie des règles de déduction. Elles comprènnent les règles de relation d'équivalence et la meta-règle de congruence. Les règle d'équivalence :

Reflexivité : ∀x, x=x
Symétrie : ∀x∀y, si x=y alors y=x
Transitivité : ∀x∀y∀z, si x=y et y=z alors x=z

La meta-régle de congruence :

Quelque soit un mot T, quelque soit un élément X apparaissant à un endroit dans ce mot, quelque soit un autre mot Y, si nous avons la propriété X=Y alors nous pouvons déduire que le mot T où cette occurence de X est remplacée par Y, est égale à T.

Quelque soit une proposition P, quelque soit un élément X apparaissant à un endroit dans cette proposition sans être quantifié, quelque soit un autre mot Y, si nous avons la propriété X=Y alors nous pouvons déduire la proposition P où cette occurence de X est remplacé par Y.

Il reste à définir un langage formel pour décrire ces deux règles de déduction

 

6) La calculabilité unifie la notion de fonction et de prédicat

Les opérateurs du langage sont souvent sans procédé de calcul propre, mais ils possèdent un procédé de calcul par défaut qu'est le mécanisme de construction même du langage d'opérateurs et de la structure libre associée. Par exemple, étant donné l'opérateur g d'arité 2, on peut définir cette opérateur sans altérer aucunement sa généralité comme l'application suivante g : (x,y)-->g(x,y). Cette application ne possède pas de procédé de calcul propre, et son procédé de calcul par défaut est le mécanisme de construction des mots de l'univers de Herbrand. Si nous appliquons l'opérateur g aux mots a et f(b), nous obtenons simplement le mot g(a,f(b)).

Ainsi tous les opérateurs du langages sont des applications de l'univers de Herbrand sur lui-même.

On peut donner à un opérateur du langage un procédé de calcul propre, c'est à dire un mécanisme autre que celui par défaut, produisant un mot désignants sémantiquement l'élément image. Ce procédé de calcul est un programme écrit dans un langage de programmation qui reste à définir. Par exemple prenons l'opérateur f : x-->f(x) et posons un procédé de calcul consistant à remplacer toutes les a par b et toutes les b par a. L'application de l'opérateur f au mot g(a,b) va produire deux mots, l'expression dite non évaluée f(g(a,b)), et l'expression dite évaluée g(b,a). Et nous résumons la situation par l'égalité entre ces deux mots f(g(a,b))=g(b,a). L'opérateur f s'appellera alors une fonction ou une application. La fonction produit deux mots, l'un correspondant à la construction de la structure libre, l'autre correspondant à l'évaluation du calcul propre. Dans les cas plus complex, il se peut que le calcul propre ne s'arréte jamais, auquel cas l'évaluation de la fonction ne produit rien, appelé l'infinit de Turing, et qui est un oracle.

On peut nommer par h la fonction définie au paragraphe 4.2 :

h = (x --> g(f(x),a))

Notez alors, qu'il y a extention du langage par un nouvel opérateur h(.) et qui possède un calcul propre.

On peut concevoir des calculs propres qui donnent plusieurs résultats, voir une infinité énumérable de résultats. Et par analogie entre le procédé de calcul et la fonction, on définie le concept de démon. Un démon est une représentation d'un procédé de calcul qui produit une liste de mots pouvant être sans fin. Si on étudit la complexité des calculs, on devra concidérer des fonctions ayant une arité de sortie supérieur à 1, permettant de partager des calculs intermédiaires pour le calcul de plusieurs résultats parallèles.

Si on conçoit les opérateurs et les prédicats comme possédant un procédé de calcul propre correspondant à une machine de Turing, alors il n'y a pas de différence substancielle entre un + f et un prédicat P. Peut-on simplifier le langage en unifiant opérateur et prédicat ? Oui, à condition de donner une valeur logique aux éléments, c'est à dire aux mots sachant que si deux mots désignent le même élément ils doivent nécessairement possèder la même valeur logique qui correspondra à celle de l'élément. Le prédicat devient une fonction qui retourne un mot de l'univers de Herbrand, et auquel on s'intéresse à sa valeur logique. L'unification fonction-prédicat affirme seulement qu'il n'existe qu'un seul procéder de calcul général pouvant être mis en oeuvre pour calculer aussi bien les fonctions que les prédicats, qu'est la machine de Turing.

7) La skolémisation à revoir

Thoralf Albert Skolem, mathématicien et logicien norvégien (23 mai 1887 - 23 mars 1963) proposa, de remplacer dans une proposition logique, chaque variable quantifiée existenciellement par des fonctions de choix symbolique, appelées fonction de Skolem. Ce procédé s'appel la skolémisation.

Une skolème est une clause où toute les variables universelles sont qantifiées universellement. Par exemple : ∀x ∀y  ¬R(x,y) ou R(y,x). Cette proposition signifie que la relation R est symétrique.

Une négaskolème est un état où toute les variables universelles sont qantifiées existentiellement. C'est aussi une négation d'une skolème. Par exemple : ∃x ∃y  R(x,y) et ¬R(y,x). Cette proposition signifie que la relation R n'est pas symétrique.

Dans une proposition, les variables quantifiés existentiellement peuvent-elle toujours être résolues et choisies symboliquement ?. Pour le cas des variables indépendantes, cela consiste à choisire une solution, sans même la construire ni la connaitre, et à la nommer en complétant ainsi le langage. Par exemple, nous nous plaçons dans une structure S1 possédant une théorie T1 et un langage L1. Et on considère la proposition ∃x P(x). Puis on procède à une extension du langage pour aboutire à la structure S2.

T1 et ( ∃x P(x) )                      langage L1 = {x, s(.), P(.)}

peut être remplacée par :

T2 et P(c)                               langage L2 = {x, c, s(.), P(.)}

c est une nouvelle constante ajoutée au langage. c représente un élément inconnu étendant la structure S1 en la structure S2. c satisfait P, et la théorie T2 est la même théorie que T1 dans lequel le domaine des quantificateurs a augmenter de L1° à L2°.



Ces deux propositions sont-elle équivalente ? La démonstration doit se faire dans le langage L2, car dans le langage L1 on ne peut pas évoquer l'élément c.  Nous avons évidement P(c) => ∃x P(x), parcontre la réciproque exige que l'élément c ai été choisie tel que P(c).

Et ce choix est-il mécaniquement possible en un temps fini ? Cette question nous replace dans la première structure où :

∃x P(x) = P(x) ou P(s(x)) ou P(s(s(x))) ou P(s(s(s(x)))) ....


Mais on peut passer outre cette exigence






Si on admet l'axiome qui autorise à choisir un élément dans un ensemble non vide inconnu alors...

Lorsque la variable existentielle n'est pas autonomes et dépend d'autres variables universelles, on choisie symboliquement les solutions grace à une fonction de choix symbolique dite fonction de Skoleme, qui constitue un nouvel opérateur d'arité aproprié que l'on ajoutent au langage.Par exemple la proposition suivante :

∀x,∃y,Q(x,y)

peut être remplacée par :

∀x Q(x,f(x))

f(.) est un nouvel opérateur ajouté au langage. f représente une fonction inconnue satifaisant ∀x Q(x,f(x)). La fonction f est construite en choisissant une solution pour chaque valeur de x. Ces deux propositions sont équivalentes si on fait abstraction du choix de dénomination de f, et si on admet l'axiome de choix qui autorise à effectuer une infinité de choix.

Ce dernier axiome n'est pas anondin. En effet, une machine de Turing ne sait pas effectuer une infinité de choix librement. Les choix, s'il sont en nombre infini, sont obligatoirement liés car déterminés par un même programme de taille finie.

Le problèmes ne se pose pas pour les structures finies.

8.2) La skolémisation

La skolémisation d'une proposition logique consiste à remplacer les variables existentielles par des éléments ou opérateurs d'arité aproprié que l'on rajoute au langage, puis à décomposer la proposition en conjonction de clauses, sachant que les quantificateurs ∀, ∃ correspondent respectivement au ET, OU intégré sur tous les éléments de l'univers de Herbrand généralisé. On obtient ainsi une conjonction de skolèmes.

Proposition
Extension du langage
Proposision sans quantificateur existenciel
dans le langage étentu
∃x P(x) e
P(e)
∀y ∃x Q(y,x)
f(.)
∀y Q(y,f(y))
∃x ∀y Q(y,x) e
∀y Q(y,e)
∀y ∀z ∃x K(y,z,x) f(.,.)
∀y ∀z K(y,z,f(y,z))
∀x ∃y ∀u ∃v L(x,y,u,v) f(.),g(.,.)
∀x ∀u L(x,f(x),u,g(x,u))









Etant donné une relation d'équivalence R, on note E/R l'ensemble des classes d'équivalences. Ces classes d'équivalence sont les ensembles de mots de l'univers de Herbrand généralisé équivalents entre eux selon la relation R. On dit que R partitionne E pour produire E/R. Et on applique cela pour la relation d'équivalence particulière qu'est l'égalité. E/= est l'ensemble des classes d'équivalence désignant un même élément.

Mais attention lorsque la strucure n'est plus libre et quelle est donc soumise à une théorie, alors deux mots de l'univers de Herbrand peuvent désigner le même éléments, ou même deux éléments dont il est impossible de prouver qu'ils sont distincts ou non.

Une proposition logique du premier ordre est une composition d'opérations logiques {1, 0, ¬, et, *, ou, =>, <=, <=>, w, +}, d'un ensemble de prédicats d'arité diverse {=(.,.), X, P(.), Q(.,.), R(.,.), K(.,.,.), L(.,.,.,.)} appelé langage de prédicats, d'un ensemble d'opérateurs d'arité diverse {a, b, f(.), g(.,.)} appelé langage d'opérateurs, et d'une séquence de n variables élémentaires {x, y, z, t} chacune quantifiées par un quantificateurs quel que soit ( ∀ ) ou il existe ( ∃ ). L'entier n est le nombre d'inconnues élémentaires, et est appelé le degrés de liberté élémentaire de la proposition ou du langage.

Mais dans une proposition, leurs significations changent délors que l'on précise leurs quantifications. On remarque qu'il n'existe pas de différence entre les éléments constants du langage tels que a, b et les variables élémentaires nommées telles que x, y, z, t.. A savoir que l'on peut quantifier une constante du langage, et se faisant


Le prédicat égale =(.,.)joue un rôle particulier. Il porte la notion élémentaire de l'élément. Et d'une façon plus générale, il peut être remplacé par une relation d'équivalence, c'est à dire par un prédicat R(.,.) satisfaisant la propriété suivante : R est reflexive, symérique et transitive :

∀x, R(x,x)                                                (R est reflexive)
∀x,∀y, ¬R(x,y) ou R(y,x)                          (R est symétrique)
∀x,∀y,∀z, ¬R(x,y) ou ¬R(y,z) ou R(x,z)    (R est transitive)

qui doit jouer le rôle de l'égalité vis-à-vis des autres opérateurs et prédiats. C'est à dire si f(.) et si P(.,.) est un opérateur du langage alors la propriété suivante doi être ajouté :

R(f(x),f(y)) ou ¬R(x,y)
P(x,y) ou ¬P(u,v) ou ¬R(x,u) ou ¬R(y,v)


6) La logique d'ordre 0 et son extention interieur

On considère les expressions booléennes construites à partir des seuls opérations logiques {0, 1, ¬, et, ou }et des n variables booléennes {X, Y, Z, T}. On définie les éléments comme étant ces expressions booléennes à équivalence près.











Les formules dans cette logique d'ordre 1 sont appelée shémas. Ici, le terme de proposition est réservé à la logique d'ordre zéro. Décrivons les qualités que peuvent prendre un shéma ainsi décrit mais sans quantificateur quel que soit ni il existe. Les variables propositionelles sont remplacées par des constantes propositionelles inconnues. Cette opération est appelé skolémisation et consiste à remplacer les inconnues par des constantes supplémentaires ajoutées au langage. (Noter que ces constantes n'ont pas le même type que les constante booléennes.)

Considérons un shémas K utilisant n variables propositionnelles {A1, A2, A3 ..., An}et trois variables booléennes {x,y,z}dites non muettes. Le langage utilisé sera une extention de la logique d'ordre zéro précédement décrite, obtenue en ajoutant sous forme de constante ces n variables propositionnelles et ces trois variables booléennes non muettes. On obtient le langage {¬, et, ou, =>, <=, <=>, w, +, *, x, y, z, A1, A2, A3 ..., An}. x est une constante booléenne. A1 est une constante propositionelle. K est un shéma. Lors d'une évaluation, A1 peut prendre comme valeur toute proposition logique sur un nombre fini quelconque de variables booléennes muettes supplémentaire au langage présent, ou déja existantes dans l'instantiation d'une autre variable propositionnelle utilisée, ou soit non muettes.

Cela signifit que l'on ne peut pas concidérer une à une les variables propositionnelles d'un shéma, car elle sont potentiellements liées entre elles. Nous parlerons donc d'instantiation du jeux complet des n variables propositionnelles {A1, A2, A3 ..., An}dans le langage infini {¬, et, ou, =>, <=, <=>, w, +, *, x, y, z, x1, x2, x3, x4 ...}, mais où chaque valeur propositionnelle est de taille finie.


1) L'extension interieure de la logique d'ordre 0 à une logique d'ordre 1

L'extention interieure de la logique d'ordre zéro à la logique d'ordre 1 consiste à prendre, comme éléments d'un model en cours de construction, les propositions de la logique d'ordre zéro. On définie ainsi un type de variable universelle susceptible d'être égale à n'importe quelle proposition d'ordre 0. De telles variables désignants des propositions logiques d'ordre zéro, utilisent un nombre fini mais non borné de variables booléennes, et peuvent donc avoir un nombre infini de valeurs possibles. Elles constituent des variables universelles, leurs quantificateurs quel que soit et il existe ne peuvent pas être remplacés par une énumération finie de possibilité.



11.1) Les sept qualités possibles d'un schéma

Dans ce nouveau langage permettant de définir les schémas, il y a deux types de constantes ; Celles correspondantes aux variables booléennes qui ont deux valeurs possibles {0,1}correspondant aux deux qualités possibles {vrai, faux}, et celles correspondants aux variables propositionnelles qui ont une infinité de valeurs possibles, mais possédant trois qualités possibles {contradictoire, indéterminé, tautologique} selon qu'une fois développé, leur polynôme associé est nul, non trivial, ou égale à 1, et qui correspond aux sous-ensembles des qualités rencontrées lorsqu'on évalue la proposition pour chaque valeur possible de ses variables booléennes. C'est à dire tautologique = {vrai}, indéterminé = {vrai, faux}, contradictoire = {faux}

Pour une valeur donnée des n constantes propositionnelles, le schéma K(x,y,z,A1,A2,A3...,An) possède une des qualités ; contradictoire, indéterminé, ou tautologique, selon qu'une fois développé, K(x,y,z,A1,A2,A3...,An) est un polynôme nul, ou possédant au moins une variable booléennes (muettes ou non), ou égale à 1.

Dans l'univers des schémas, Il y a autant de qualité qu'il y a de partie non vide de l'ensemble {contradictoire, indéterminé, tautologique}, soit 7 qualités possibles que l'on nomme {absurde, trivial, bivalant, nonabsurde, nontrivial, nonbivalant, libre}et qui correspondent aux sous-ensembles des qualités rencontrées lorsqu'on évalue le schéma pour chaque valeur possible de ses variables propositionnelles. C'est à dire absurde = {contradictoire}, trivial = {tautologique}, bivalant = {indéterminé}, nonabsurde = {tautologique, indéterminé}, nontrivial = {contradictoire, indéterminé}, nonbivalant = {tautologique, contradictoire}, libre = {tautologique, contradictoire, indéterminé}.

Sur ces 7 qualités, seulement 6 sont rencontrées. Voici les exemples canoniques pour les six, et une solution pour la septième.

  1. Absurde {contradictoire} exemple : 0
  2. Trivial  {tautologique} exemple : 1
  3. Bivalant  {indeterminé} exemple : x
  4. Libre {tautologique, contradictoire, indéterminé} exemple : A
  5. Nontrivial {contradictoire, indéterminé} exemple : A et x
  6. Nonabsurde {tautologique, indéterminé} exemple : A ou x
  7. Nonbivalant {tautologique, contradictoire} exemple : A |- 0

Cette logique d'ordre 1 ne possède pas de possibilité d'expression supérieure à notre logique d'ordre 0. Il est nécessaire d'adjoindre de nouveaux opérateurs pour étendre sous domaine d'expression, en tout cas pour atteindre la septième qualité manquante. Cette dernière est atteinte en définissant l'opérateur de démontrabilité |-.

11.2) Le méta opérateur de démontrabilité

On définit le méta opérateur binaire constant, |- , qui représente la relation de démontrabilité, par le procédé récursif suivant :

Soit K, G deux schémas n'utilisant pas l'opérateur |-. Pour chaque valeur possible de leurs variables propositionnelles, nous posons : (K |- G) retourne 1 si (K et ¬G) est contradictoire, c'est à dire une fois développé, est égale au polynôme nul. (K |- G) retourne 0 si (K et ¬G) n'est pas contradictoire, c'est à dire tautologique ou indéterminé, c'est à dire une fois développé, est différent du polynôme nul.

Si l'opérateur |- est appliqué plusieurs fois de façon emboîtée, il faut d'abord évaluer les opérateurs |- appliqué à des schémas sans opérateur |-, et remonter ainsi de suite.

Puis il faut intégrer toutes les valeurs possibles des variables propositionnelles et procéder à la réunion de toutes les qualités produites possibles. Ce qui donne une définition non constructible du méta opérateur |-.

Schéma
Schéma
Schéma évalué
Qualité
du Schéma
(A |- 0)
c(A)
A est contradictoire
Nonbivalant
(¬A |- 0)
c(¬A)
A est tautologique
Nonbivalant
(A |- 1)
c(0)
1
Trivial
(¬A |- 1)
c(0)
1
Trivial
(0 |- A)
c(0)
1
Trivial
(0 |- ¬A)
c(0)
1
Trivial
(1 |- A)
c(¬A)
A est tautologique
Nonbivalant
(1 |- ¬A)
c(A)
A est contradictoire
Nonbivalant
¬(A |- 0)
¬c(A)
A est tautologique ou indéterminé
Nonbivalant
¬(¬A |- 0)
¬c(¬A)
A est contradictoire ou indéterminé
Nonbivalant
¬(A |- 1)
¬c(0)
0
Absurde
¬(¬A |- 1)
¬c(0)
0
Absurde
¬(0 |- A)
¬c(0)
0
Absurde
¬(0 |- ¬A)
¬c(0)
0
Absurde
¬(1 |- A)
¬c(¬A)
A est contradictoire ou indéterminé
Nonbivalant
¬(1 |- ¬A)
¬c(A)
A est tautologique ou indéterminé
Nonbivalant
(A |- A)
c(0)
1
Trivial
(A |- ¬A)
c(A)
A est contradictoire
Nonbivalant
(¬A |- A)
c(¬A)
A est tautologique
Nonbivalant
(¬A |- ¬A)
c(0)
1
Trivial
¬(A |- A)
¬c(0)
0
Absurde
¬(A |- ¬A)
¬c(A)
A est tautologique ou indéterminé
Nonbivalant
¬(¬A |- A)
¬c(¬A)
A est contradictoire ou indéterminé
Nonbivalant
¬(¬A |- ¬A)
¬c(0)
0
Absurde
(A |- B)
c(A et ¬B)
(A et ¬B) est contradictoire
Nonbivalant

Nous pouvons également définire d'autre méta opérateurs :

 


D. Mabboux-Stromberg

/.../

 


Une équation logique, dite de Lewis Carroll (renommée ainsi pour en avoir donné une résolution compréhensible par le grand publique), est une équation plus perfectionnée que celles d'ordre 0 appelé "equations booléennes". Elle est écrite dans un langage augmenté par des prédicats unaires et des variables dites universelles.

Un modèle est un ensemble énumérable d'éléments sur lesquels les prédicats du langage ainsi que les opéateurs d'éléments sont définis. De plus l'ensemble doit être clos par la composition d'opérateurs d'éléments du langage.




Lorsqu'on suppose que le modèle est fini, c'est à dire qu'il possède un nombre finie d'éléments, alors un autre quantificateur est intéressant à définire qu'est le quantificateur majoritaire ( M

Hypothèse
Proposition logique
d'ordre 1
Description
Nombre fini
d'éléments
Mx P(x) Il y a une majorité d'éléments x tel que P(x)=1
Aucune
Mx P(x) Il existe une fonction f injective qui appliqué à tous élément x tel que ¬P(x)
produit un élément f(x) vérifiant P(f(x)).

Mx P(x) = (∀x P(x) ou P(f(x))) et  (∀x ∀y f(x)≠f(y) ou x=y)



III) La théorie de la preuve

Une preuve est une liste de formules respectant des règles de raisonnement. Elle contient une hypothèse qui est une formule, et une conclusion qui est une autre formule. On note par A⊢B la propriété que B est démontrable à partir de A, c'est à dire qu'il existe une preuve ayant comme hypothèse A et comme conclusion B.

1) Le système axiomatique de Hilbert

1.1) Les 3 shémats d'axiomes

A => (B => A)
(A => (B => C)) => ((A => B) => (A => C))
(¬A => ¬B) => (B => A)

1.2) La règle d'inférence dite du Modus Ponens

A, A=>B --> B

2) La déduction naturelle

2.1) Les 9 règles d'inférences

  1. Les conjonctions de clauses
  2. Les disjonctions d'états
  3. Le corps perçu par les conjonctions de clauses de validité impaire
  4. Le corps perçu par les disjonctions d'état d'invalidité paire
  5.  

     

  6.  

    4) Langage de programmation

    Comme nous construisons la logique à partir des programmes, il convient d'abord de formaliser le langage de programmation avant de pouvoir formaliser la logique. Ce langage de programmation doit contenir les mécanismes de construction des fonctions calculables, c'est à dire les mécanismes de construction des fonctions primitives-récursives et le mécanisme de la minimalisation non bornée. (à vérifier)

    On commence par présenter ce qu'est la récurrence générale et ce qu'est la récurcivité générale s'appliquant dans un univers de Herbrand.

    4.1) La récurrence générale

    On définie d'une manière plus générale la récurrence appliquée à une structure autre que celles des entiers. La récurrence générale met simplement en oeuvre le principe de clôture par composition close, un principe consubstantiel à la notion de structure. A savoir, par exemple : Si des éléments a, b satisfont une propriété P(.), c'est à dire si nous avons P(a) et P(b), et que des opérateurs f(.), g(.,.) respectent la propriété P(.) sur la structure <a,b,f(.),g(.,.)>, c'est à dire si pour tout élément x de la structure <a,b,f(.),g(.,.)> nous avons P(x) => P(f(x)) et si pour tout couple d'éléments x et y appartenants à la structure <a,b,f(.),g(.,.)> nous avons (P(x) et P(y)) => P(g(x,y)), alors nous pouvons déduire par récurrence généralisée que tous les éléments de la structure <a,b,f(.),g(.,.)> satisfont la propriété P(.).

        P(a)
        P(b)

        ∀x∈<a,b,f(.),g(.,.)>, P(x) => P(f(x))
        ∀(x,y)∈<a,b,f(.),g(.,.)>2, P(x) et P(y) => P(g(x,y))
    =>
    ∀x∈<a,b,f(.),g(.,.)>, P(x)

    La récurrence générale est ici décrite pour un cas particulier qu'est le langage logique (<a,b,f(.),g(.,.)>, P(.)). Comment décrire formellement la récurrence générale dans le cas général ? Quelle langage devons-nous adopter ?.

    4.2) Les fonctions primitive-récurcive

    On note une séquence de variables comme par exemple : u = (u1, u2).

    Une fonction primitive récurcive r d'arité 2+1 peut se construir par exemple à partir de 4 opérateurs a, b, f(.), g(.,.), formant implicitement une structure libre <a,b,f(.),g(.,.)>, et à partir de 4 fonctions r1, r2, r3, r4 , une fonction par opérateur a, b, f, g, d'arité égale à 2 plus deux fois l'arité de l'opérateur correspondant. La fonction r se programme alors comme une suite d'alternatives :

    r(u, a) = r1(u)
    r(u, b) = r2(u)
    r(u, f(x)) = r3(u, x, r(u,x))
    r(u, g(x,y)) = r4(u, x, y, r(u,x), r(u,y))

    Notez que les dernières alternatives sont récurcives. La fonction r est réappelée dans un ou plusieurs arguments. L'opérateur r se note à l'aide du méta-opérateur d'alternative | comme suit :

    r = (u, a) --> r1(u)  |  (u, b) --> r2(u)  |  (u, f(x)) --> r3(u, x, r(u,x))  |  (u, g(x,y)) --> r4(u, x, y, r(u,x), r(u,y))

    C'est une liste d'alternatives à prendre dans l'ordre. Lors de l'appel r(w)w est une séquence de 2+1 termes clos, la fonction r va tester l'unification de w avec la première entête (u,a). Si l'unification réussi alors la fonction r retourne r1(u), et si l'unification échoue alors on passe à l'alternative suivante, etc...

    La récurcivité primitive peut ainsi être construite indépendament des entiers. De tel sorte que les entiers ne sont plus une structure particulière, nécessaire à la récurrence.

     


    les projections pi_ j^i
    Les fonctions correspondant aux opérateurs générateur
    Les fonction reccurcive primitive

     

    Niveau n°6 (Programmation primitive récurcive) (Arret borné)

    Contient tous les opérateurs qu'il est possible de construire à partir des précédents à l'aide de la programmation primitive récurcive, c'est à dire programmés par composition et par récursion primitive (ou dit autrement dans un langage de programmation impératif, programmés uniquement avec des boucles "for" et non avec les boucles "while", et sans modifier les indexes des boucles "for" autrement que par augmentation, ni modifier les bornes des boucles "for" autrement que par réduction, permettant ainsi de garantir l'arrêt borné du programme.)

     

    3) Les fonctions propositionelles et fonctions élémentaires

    Un élément exprimable c'est à dire un mot appartenant à l'univers de Herbrand, est une composition close d'opérateurs. Par exemple si le langage d'opérateurs est <a,b,f(.),g(.,.)> alors les 3 compositions closes f(a), b, g(g(a,b),f(a)) représentent 3 mots de l'univers de Herbrand, désigant 3 éléments non nécessairement distincts, dits exprimables. Les éléments sont beaucoup plus mystèrieux. Dans notre approche constructive, on ne manipule pas les éléments directement mais seulement les mots qui les désignent et qui font partie d'un langage formant une structure libre qu'est l'univers de Herbrand.

    Le prédicat d'égalité est un prédicat particulier, noté =, qui peut être ajouté à la liste des prédicats du langage, et qui est associé à un ensemble de règles de déduction (voir théorie d'égalité).

    2) Les opérateurs d'arité 0

    On augmente le langage en ajoutant n variables élémentaires nommées {x,y,z,t}. L'univers de Herbrand est alors étendu <a, b, f(.), g(.,.), x, y, z, t>. Les variables rajoutées dans le langage désignent des éléments sans apriorie, comme l'ajout d'éléments inconnus mais qui peuvent s'avéré égale à des éléments déjà préexistant. Cela constitue une extension du langage. Il n'y a pas de différence entre une constante élémentaire du langage et une variable élémentaire rajoutée au langage. Ce sont tous les deux des opérateurs d'arité 0. Grace à cette extension on peut désigner de nouveaux éléments tel que par exemple f(x), y, g(y,f(a)), ce sont 3 mots de l'univers de Herbrand, désignant 3 éléments non nécessairement distincts.

    Néanmoins la raison pour laquel on ajoute des variables nommées au langage s'avère rarement pour faire des extensions élémentaires mais pour les utiliser comme variable, permettant de définir des fonctions, et d'intégrer sur l'ensemble de tous les éléments exprimables l'une des opérations logiques (ET), (OU), qui correspondent respectivement à la quantification quel que soit (∀), il existe (∃).

    3) Les fonctions

    Pour définir des fonction unaire on introduit l'opérateur de définition de fonction d'arité 2 noté -->. Le premier argument comprend un opérateur d'arité zéro de la présentation qui jouera le rôle de la variable muette, et le deuxième argument comprend le corps de la fonction c'est à dire ce que retourne la fonction. Par exemple :

    x --> g(f(x),a)

    Dans cette expression x désigne une variable muette de la fonction. Dés lors il n'est plus possible d'utiliser la constante x dans le corps de la fonction si celle-ci avait une signification élémentaire antérieur, car elle est masquée par l'environnement des variables muettes locales à la fonction. Et cela n'est pas un vice. Il est normale que le langage nécessite deux opérateurs pour effectuer une telle opération, pour que l'un ne soit pas masqué par l'autre.

    L'appel de cette fonction sur un argument va produire un mot qu'est le corps de la fonction dans lequel x est substitué par l'argument. Par exemple :

            (x --> g(f(x),a)) (g(b,b)) = g(f(g(b,b)),a)

    L'argument doit être un mot de l'univers de Herbrand. L'argument peut donc contenir la constante x, et cela n'introduit pas de boucle sans fin car nous ne sommes pas dans le concept d'unification, seuls les variables x placées dans le corps de la fonction sont remplacées par l'argument.

    Pour définir des fonction n-aire on introduit un opérateur de définition de fonction d'arité n+1 noté également par -->. Les n premiers arguments comprenent les opérateurs d'arité zéro qui joueront le rôle de variables muettes, et le dernier argument comprend le corps de la fonction. Par exemple :

    (x,y) --> g(x,g(y,x))

    Les fonctions sont aussi considérées comme des énumérateurs. On suppose que le n-uplet de variables muettes parcourt l'ensemble des n-uplet de mots de l'univert de Herbrand selon un algorithme canonique. Il en résulte que la fonction parcourt un ensemble image.

    ---- 9 Décembre 2012 ----

     


    4.4) Les structures du premier ordre.

    On définie une structure par sa théorie qui est une proposition logique du premier ordre, et par son langage comprenant un nombre fini d'opérateurs et de prédicats. Et on est obligé de préciser le langage car celui-ci peut être plus grand que celui de la théorie. On redonne ainsi un rôle plus important au langage ce qui réequilibre la notion de structure, et qui permet de se consacrer à la recherche du 3ième pilier, l'aspect dynamique de la structure, qu'est son programme.

    Grace à notre définition prudente des quantificateurs, on s'oblige pour toute extension du langage à préciser explicitement si les éléments nouvellement exprimables doivent satisfaire à la théorie de la structure, auquel cas, la théorie en cours change puisque le sense des quantificateurs change, et elle peut même en devenir incohérente. Où plus exactement, des théories incohérentes peuvent devenir cohérentes dans un langage limité ne permettant pas d'accéder à la contradiction.

    Il est possible d'ajouter des éléments qui ne respectent pas la théorie, on réhabilite ainsi la construction de nouvelles structures par simple ajout.

 

 

Un prédicat est non-calculable ssi il est ni décidable ni réfutable, c'est à dire, s'il n'existe pas de programme de taille finie qui appliqué à n'importe quelle élément valide, calcul en un temps fini le résultat booléen 1, et qu'il n'existe pas de programme de taille finie qui appliqué à n'importe quelle élément invalide, calcul en un temps fini le résultat booléen 0.

Attention aux homonymes, non calculable ne signifie pas non-calculable. Non calculable signifie qu'il n'existe pas de programme de taille fini qui appliqué à n'importe quelle élément de l'univers de Herbrand, calcul en un temps fini le résultat booléen.

on ne considérera que des mondes calculables, les seuls que nous pouvons construire.

 

C'est ce que nous faisons en construisant des prédicats affirmables et des prédicats réfutables.

Un prédicat unaire est affirmable ssi restreint aux seuls éléments valides pour ce prédicat, il est calculable. Le prédicat affirmable correspond à un état calculable affirmatif dans le langage logique comprenant ce seul prédicat. On entend par état affirmatif une conjonction de littéraux affirmatifs. Un prédicat affirmable correspond alors à un énumérateur de tous les éléments valides selon lui. Un tel prédicat ne dit jamais Non. Pour les éléments non valides, le prédicat ne donne pas de réponse en un temps fini. Cela signifie que la réfutation par ce prédicat peut constituer un oracle.

Un prédicat unaire est réfutable ssi restreint aux seuls éléments invalides pour ce prédicat, il est calculable. Le prédicat réfutable correspond à un état calculable négatif dans le langage logique comprenant ce seul prédicat. On entend par état négatif une conjonction de littéraux négatifs. Un prédicat réfutable correspond à un énumérateur de tous les éléments invalides selon lui. Un tel prédicat ne dit jamais Oui. Pour les éléments valides, le prédicat ne donne pas de réponse en un temps fini. Cela signifie que l'affirmation par ce prédicat peut constituer un oracle.

Un prédicat unaire est calculable ssi il est affirmable et réfutable, c'est à dire s'il est capable d'énumérer tous ses éléments valides et d'énumérer tous ses éléments invalides.

3) La calculabilité et les mondes

Par exemple considérons le langage d'opérateurs `"{"a, b, f"(.)", g"(.,.)}"`. C'est une structure libre `"<"a, b, f"(.)", g"(.,.)>"` engendrée par les 4 générateurs `a, b, f, g`. Cette structure contient tous les mots qu'il est possible de construire par composition close avec ces générateurs. Cette structure constitue l'univers de Herbrand.

Une structure libre engendrée par un nombre fini de générateurs est énumérable. Cela signifie qu'il existe un programme de taille finie qui énumère tous les mots possibles. Le mécanisme de cloture par composition close constitue cet énumérateur des mots et donc des éléments de la structure libre. On choisie un ordre d'énumération des mots selon la taille, le niveau ou la complexité de composition des mots (voir Langage d'opérateurs ).

Le produit directe de telles structures est encore énumérable, autrement dit, les couples d'éléments de l'univers de Herbrand son énumérables, c'est à dire qu'il existe un programme de taille finie qui les énumère. De même, les suites finies d'éléments de l'univers de Herbrand son énumérables, et davantage encore, les suites infinies calculables sont énumérable comme le sont les programmes de taille finie qui les énumère. On entend par suite calculable, une suite infinie de valeurs telles qu'il existe un programme de taille finie qui les énumère.

On peut étendre ces structures libres en ajoutant une liste infinie énumérable de générateurs. Une structure libre engendrée par un ensemble énumérable de générateurs est encore énumérable.

Un monde est un ensemble de présuposés permettant de trancher tout les formules simples.

Pour formaliser les mondes, un moyen simple consiste à utiliser l'axiome du choix. C'est à dire la capacité d'effectuer une infinité de choix arbitraires. Cette capacité nous permet de définir les suites formelles de valeurs, c'est à dire de poser une infinité de valeurs arbitraires, et nous permet de définir les états formels c'est à dire une conjonction infinie de littéraux arbitraires.

Un état formel est dit cohérent s'il ne contient jamais à la fois un littéral et sa négation, et il est dit complet si chaque littéral possible y apparait au moins une fois de façon soit affirmative ou soit négative. Il est calculable à la place de formel s'il existe un programme de taille fini qui énumère tous ses littéraux. Il est dit affirmatif si tous ses littéraux sont affirmatifs. Il est dit négatif si tous ses littéraux son négatifs.

Un monde détermine tous les littéraux c'est à dire tous les prédicats de base pour tous les éléments possibles. Chaque prédicat de base peut être définie sous forme d'une suites formelles qui passe en revue la liste de tous les éléments (ou les couples d'éléments dans le cas d'un prédicat binaire) pour lui affecter une valeur booléenne décidée par le prédicat. Et cela revient au même de définir chaque prédicat de base par un état formel complet et cohérent dans le langage logique restreint au seul prédicat en question, et qui attribut à chaque élément (ou à chaque couples d'éléments dans le cas d'un prédicat binaire) une valeur booléenne décidée par le prédicat. Prenons un exemple :

Prédicats de base définie par des suites formelles, cela correspond à leur graphe :

`V=0`
`P=((a,1),(b,0),(f(a),1),(f(b),1),...)`
`R=((a,a,0),(a,b,0),(b,a,1),(b,b,0),(a,f(a),1),...)`

Prédicats de base définie par un état formel :

` ¬V`
`P(a) "et" ¬P(b) "et" P(f(a)) "et" P(f(b)) "et" ... `
`¬R(a,a) "et" ¬R(a,b) "et" R(b,a) "et" ¬R(b,b) "et" R(a,f(a)) "et" ... `

Un monde correspond à un état formel complet et cohérent.

Tout est bien qui finit bien dans le meilleur des mondes me direz-vous..., à part que cela ne convient pas, car nous avons utilisé un outils qui ne nous appartient pas, un oracle que seul les dieux peuvent nous conférer, celui d'effectuer une inifnité de choix arbitraires, celui d'utiliser de façon effective une fonction non calculable, et donc qui est rendu calculable par magie en quelque sorte, somme-toute une chose qui n'existe pas.

Si on adopte une approche constructive, plus paresseuse et plus prudente, il convient alors de se restreindre aux seuls objects que l'on peut construire. La règle en la matière est :

« Parmis les suites comprenant une infinité de valeurs, on ne peut construire et donc utiliser que les suites calculables c'est à dire dont les valeurs sont énumérés par un programme de taille finie ».

Un prédicat unaire est calculable ssi il existe un programme de taille finie dont l'arrêt est sûr, qui appliqué à n'importe qu'elle mot de l'univers de Herbrand donne comme résultat la réponse du prédicat. Et cela revient au même de définir le prédicat par un état calculable complet et cohérent dans le langage logique restreint au seul prédicat en question. On remarque alors que cet état calculable complet et cohérent se scinde en la conjonction de deux états, l'un étant calculable affirmatif et l'autre étant calculable négatif, et la réunion des deux doit être complet.

On se restreint à ne considérer que les seuls objects que l'on peut construitre. Mais il n'y a pas de contrainte sur la nature des objects, la seul contrainte est qu'ils soient constructibles, on peut donc construire qu'une moitier d'objet, formant en quelque sorte des demi-objects, des demi-prédicats ou prédicats incomplets, et des demi-mondes ou mondes incomplets.

Un prédicat unaire est calculable ssi il est capable d'énumérer tous ses éléments valides et d'énumérer tous ses éléments invalides.

Le prédicat détermine de façon calculable ses éléments affirmables et ses éléments réfutables, et il peut être amené à déterminer de façon non calculable ses éléments valides et ses éléments invalides. Du point de vu intuitionniste seul les deux premières notions existent.

Pour tout prédicat, chaque élément est soit valide ou invalide par contre il peut exister des éléments ni affirmables ni réfutables. On les appelle éléments indécis. Et cela constitue une troisième valeur logique qu'est l'infini de Turing, notée `oo`.

L'introduction de la notion de calculabilité dans la logique ajoute cette troisième valeur logique `oo`. Cette valeur correspond à la non réponse d'un programme, au fait que le programme ne s'arrête jammais. Une opération logique est un programme. Une valeur logique est le résultat du programme ou son non-résultat. Mais on ne peut pas utiliser de façon effective des opérateurs logiques non calculables tel que celui qui convertirait l'infini de Turing `oo` en une réponse Oui ou en une réponse Non.

Si on s'en tient qu'aux suites calculables selon les préceptes intuitionnistes, on se doit d'abandonner pour un prédicat unaire les notions d'éléments valides et d'élément invalides au profit des notions constructives d'éléments affirmables et d'éléments réfutables. Tout prédicat unaire comprend deux énumérateurs, un énumérateur des éléments affirmables et un énumérateur des éléments réfutables.

**

On définit constructivement tout prédicat unaire comme composé de deux énumérateurs, un énumérateur des éléments affirmés et un énumérateurs des éléments réfutés. Le prédicat est calculable si la réunion des deux énumérateurs constitue un énumérateur de tous les éléments c'est à dire si la réunion des éléments affirmés et des éléments réfutés par le prédicat couvre l'ensemble de tous les éléments, autrement dit s'il n'y a pas d'élément indécis. Le prédicat est non-calculable s'il existe des éléments ni affirmables ni réfutables, appellés éléments indécis.

Un monde calculable est un monde où chaque prédicat de base est complet et calculable. Le monde calculable définie chaque prédicat de base par un programme de taille finie dont l'arrêt est sûr et qui donne la valeur du prédicat pour tous les mots de l'univers de Herbrand. Un monde calculable correspond à un état calculable complet et cohérent.

Pour définir un monde calculable, il faut définir son schéma c'est à dire le langage logique dans le quel il s'inscrit, par exemple le langage `"(<"a, b, f"(.)", g"(.,.)>", V, P"(.)", R"(.,.))"`. Puis il faut programmer chaque prédicat de base par un programme de taille finie et dont l'arrêt est sûr. Cela consiste à programmer `V`, `P"(.)"`, et `R"(.,.)"` mais de telle sorte que l'arrêt soit sûr. Et nous voyons bien que, construisant la logique à partir des programmes, il est nécessaire de formaliser la programmation avant de pouvoir formaliser la logique, ce que nous verrons au chapitre 12.

Dans un monde calculable, une formule simple est toujours évaluable en un temps fini.

Un monde affirmatif est un monde où chaque prédicat de base est affirmatif. Un prédiciat affirmatif est un énumérateur des éléments affirmables. Le monde affirmatif définie chaque prédicat de base par un programme de taille finie qui énumère leurs éléments affirmables.

Symétriquement, un monde négatif est un monde où chaque prédicat de base est affirmatif. Un prédiciat négatif est un énumérateur des éléments réfutables. Le monde négatif définie chaque prédicat de base par un programme de taille finie qui énumère leurs éléments réfutables.

 

Et il convient aussi d'envisager le cas où le prédicat est incohérent, c'est à dire, affirme à la fois pour un élément sa validité et son invalidité. Ce cas de figure introduit une quatrième valeur logique qu'est l'incohérence noté `⊥`.