Sommaire :
La théorie des ensembles n'est pas le moyen le plus pertinent pour fonder les mathématiques. Il parrait plus judicieux de commencer par la théorie des suites qui est plus simple et qui fait partie de l'informatique. Et dans un second temps, de passer de la suite à l'arrangement, en distinguant tout élément de par sa place occupée, puis de passer de l'arrangement à l'ensemble en faisant abstraction de l'ordre. C'est d'ailleurs ce qui se fait d'une certaine façon, car lorsque la difficulté apparait, on commence par étudier des ordinaux qui représentent les arrangements et les arrangements transfinies avant d'étudier des cardinaux qui représentent les ensembles.
La théorie des ensembles, dans sa recherche de cohérence, est définie dans le langage logique du premier ordre. Et là encore, la logique du premier ordre ne parrait pas le moyen le plus pertinent pour fonder les mathématiques. Il parrait plus judicieux d'user d'emblès des logiques d'ordres supérieurs, qui déploie toutes les capacitées de calcul dans les mécanismes de raisonnement. Car raisonner ce n'est que calculer. Cela relativise toute modélisation, intégrant le modèle comme un autre langage, et mettant l'accent sur les mécanismes de traduction qui permettent de passer d'une logique à une autre, d'un langage à un autre.
Néanmoins, on conçoit bien qu'il peut être plus simple d'aborder la question du fondement en étudiant quelque cas particulier, bien circonscrit, tel que les premières théories des ensembles écrites dans ce langage logique du premier ordre. Alors il convient de décrire préalablement ce langage logique du premier ordre, ainsi que les règles de raisonnement qui s'y appliquent. Ces règles nous rappellent que le raisonnement n'est qu'un calcul. Déduire, c'est calculer.
Un fondement mathématique, pour être incontestable à notre époque, doit reposer sur un mécanisme parfait... au sens de la mécanique classique. Les mathématiques sont un jeu de construction, un jeu de légo, où chaque pièce s'encastre exactement dans un édifice servant de démonstration. Rien ne relève du mystère, tout est trivial..., c'est l'aspect exacte de la science mathématique. Le démonstrateur n'est finalement qu'une machine, une machine idéale, composée de rouages parfaitement emboités et sans aucun jeu. Ces machines sont décrites à l'aide d'un langage formel.
Lorsque les structures étudiées sont finies, leur exactitudes et leurs fondations ne posent pas de problème à notre échelle. Parcontre, l'introduction de l'infini, qui est forcement hors échelle, se construit de façon indirecte comme un infini potentiel, et cela se fait de plusieurs façons possibles par l'ajout de règles de déduction spécifiques, et qui sont souvents incompatibles entre-elles, définissant ainsi plusieurs concepts de l'infini. Lesquelles choisir ?.... Il faut s'interresser aux raisons de toutes ces constructions, des mécanismes de déduction, des langages formels dans lesquel ils opèrent, des sémantiques qu'elles portent, et leur multiples variantes possibles..., et à leurs conséquences..., car ce sont là des choix politiques.
Tout est langage. Dans une démarche minimaliste où l'on ne veut poser aucune hypothèse, où l'on ne veut dépendre d'aucune prémisse, le premier choix qu'il convient de faire est de définir un langage. Et ce choix va limiter notre pouvoir d'expression tout en nous en donnant un.
On choisit un langage d'opérateurs. Et on choisit des opérateurs d'arité fixe, parce que l'étude des opérateurs d'arité variable montre qu'ils peuvent toujours être remplacés de façon équivalente par deux opérateur binaires.
Un language d'opérateurs est défini par sa présentation qui est un ensemble énumérable d'opérateurs. Par exemple la présentation `L= {a,b,f"(.)",g"(.,.)"}` désigne deux opérateurs zéro-aire `a` et `b` qui constituent des éléments, un opérateur unaire `f` et un opérateur binaire `g`. Les opérateurs `{a,b,f"(.)",g"(.,.)"}` sont dit générateurs car ils engendrent le langage par composition close.
Un terme est une composition close d'opérateurs appartenant à `L`. L'ensemble des termes du langage forme le domaine de Herbrand que l'on note `"<"L">"` ou directement `"<"a,b,f"(.)",g"(.,.)>"` :
`"<"L">" = {a, f(a), f(f(a)), f(b), f(g(b,a)), g(a,b),...}`
C'est l'ensemble des éléments que l'on peut construire, ou désigner, avec le langage `L`.
Le « langage `L` » désigne l'ensemble `"<"L">"` c'est à dire le domaine de Herbrand, et réciproquement « la présentation du langage `<L>` » désigne l'ensemble `L`. La présentation du langage est l'ensemble des opérateurs générateurs du langage. Ces opérateurs sont dits générateurs parcequ'ils engendrent le langage `L`.
Par contre les opérateurs défini par exemples comme suit : `x|->g(x,x)`, `(x,y)|->g(y,x)`, `x|->f(f(x))` n'appartienent pas à la présentation de `L`, et donc ne sont pas des opérateurs générateurs. Néanmoins Ils ont quand-même un lien fort avec langage d'opérateurs en question puisque leur définition s'écrivent dans ce langage en question augmenté du méta-connecteur `vecx|->` qui précise l'ordre des variables muettes Autrement dit, Ils sont définissables selon le niveau 3 (composition générale) dans le langage en question.
On remarque que les opérateurs générateurs d'arité `n` restreints au domaine de Herbrand sont des applications injectives distinctes de `"<"L">"^n"↪""<"L">"`, et que les opérateurs générateurs d'arité `0` sont des éléments distincts de `"<"L">"`.
Le but d'un langage est de désigner autre chose que lui-même. Un terme désigne un élement. Le terme est le signifiant. L'élément est le signifié. Dans une démarche constructive, cette séparation se fait dans un premier temps, à l'identique, de telle sorte que deux termes distincts désignent deux éléments distincts. On parlera d'une désignation injective. L'ensemble des termes est regroupé dans le langage. L'ensemble des éléments est regroupé dans la structure qui est le domaine de Herbrand, et qui est dite libre du fait de cette désignation injective c'est à dire telle que deux termes distincts désignent nécessairement deux éléments distincts.
Ainsi le langage d'opérateurs `L` définie une structure libre, appelée aussi le domaine de Herbrand, noté `"<"L">"`, qui comprend toutes les compositions closes possibles d'opérateurs générateurs, et que nous appellons termes ou éléments. Par exemple le terme `g(a,f(a))` désigne un élément. Et deux termes distincts désignent obligatoirement deux éléments distincts, principe d'une désignation injective qui ne perd aucune information.
On remarquera alors, que le langage d'opérateurs n'apporte aucune information sur la situation des éléments qu'il désigne. Il ne fait que leur donner un nom, et il définit par ailleurs chaque opérateur générateur comme une injection dans l'ensemble des éléments désignables, ou constructibles, par le langage. Par exemple si l'opérateur `f"(.)"` fait partie de la présentation du langage, alors quelque soit les éléments `x` et `y` désignables par ce langage, nous avons la propriété suivante `x"≠"y => f(x)"≠"f(y)`. Remarquez que cette formulation ne fait pas encore partie de notre langage formel puisque les symboles `"="` et `"≠"` n'y sont pas encore définis. C'est aussi pourquoi à cette étape, le langage d'opérateurs ne peut définir qu'une structure libre.
On accordera le rôle qui consiste à apporter une information sur la situation des éléments, à une autre sorte d'opérateur appelé prédicat. Le prédicat prend en argument un n-uplet d'éléments et retourne comme résultat non pas un élément mais une information que nous appellons prédication, sur ce n-uplet d'éléments. Notez qu'à ce stade, nous n'avons pas définie le type des prédications, à quoi sont-elles égales ? C'est une étape importante dans la définition de la logique, et nous allons faire le choix classique de considérer la prédication comme un inconnu booléen. En effet, la plus petite quantité d'information atomique est le bit, ou autrement dit, la case mémoire contenant un booléen, autrement dit, la variable boléenne. Toutes les autres formes d'information peuvent être construites à partir de variables booléennes. C'est pourquoi on choisit des prédications booléennes. Déslors, Le prédicat n-aire devient une fonction caractéristique. Il partitionne en deux, l'ensemble des n-uplets d'éléments désignables par le langage d'opérateur utilisé. Autrement dit, il définit un sous-ensemble au sens classique, de l'ensemble des n-uplets d'éléments désignables.
Un langage prédicatif se défini par un langage d'opérateurs `L` complété d'un ensemble énumérable de prédicats. Conventionnellement, les opérateurs générateurs sont notés en premier en minuscule et la liste est entourée de crochet `"< >"`, puis les prédicats sont notés en second en majuscules et placés après, et la liste est entourée de braquette `{ }`. Par exemple, le langage prédicatif `"<"a,b,f"(.)>", {K, E"(.)",R"(.,.)"}` désigne deux opérateurs générateurs d'arité zéro `a` et `b` qui constituent deux éléments distincts, un opérateur générateur unaire `f` qui appliqué à un élément quelconque `x` produit l'élément désigné par `f(x)`, un prédicat d'arité zéro `K` qui constitue un paramètre boolean, un prédicat unaire `E` qui appliqué à un élément quelconque `x` produit un booléen, autrement dit, un ensemble d'éléments `E`, et enfin un prédicat binaire `R` qui constitue une relation, et qui appliqué à un couple d'éléments quelconques `(x,y)` produit la prédication `R(x,y)`, autrement dit, un ensemble de couples d'éléments que l'on note avec la même lettre `R`.
Le langage d'opérateur regroupe tous les termes qui sont par définition des compositions closes d'opérateurs générateurs du langage, et forme le domaine de Herbrand. Par exemples : `a, f(a), f(f(b))`.
Le langage prédicatif regroupe toutes les prédications qui sont obtenues par la composition d'un prédicat du langage par des termes du langage d'opérateurs. Par exemples : `K, E(a),R(a,f(b))`
On a ainsi fait le choix qui accorde la plus grande liberté possible au langage, tout en séparant opérateurs générateurs et prédicats. Les opérateurs générateurs nomment les éléments, et donc construisent la structure libre associée. Les prédicats sont les seules composantes du langage à contenir de l'information, une information booléenne sur les n-uplets d'éléments, en indiquant s'il appartiennent où non à un ensemble (l'ensemble portant le même nom que le prédicat). Les prédicats construisent à partir de la structure libre associée, l'univers associé. C'est un réseau infini de cases mémoires, une matrice infinie où chaque prédicat zéro aire, chaque élément de la structure libre complété par chaque prédicat unaire, chaque couple d'éléments de la structure libre complété par chaque prédicat binaire..., chaque n-uplets d'éléments de la structure libre complété par chaque prédicat n-aire..., appelé aussi adresse mémoire, y possèdent une case mémoire distincte contenant une valeur booléenne pouvant être définie librement. Dans l'exemple `"<"a,b,f"(.)>", {K, E"(.)",R"(.,.)"}`, cela revient à la libre définition d'une valeur booléenne `K`, d'un ensemble `E` d'éléments désignables, et d'un ensemble `R` de couples d'éléments désignables.
La démarche pour fonder les ensembles passe par la définition informatique d'une catégorie d'ensembles plus simples que sont les ensembles de n-uplets d'éléments désignables.
La syntaxe décrit le signifiant, tandis que la sémantique décrit le signifié. Chaque terme détermine un élément du monde. Chaque prédication détermine une caractéristique du monde. Quelle est cette caractéristique ? qu'est ce que désigne une prédication ? Ce sont les appartenance aux ensembles prédéfinis vus précédement. Dans l'exemple, c'est le paramètre booléen `K`, les ensembles `E` et `R`. Mais il est possible de répondre à cette question d'une façon plus générale, sans y répondre vraiment, en se plaçant à une échelle d'ordre supérieur, simplement par une définition, en répondant à la question « Qu'elle est sa sémantique ? ». La sémantique d'une prédication est l'ensemble des mondes qui la satisfait.
La prédication apporte une information sur son n-uplet d'éléments qui lui sert d'argument, et détermine ainsi une caractéristique du monde. Le monde est une structure qui est enrichie de cette information pour chaques prédications.
Le choix classique impose le tiers exclus. C'est à dire qu'on admet par principe, qu'un monde satisfait ou ne satisfait pas une prédication, et qu'il n'y a pas d'autre alternative. Cela symétrise l'affirmation et la négation. Cela a pour conséquence de rendre booléen la caractéristique que représente la prédication. Deuxième raison pour laquelle les prédications représentent des variables booléennes.
On ajoute le connecteur logique de négation `¬` dans notre langage formel pour pouvoir écrire que la prédication `R(a,b)` est égale à `0` en notant simplement `¬R(a,b)`, et que la prédication `R(a,b)` est égale à `1` en notant simplement `R(a,b)`. Les uns sont appellés littéraux négatifs car ils sont préfixés par le connecteur de négation `¬`, et les autres sont appelés littéraux affirmatifs. Les prédications se regroupe alors les littéraux affirmatifs et les littéraux négatifs.
Après ce choix du tiers exclus, une prédication peut être affirmative ou négative, et correspond exactement à un littéral.
On a ainsi fait le choix classique qui considère chaque prédication comme un inconnu booléen. Par exemple la prédication `R(a,f(f(a)))` désigne un inconnu booléen. Et deux inconnus booléens sont distincts, c'est à dire constituent deux mémoires booléennes d'adresses distinctes, si les prédications qui les désignent sont d'expression distinctes. Et on remarque qu'un prédicats d'arité `0` est une variable booléenne. Et on remarque qu'un prédicat d'arité `n` restreint au domaine de Herbrand `"<"L">"`, est une application de `"<"L">"^n"→"{0,1} `. Un prédicat est donc une fonction caractéristique. Un prédicat d'arité `n` définit donc un ensemble de n-uplet d'éléments désignables. Et on désigne cet ensemble par la même lettre que le prédicat. Par exemple :
`R(a,b) <=> (a,b)"∈"R`
`¬R(a,b) <=> (a,b)"∉"R`
Chaque prédication est une case mémoire contenant un booléen. L'ensemble de toutes ces cases mémoires constituent l'univers. Un monde est une instanciation de cet univers, c'est à dire dans lequel chaque case mémoire est fixée à une valeur `0` ou `1`. L'univers est l'ensemble des mondes possibles. Il y a donc deux façons de percevoir ce qu'est l'univers. C'est une liste des cases mémoires booléennes qui permet de définir complétement un monde, ou bien c'est l'ensemble des mondes possibles.
Là où il faut être prudent, c'est que ces mondes sont constitués d'une infinité énumérable de cases mémoires booléennes et donc sont suceptibles de contenir une quantité d'information infinie ce qu'aucun objet physique réel n'est capable de faire. Et donc, il y a deux sortes de monde ;
Dans ce dernier cas, il faut admettre que ces mondes sont immanents puisque non-constructibles. Ils sont donc préalablement définis par une infinité de choix arbitraires que nous ne pourrions évidement pas créer nous-même.
Le monde `M` est dit « satisfaire une prédication `R(a,b)` », ce qui ce note `M"⊨"R(a,b)`, si et seulement si la prédication `R(a,b)` correspond bien à l'information mémorisée par `M` à l'adresse `R(a,b)`. La signification de la prédication `R(a,b)` est que le couple `(a,b)` appartient à l'ensemble `R`. La sémantique de la prédication `R(a,b)` est donné par l'ensemble des mondes la satisfaisant :
`R(a,b) <=> (a,b)"∈"R`
`R(a,b) ≡ {M "/" M"⊨"R(a,b)}`
Comme les booléens se composent à l'aide des connecteurs booléens, les littéraux se composent avec ces mêmes connecteurs, appelés pour l'occasion connecteurs logiques, pour produire des propositions qui, comme les littéraux , ont une valeur booléenne déterminée par ces dernières dans chaque monde. Une proposition est une composition de connecteurs et de littéraux
Le langage des propositions regroupe toutes les propositions qui sont obtenues par la composition de connecteurs logique et de littéraux. Par exemple : `R(a,f(b))=>R(b,a)`
La relation de satisfaisabilité `"⊨"` qui s'applique aux mondes et aux littéraux, s'étend aux propositions, puis s'étend en fin de course aux ensemble de mondes, c'est à dire aux sous-ensembles de l'univers. Et dans l'ensemble des ensembles de mondes, c'est à dire dans l'ensemble des sous-ensembles de l'univers, elle correspond à la relation d'inclusion, c'est pourquoi on peut la noter aussi par le symbole `"⊆"`. Et le symbole `≡` précédement utilisé désigne l'égalité sémantique.
Cela permet de définir ce qu'est la conséquence sémantique. Etant donné deux propositions `P, Q`, l'expression `P"⊨"Q`, ou `P"⊆"Q` signifie que `Q` est une conséquence sémantique de `P`, c'est à dire que l'ensemble des mondes satisfaisant `P` est inclus dans l'ensemble des mondes satisfaisant `Q`, autrement dit, que si un monde satisfait `P` alors il satisfait `Q`. Par contre la conséquence syntaxique qui sera décrite plus loin, ne met en oeuvre que des règles formelles de raisonnement que l'on se sera choisies, et ne s'applique que sur la syntaxe des propositions.
Pour récapituler, considérons par exemple le langage prédicatif suivant `"<"a,b,f"(.)>", {K, R"(.,.)"}`.
`"<"L">"={a, f(a), f(f(a)), f(x), f(g(x,a)), g(a,b),...}`
On remarque que les opérateurs générateurs d'arité `n` restreints au domaine de Herbrand `"<"L">"` sont des applications injectives distinctes de `"<"L">"^n"→""<"L">"`, et que les opérateurs générateurs d'arité `0` sont des éléments distincts de `"<"L">"`.
`R(x,a), K, R(x,f(x)), Q(a)`
Voici des exemple de littéraux négatifs :
`"¬"R(x,f(x)), "¬"K, "¬"Q(y)`
On remarque que les prédicats d'arité `0` sont des inconnus booléens qui sont distingués par leur noms. On remarque que les prédicats d'arité `n` restreints au domaine de Herbrand `"<"L">"` sont des applications de `"<"L">"^n"→"{0,1} ` qui sont distingués par leur noms, et qui correspondent donc à des ensembles de n-uplet que l'on désigne par la même lettre que le prédicat. Exemple : `Q(y) <=> y∈Q`.
Le langage prédicatif, sans quantificateur et sans le prédicat d'égalité, se ramène à un langage rudimentaire qu'est le langage propositionnel classique. C'est le langage des équations booléennes. Les prédications sont autant d'inconnues booléennes que l'on renomme en `X_1,X_2,X_3,...`. Une proposition est par définition de taille finie, et donc constitue une équation booléenne.
Les règles de déduction du calcul propositionnel classique peuvent se décrire de différentes façons. Présentons d'abord 5 méthodes pour déterminer si une proposition est une tautologie, une antilogie, ou est indécidable :
Ces règles nous rappellent que le raisonnement n'est qu'un calcul. Déduire, c'est calculer.
Cette méthode consiste à procèder à tous les testes possibles en attribuant aux inconnues `X_1,X_2,X_3,...` les valeurs booléennes dans l'ordre que l'on choisie habituellement selon le big-endian. S'il y a au moins un résultat à `0` et un résultat à `1` alors la proposition est indécidable. Si les résultats sont toujours à `0` alors la proposition est une antilogie. Si les résultats sont toujours à `1` alors la proposition est une tautologie. Cette méthode comprend une variante dite "méthode Shadock" qui consiste à procèder à un trés grand nombre de testes en attribuant aux inconnues `X_1,X_2,X_3,...` des valeurs booléennes au hasard. Si il y a au moins un résultat à `0` et un résultat à `1` alors la proposition est indécidable de façon certaine. Si les résultats sont toujours à `0` alors la proposition est une antilogie selon un indice de confiance. Si les résultats sont toujours à `1` alors la proposition est une tautologie selon un indice de confiance. L'indice de confiance pertinent est le rapport entre le nombre d'essais effectués et le nombre d'essais distincts possibles.
Ce système axiomatique utilise les seuls connecteurs logiques `¬, "⇒"` qui sont suffisant pour engendrer tous les connecteurs logiques, et des variables booléennes `A,B,C,...`. On accumule dans un arrangement toutes les propositions que l'on démontre. Les règles de déduction prennent des propositions présentes dans l'arrangement et opère un calcul pour produire le cas échéant une nouvelle proposition que l'on rajoute dans l'arrangement. Et il y a 4 règles :
`(A, A"⇒"B)⊢ B`
`⊢ A "⇒" (B "⇒" A)`
`⊢ (A "⇒" (B "⇒" C)) "⇒" ((A "⇒" B) "⇒" (A "⇒" C))`
`⊢ ("¬"A "⇒" "¬"B) "⇒" (B "⇒" A)`
La première règle s'appelle le modus ponens. Elle prend en entré deux propositions présentes dans l'arrangement, et si l'unification avec l'entête réussi, elle retourne une nouvelle proposition que l'on rajoute dans l'arrangement. Les 3 autres règles ont une liste vide comme entête et engendrent des tautologies où `A,B,C` parcourent toutes les propositions écrivables, présentes ou non dans l'arrangement. La clôture de cet ensemble par la règle du modus ponens, produit exactement l'ensemble de toutes les propositions tautologiques. Pour détecter les propositions indécidables il faut un autre algorithme.
Ce système utilise les seuls connecteurs logiques `{¬, "et", "ou" }` et des variables booléennes `A,B,C,...`. L'étude de la logique propositionnelle, nous montre que toute proposition, se ramène à une conjonction de clauses. En effet, prenez par exemples la proposition `(X"⇒"Y)"⇒"Z` où `X, Y, Z` sont trois valeurs booléennes, cette proposition est équivalente à `(X "ou" Z) "et" ("¬"Y "ou" Z)`. Les règles de déduction du calcul propositionnel se décrivent simplement si on décompose ainsi les propositions en clauses. Une clause est un couple d'ensembles finis de variables booléennes, le premier ensemble regroupe les variables booléennes affirmatives dans la clause, et le second ensemble regroupe les variables booléennes négatives dans la clause. Par exemple :
`({a,b,c},{d,e}) = a" ou "b" ou "c" ou ¬"d" ou ¬"e`
Puis on applique 5 règles :
Le moteur s'arrête si l'arrangement contient la clause vide ou si l'arrangement devient vide. Pour détecter les propositions indécidables il faut un autre algorithme.
On transcrit la proposition dans le langage logique suivant `{0,1,"⇎","et"}` ou bien suivant `{0,1,"⇔","ou"}`, qui correspond à des structures de corps de caractéristique 2 que l'on renomme en `{0,1,"+","∗"}`. La proposition se transcrit en un unique polynome développé en enlevant les puissances `x^2"="x` et en enlevant les mônomes doubles `x"+"x"="0`, puisque nous somme dans un corps de caractèristique 2. La proposition est une tautologie si elle est égale au polynome `1`, elle est une antilogie si elle est égale au polynome `0`, et elle est indécidable si elle est égale à un polynôme autre que `0` ou `1`.
Les règles de déduction sont codifiées à l'aide du symbole de production `"⊢"` . Elles possèdent une entête qui est une liste de propositions, et un corps qui est une proposition. Par exemple, considérons la rège suivante où `A,B,C` sont des variables booléennes libres :
`(A"⇒"B, A" et "C) |-- B" et "C`
Cette règle s'applique par exemple au couple de propositions suivantes `(X"⇒"Y, X" et "¬Y)` en procédant une unification avec son entête, les variables libres étant `A`, `B` et `C`. Si l'unification réussie ce qui est le cas ici, les variables libres sont affectées `A"="X,B"="Y,C"=¬"Y`, la règle produit alors son corps dans lequel les variables libres affectées sont remplacées par ce qu'elles contiennent, et les eventuelles variables libres non affectées peuvent prendre comme valeurs toutes les propositions.
Ce système axiomatique utilise les seuls connecteurs logiques `{¬, "⇒", "et", "ou" }` et des variables booléennes `A,B,C,...`. Les règles de déductions sont :
Règle d'introduction du `"et"` `(A, B)⊢ A "et" B` Règles d'élimination du `"et"` `(A "et" B) ⊢ A`
`(A "et" B)⊢ B`Règles d'introduction du `"ou"` `A⊢(A "ou" B)`
`B⊢(A "ou" B)`Règles d'élimination du `"ou"` `(A "ou" B,A"⇒"C,B"⇒"C)⊢C` Règle d'introduction du `"⇒"` `(A⊢B)⊢(A"⇒"B)` Règle d'élimination du `"⇒"` `(A, A"⇒"B)⊢B` Règle d'introduction du `"¬"` `(A⊢ ⊥)⊢ "¬"A` Règle d'élimination du `"¬"` `(A, "¬"A)⊢ ⊥` Règle "Ex falso" `⊥ ⊢ A` Règle "Ab absurdo" `("¬"A"⇒"⊥)⊢ A`
Mais il y a une subtilité apportée par les règles de déduction possédant dans leur entête le symbole de déduction `"⊢"` que sont l'introduction de l'implication `(A⊢B)⊢(A"⇒"B)`et l'introduction de la négation `(A⊢ ⊥)⊢ "¬"A`. Elles ne peuvent pas fonctionner comme pour l'axiomatique de Hilbert à partir d'un unique arrangement fourre-tout répertoriant toutes les propositions déduites en cours de route (voir Moteur de déduction naturel ).
Pour définir les fonctions propositionnelles, on utilise des variables qui sont des extensions internes du langage. On ajoute des noms de variable, et ces variables sont supposées désigner des éléments de la structure libre initiale, c'est à dire des termes du domaine de Herbrand initial. L'extension est dite interne car elle n'étend pas la structure, elle n'ajoute pas de nouveaux éléments à la structure. Parcontre elle augmente le langage des propositions. Une proposition comprenant `n` telles variables, et dont on choisie un ordre des noms de variables, constitue une fonction propositionnelle d'arité `n`.
Par exemple, considérons le langage d'opérateurs de présentation suivante `L = {a, b, f"(.)"}`, que l'on complète en un langage prédicatif en le munissant des prédicats suivants : `{Q"(.)", R"(.,.)"}`.
Une structure se définie rigoureusement par 3 théories :
On procède à une extension élémentaire en ajoutant au langage de nouveaux éléments générateurs `x, y`. Puis on complète la théorie d'engendrement par les propositions suivantes :
`x in "<"a, b, f"(.)>"`
`y in "<"a, b, f"(.)>"`
De cette façon, l'extension est dite interne. Les éléments `x` et `y` perdent leur statut d'éléments générateurs pour devenir des variables muettes évoluant dans le domaine de Herbrand initial `"<"a, b, f"(.)>"`. ce sont des variables internes c'est à dire dont on suppose qu'elles désignent des éléments exprimables par le langage initial, autrement dit, des termes du domaine de Herbrand initial. Après cela, on peut construire des fonctions propositionnelles telles que par exemple :
`varphi(x,y) = R(x,y)"⇒"R(f(y),x) `
`varphi = (x,y) |-> R(x,y)"⇒"R(f(y),x) `
Notez la priorité syntaxique des opérateurs et connecteurs de la plus faible à la plus élevée `=, |->, ⇒` ainsi choisie pour réduire le nombre de parenthèses.
Notez l'usage du méta-connecteur `vecx|->` qui précise un ordre des variables.
`varphi"(.,.)"` est une fonction propositionnelle binaire. Son entête `(x,y) |->` sert à ordonner les noms des variables. Elle fait partie du langage des propositions augmenté du méta-connecteur `vecx|-> qui précise l'ordre des variables muettes. mais elle ne constitue pas un prédicat, car elle ne fait pas nécessairement partie de la présentation du langage prédicatif.
Elle constitue une relation (en tant que prédicat binaire) définissable selon le niveau 3 (composition générale) dans le langage en question. Leur définition s'écrivent dans ce langage en question augmenté du méta-connecteur `vecx|->` qui précise l'ordre des variables muettes.
Le prédicat d'égalité `="(.,.)"` joue un rôle spécial. Etant donné deux termes distincts du langage, c'est à dire deux éléments distincts de la structure libre, par exemple `f(f(a)), a`, la prédication `f(f(a))"="a` va modifier la construction de la structure en liant ces deux éléments par un lien transitif, symétrique et réflexif qu'est l'égalité. Ce lien d'égalité est une relation d'équivalence. La structure s'obtient en quotientant la structure libre par la relation d'équivalence. Les éléments de la structure sont les classes d'équivalence de la structure libre. Les relations d'équivalences s'ajoutent pour former une relation d'équivalence aux classes d'équivalence plus vastes, c'est pourquoi le même raisonnement s'applique pour une conjonction d'égalités qui établit une relation d'équivalence aux classes d'équivalence plus vastes. Mais cela ne s'applique pas pour une disjonction d'égalités car celle-ci ne permet pas d'établir une relation d'équivalence. Par exemple :
`("<"a,b,f"(.)>")/{f(f(a))"="a "et" f(b)"="a} = {a,b,f(a)}`
Le prédicat d'égalité `"=(.,.)"` appliqué à un couple d'éléments désignable par le langage `(x,y)` produit la prédication `x"="y` qui a pour signification que les deux éléments `x` et `y` sont égaux. Ce prédicat constitue une relation d'équivalence sur l'ensemble des termes c'est à dire des éléments de la structure libre. Autrement dit, la relation est reflexive, symétrique et transitive. Les termes ne désignent plus de façon injective les éléments. Ce sont les classes d'équivalence qui désignent de façon injective les éléments. Ce prédicat d'égalité entraine des contraintes sur lui-même, à savoir que c'est une relation d'équivalence (reflexive, symétrique et transitive) :
`AAx, x"="x`
`AAxAAy, (x"="y)=>(y"="x)`
`AAxAAyAAz, (x"="y)" et "(y"="z)=>(x"="z)`
Notez la priorité syntaxique des connecteurs et déclarateurs de la plus faible à la plus élevée `AAx , AAy , AAz , =, <=>, =>, "et" `.
La notation `AAx` signifie quelque soit un élément `x` désignable par le langage, c'est à dire quelque soit un terme du domaine de Herbrand, ou autrement dit quelque soit un élément `x` de la structure libre.
Le prédicat d'égalité entraine des contraintes d'égalité sur les opérateurs du langage, à savoir que les opérateurs unaires appliqués à `x` doivent produire le même éléments que les opérateurs unaire appliqué à `y` si `x"="y`. Et que les opérateurs binaire appliqués à `(x_1,x_2)` doivent produire le même élément que les opérateurs binaires appliqués à `(y_1,y_2)` si `(x_1,x_2)"="(y_1,y_2)`. Et de même pour les `n`-uplet s'il y a des opérateurs d'arité `n` :
`AAf"(.)"AAxAAy, (x"="y) => (f(x)"="f(y))`
`AAf"(.,.)"AAx_1AAy_1AAx_2AAy_2, (x_1"="y_1)" et "(x_2"="y_2) => (f(x_1,x_2)"="f(y_1,y_2))`
`AAf"(...)"AAvecxAAvecy, (vecx"="vecy) => (f(vec x)"="f(vecy))`
La notation `AAf"(.)"` signifie quelque soit `f` un opérateur unaire du langage, c'est à dire appartenant à la présentation du langage. La notation `AAf"(.,.)"` signifie quelque soit `f` un opérateur binaire du langage, c'est à dire appartenant à la présentation du langage. La notation `f"(...)"` désigne un opérateur d'arité `n`, et la notation vectorielle `vecx, vecy,...` désigne des n-uplets d'éléments de la structure libre. La notation `AAf"(..,)"` signifie quelque soit `f` un opérteur n-aire du langage, c'est à dire appartenant à la présentation du langage.
Le prédicat d'égalité entraine des contraintes sur les autres prédicats du langage, à savoir que les prédications relatives à `x` doivent être identiques aux prédications relatives à `y` si `x"="y`. Et que les prédications relatives à `(x_1,x_2)` doivent être identiques aux prédications relatives à `(y_1,y_2)` si `(x_1,x_2)"="(y_1,y_2)`. Et de même pour les `n`-uplet s'il y a des prédicats d'arité `n` :
`AAP"(.)"AAxAAy, (x"="y) => (P(x)"⇔"P(y))`
`AAP"(.,.)"AAx_1AAy_1AAx_2AAy_2, (x_1"="y_1)" et "(x_2"="y_2) => (P(x_1,x_2)"⇔"P(y_1,y_2))`
`AAP"(...)"AAvecxAAvecy, (vecx"="vecy) => (P(vec x)"⇔"P(vecy))`
La notation `AAP"(.)"` signifie quelque soit `P` un prédicat unaire du langage, c'est à dire appartenant à la présentation du langage. La notation `AAP"(.,.)"` signifie quelque soit `P` un prédicat binaire du langage, c'est à dire appartenant à la présentation du langage. La notation `P"(...)"` désigne un prédicat d'arité `n`. La notation `AAP"(...)"` signifie quelque soit `P` un prédicat n-aire du langage, c'est à dire appartenant à la présentation du langage.
L'ensemble de ces contraintes est équivalente à l'unique contrainte générale suivante s'appliquant à toutes les fonctions propositionnelles `varphi` :
`AA varphi"(...)"AAxAAyAAvecu, (x"="y) => (varphi(x,vecu)"⇔"varphi(y,vecu))`
La notation `varphi"(...)"` désigne une fonction propositionnelle d'arité `n` du langage. C'est donc beaucoup plus vaste qu'un simple prédicat appartenant à la présentation du langage, mais cela doit être une proposition exprimable dans le langage augmenté de `n` variables internes.
Et on peut supposer qu'il n'y a pas d'autre contrainte.
Notez que ces formulations ne font pas encore partie de notre langage formel puisque le symbole `AA` n'y est pas encore défini, et que les vaiables autres qu'élémentaires n'y sont pas non plus définies. Ces formulation font partie d'un méta langage plus riche.
Le prédicat d'égalité `="(.,.)"` joue un rôle tout à fait spécial, et va complexifier la logique de manière importante. Condidérons l'ajout d'une égalité entre deux éléments tel que par exemple :
`f(a,f(a)) = g(a,a)`
On la décrit en décrivant l'univers résultant. L'égalité entre deux termes, entre deux éléments, signifie concrètement que dans l'univers les cases mémoires d'adresse `a_1` et `a_2` sont égales si les adresses sont égales en prenant compte les égalités.
Les termes du langage désignent des éléments d'une façon qui n'est plus forcement injective, c'est à dire que deux termes distincts peuvent désigner le même éléments. Les termes égaux entre eux forment des classes d'équivalence, et ce sont ces classes d'équivalences qui désignent de façon injective les éléments de la structure associée.
On est donc amené à considèrer un type de proposition particulière qui est une conjonction d'égalités de termes. Cette proposition `T` engendre à l'aide des deux premières règles du chapitre précédent, une relation d'équivalence sur la structure libre `"<"L">"` . Et la structure quotient qui se note `"<"L">/"T` regroupe l'ensemble des classes d'équivalences, et constitue la structure associée.
---- 16 février 2019 ----
Ces règles de déduction s'obtiennent à partir des règles vues au chapitre §5 et des contraintes de l'égalité vues au chapitre §6.
Le langage prédicatif sans quantificateur mais avec prédicat d'égalité, peut exprimer des propositions extrêmement difficiles à résoudre c'est à dire à determiner si elles sont tautologiques, indécidables ou antilogiques.
À ce stade, il convient de trouver un algorithme efficace pour résoudre ce genre de problème.
Une première simplification s'opère. L'étude de la logique propositionnelle, nous montre que toute proposition, se ramène à une disjonction de conjonctions de littéraux. En effet, prenez par exemples la proposition `(X"⇒"Y)"⇒"Z` où `X, Y, Z` sont trois valeurs booléennes, cette proposition est équivalente à `(X "et" "¬"Y) "ou" (X "et" Z) "ou" (Z "et" "¬"Y)`.
Chaque conjonction est alors traitée séparément. Si chacune sont antilogiques alors la disjonction est antilogique, s'il existe une conjonction tautologique alors la disjonction est tautologique, et sinon la disjonction est indécidable.
On a ainsi ramené le problème à celui d'une conjonction d'égalités et d'inégalités dans un langage d'opérateurs.
Si il n'y a que des opérateurs d'arité `0` et `1`, alors la résolution se fait en construisant la forêt des monoïdes engendrés par ces opérateurs.
Si on ajoute au langage un opérateur binaire `g"(.,.)"`, le problème se complexifie considérablement.
...
Le langage logique est dit du premier ordre car il n'utilise qu'un seul type de variable, et ces variables peuvent être quantifiées existentiellement ou universellement.
On définie le langage des propositions avec quantificateurs de façon réccurcive. Le langage utilisé est contextuelisé, c'est à dire qu'il n'est pas le même dans toute la proposition, il est complété dans chaque sous-proposition par la déclaration de variable faite par le quantificateurs racines de la sous-proposition et qui n'a de portée syntaxique que dans la sous-proposition.
Considérons un langage d'opérateurs de présentation `L`.
Le quantificateur universel ou existentiel, prenons par exemple `AA`, prend deux arguments :
`AAx, P`
Le premier argument `x` est une nouvelle variable élémentaire, le second argument `P` correspond à une sous-proposition qui est une proposition quelconque avec quantificateur, écrite dans le langage `L+{x}`. C'est parcequ'on ne veut pas que les variables locales masquent les variables globales que l'on ne considère que des unions disjointes. La définition étant réccurcive, il peut être nécessaire de préciser qu'une sous-proposition ne peut pas être la proposition globale ou une autre sous-proposition, ou autrement dit, on s'interdit le partage de données dans la syntaxe.
Etant donné le langage prédicatif `L`. On définie ce qu'est une proposition unaire `P"(.)"` dans le langage `L` (ou dit classiquement une fonction propositionnelle à un argument). C'est une proposition écrite dans le langage augmenté `L+{lambda_1}` où `lambda_1` joue le rôle de l'argument anonyme. Cela permet d'anonymiser les arguments. On parlera ainsi d'une proposition unaire `P"(.)"` définie dans `L`, qui admet donc une instantiation `P(x)` définie dans `L+{x}`, et une instanciation `P(y)` définie dans `L+{y}`, et etc..
On remarque alors que la proposition `P(y)` est identique à la proposition `P(x)` dans laquelle on a remplacé chaque occurence de `x` par `y`.
Qu'est-ce que signifit la proposition `AAx, P(x)` ? Il convient de choisir une signification, une sémantique, c'est à dire un type de monde appelé aussi modèle qui pourra satisfaire ou non la proposition.
`"<"L">"` représente l'ensemble des éléments `L`-constructibles où `L` est le langage logique. Mais les quantificateurs ne se restreignent pas aux seuls éléments `L`-constructibles, ils incluent les autres éléments potentiels. De ce constat, il découle intuitivement que :
Le connecteur `"et"` itéré est représenté par le symbole `^^` similaire au symbole d'intersection d'ensembles. Le connecteur `"ou"` itéré est représenté par le symbole `vv` similaire au symbole de l'union d'ensembles.
Mais cette idée intuitive ne suffit pas pour définir complètement la sémantique.
On réitère le premier choix classique qui impose le tiers exclus, et donc qui définie la négation. Ce premier choix constitue un axiome de déduction, ou plus exactement un shéma d'axiomes de déduction : La négation d'une proposition quantifiée s'obtient simplement en inversant le quantificateur et en négativant le corps.
Et c'est un shéma d'axiomes car cela s'applique pour toute proposition unaire `P"(.)"` écrite dans le langage `L`
...
...
...
...
Pour lever toute ambiguité, il convient de poser de façon formelle une théorie des ensembles telle que celle de Zermelo :
| Shéma d'axiome de compréhension Quelque soit une proposition unaire `P"(.)"` et un ensemble `x`, il existe un ensemble `y` qui contient exactement les éléments appartenant à `x` et satisfaisant `P"(.)"`. |
`AAx EEy AAe, e"∈"y <=> e"∈"x" et "P(e)` |
| Axiome d'extensionnalité Quelque soit deux ensembles `x` et `y`. S'ils possèdent les mêmes éléments alors ils sont égaux. |
`AAxAAy,(AAz, z "∈"x <=> z"∈"y) => x"="y` |
Axiome de l'ensemble vide L'ensemble vide `Ø` ne contient aucun élément. |
`AAx, x"∉"Ø` |
| Axiome de la paire Quelque soit deux éléments `a` et `b`, il existe un ensemble `c` qui ne contient que `a` et `b`. |
`AAaAAbEEcAAx, x"∈"c <=> x"="a" ou "x"="b` |
| Axiome de la réunion Quelque soit `a` un ensemble d'ensembles, il existe un ensemble `b` contenant les éléments qui appartiennent à au moins un ensemble appartenant à `a`. |
`AAaEEbAAc, c"∈"b <=>( EE d, d"∈"a" et "c"∈"d)` |
| Axiome de l'ensemble des parties Quelque soit un ensemble `x`, il existe un ensemble `y` contenant tous les sous-ensemble de `x`. |
`AAxEEyAAz, z"∈"y<=>(AAt, t"∈"z => t "∈"x)` |
| Axiome de l'infini Il existe un ensemble `x` qui contient l'ensemble vide Ø et qui, quelque soit un élément `y`, s'il contient cet élément `y` alors il contient l'ensemble singleton `{y}`. |
`EEx, Ø"∈"x" et "(AAyAAz,(AAt, t"∈"z <=> t"="y)" et "y"∈"x => z"∈"x)` |
---- 19 août 2018 ----