On part du plus petit langage d'opérateurs possible engendrant un domaine de Herbrand infini. C'est le langage composé d'un élément et d'une fonction unaire `L ={a, s"(.)"}` et qui représente d'une certaine façon les entiers naturels. Le domaine de Herbrand est l'ensemble des compositions closes du langage. La clôture par composition close se note avec le symbole `•` en exposant.
`L^• = {a,s(a),s(s(a)),s(s(s(a))),...}`
Puis on posera petit à petit les règles de déduction sous forme d'axiomes lorsque leurs nécessitées s'imposeront naturellement comme des évidences intuitive dans le choix d'une construction d'un modèle.
On définie le langage logique par des règles de construction telle une grammaire, et on commence par choisir les opérateurs qui nous sont indispensables. Un terme est une composition close du langage d'opérateurs `{a, s"(.)"}`. Ce langage peut être augmenté de nouveaux éléments telles que par exemple `x, y` ou de nouveaux opérateurs tel que par exemple `f"(.)"` pour former le langage d'opérateurs `{a, x, y, s"(.)", f"(.)"}`. Voici des exemples de termes :
`a, s(a), s(s(a)), s(x), s(f(x)), f(f(a))...`
Et il n'y a pas de différence entre une constante et une variable. Une constante sur laquelle nous n'avons aucune information est une variable libre. On parlera donc indistinctement d'élément ou de variable élémentaire, d'opérateur ou de variable fonctionnelle.
Néamoins comme nous nous restreingnons à un langage d'opérateurs d'arité fixe divers, chaque opérateur possède une arité fixe qui constitue sont type. Le langage logique que nous construisons a pour objectif de décrire des structures composée d'éléments. Soit `Omega` l'ensemble des éléments de la structures. Un opérateur d'arité `n` sera donc une application de `Omega^n"→"Omega`
Puis on choisit les prédicats qui nous sont indispenssables, et le seul qui nous soit vraiement indispenssable à ce stade, est l'égalité `=`. A ce stade, un littéral affirmatif est une égalité entre deux termes du langage d'opérateurs `{a, x, y, s"(.)", f"(.)"}^•`.
Les prédicats anonymes d'arité fixe quelconque n'apportent pas de puissance expressive supplémentaire au langage et sont définis à l'aide du prédicat `=` comme suit : Le langage comprend nécessairement un premier élément générateur, car sinon la structure est vide, et c'est ce premier élément générateur qui est choisie pour désigner la valeur logique true. On définie le prédicat comme étant un opérateur de même arité, mais dont le résultat est bridé comme suit : Si le résultat est cet élément générateur alors le bridage fait qu'il retourne true, et si le résultat diffère de cet élément alors le bridage fait qu'il retourne false. On définie de façon plus subtile ce qu'est un semi-prédicat, comme suit : C'est un opérateur d'arité `n` qui procède à un calcul, et soit celui-ci s'arrète et quelque soit ce qu'il retourne, le bridage fait qu'il retourne true, ou soit celui-ci ne s'arrète pas et ne donne jamais de réponse ce qui se note par `oo`, l'infini de Turing.
Néanmoins, pour la facilité du maniement logique, on crée un langage de prédicats, composé de prédicats d'arité fixe diverse `n` qui sont des applications de `Omega^n"→"{`true`, `false`}`
Le langage de prédicats est augmenté de variables prédicatives notées en majuscule telles que par exemple `X, P"(.)", Q"(.,.)"` pour former le langage de prédicats `{"=(.,.)", X, P"(.)", Q"(.,.)"}`. Le prédicat `X` d'arité nulle est simplement une valeur booléenne inconnue.
On rappel qu'il n'y a pas de distinction entre constante et variable, et qu'un élément est synomyme de variable élémentaire, qu'un opérateur est synonyme de variable fonctionnelle, et qu'un prédicat est synonyme de variable prédicative.
A ce stade, un littéral affirmatif est une composition d'un prédicat parmi le langage de prédicats `{"=(.,.)", X, P"(.)", Q"(.,.)"}` clos avec des termes du langage d'opérateurs `{a, x, y, s"(.)", f"(.)"}`. Voici des exemples de littéraux affirmatifs :
`a"="s(a), a"="s(x), x"="s(f(a)), P(x), Q(s(x),f(x)), ...`
Un littéral peut en plus être négativé par le connecteur logique `¬` tel que par exemples `x"≠"y, "¬"P(x)`
Une clause est une disjonction de littéraux.
Une proposition logique est une combinaison de littéraux à l'aide de connecteurs logiques.
L'étude de la logique propositionnelle, ou dite d'ordre zéro, nous montre que toute proposition logique de variables booléens, 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)`.
On entend par logique propositionnelle, un fragment de la logique qui ne s'interesse qu'aux connecteurs logique `⊤,⊥,∧,∨,⇒, ⇔` et sur ce quoi ils s'appliquent c'est à dire sur des variables booléennes.
Les propositions logiques sont des équations booléennes. Et leur table de vérité révèle leur mystère. Elle révèle les diverses possibilités logiques satisfaisant l'équation, sa validité si elles satisfont toutes l'équation, sa satisfaisabilité s'il existe au moins une possibilité satisfaisant l'équation, ou son incohérence s'il n'y en a aucune pour satisfaire l'équation.
Néanmoins cela ne répond pas à notre demande, de savoir qu'elles sont exactement les règles du raisonnements en logique d'ordre zéro.
Parcontre grace à la table de vérité, nous avons un moyen de vérifier si un système de règles donné, définit bien le raisonnement logique d'ordre zéro, c'est à dire si le système de règles génère bien toutes les formules valides possibles, et uniquement les formules valides.
Une réponse est donnée par le système axiomatique de Hilbert, qui porte le nom du célèbre mathématicien allemand David Hilbert (Königsberga, 1862 - Göttingen 1943). Ce système axiomatique utilise le langage logique `{¬, "⇒"}`, qui est suffisant pour engendrer tous les connecteurs logiques, et auquel on adjoint des variables booléennes `x,y,z,...` en nombre infini.
On accumule dans un sac toutes les formules que l'on démontre. Une règle de déduction prend comme argument des formules dans le sac, et produit une nouvelle formule que l'on rajoute dans le sac. Les règles de déduction sont des méta-formules utilisant les connecteurs logiques du langage `{¬, "⇒"}` et des variables pouvant représenter toutes formules appartenant à `{¬, "⇒", x, y, z,...}^•`
`{A, A"⇒"B} ⊢ B`
`⊢ A "⇒" (B "⇒" A)`
`⊢ (A "⇒" (B "⇒" C)) "⇒" ((A "⇒" B) "⇒" (A "⇒" C))`
`⊢ ("¬"A "⇒" "¬"B) "⇒" (B "⇒" A)`
Le premier axiomes s'appel le modus ponens. Les variables `A, B` peuvent désigner n'importe quelle formule. Mais le modus ponens ne s'applique que si `A` et `A=>B` sont bien présents tous les deux dans le sac, c'est à dire s'ils ont déjà été démontrées.
Les 3 autres axiomes s'appliquent pour n'importe quelles trois formules `A,B,C`. Ils engendrent donc un ensemble de totologies suivant :
`{A "⇒" (B "⇒" A), (A "⇒" (B "⇒" C)) "⇒" ((A "⇒" B) "⇒" (A "⇒" C)), ("¬"A "⇒" "¬"B) "⇒" (B "⇒" A)" / " (A,B,C)in({¬, "⇒",x,y,z,...}^•)^3}`
Et la clôture de cet ensemble par la règle du modus ponens, produit exactement l'ensemble de toutes les formules valides d'ordre zéro.
Le système de déduction est cohérent. Cela signifie qu'il ne démontre pas le faux : `"⊬⊥"`. Le système de déduction est complet. Cela signifie qu'il démontre toutes les formules valides. Une formule valide (appelée aussi tautologie sémantique) est ici une formule `varphi` qui est toujours vrai quelques soient les valeurs booléennes de ses variables, ce qui se note par `"⊨"varphi`. Le système de déduction est complet si pour toutes formules `varphi`, nous avons : `"⊨"varphi` implique `"⊢"varphi`. Le système de déduction est cohérent et complet si pour toutes formules `varphi`, nous avons : `"⊨"varphi` si et seulement si `"⊢"varphi`.
La demonstration est assez laborieuse. Mais pour ce système de Hilbert assez simple à décrire, elle est rigoureuse et exacte, et constitue sans doute la plus célèbre des démonstrations parmi celles des autres systèmes de déduction. C'est pourquoi il parrait naturelle de vouloir déduire les autres systèmes de déduction à partir de celui-ci.
---- 14 avril 2018 ----
Ce système se présente pareillement que le précédent. On accumule dans un sac toutes les formules que l'on démontre. Une règle de déduction prend comme argument des formules dans le sac, et produit une nouvelle formule que l'on rajoute dans le sac.
Dans le langage logique `{¬, "⇒", "et", "ou" }`, dire que `A` démontre `B` ce qui se note `A⊢B` signifie exactement que `A"⇒"B` où autrement dit que l'on peut démontre que `A` implique `B` ce qui se note `⊢(A"⇒"B)`.
⊢A"⇒"A
{A, A"⇒"B} ⊢ B
⊢(A et (A"⇒"B))"⇒"B
⊢((A"⇒"B) et A)"⇒"B
{A"⇒"B, C"⇒"D} ⊢ (A et C)"⇒"B
{A"⇒"B, C"⇒"D} ⊢ (A et C)"⇒"D
⊢ (A"⇒"B et C"⇒"D)⇒((A et C)"⇒"B)
⊢ (A"⇒"B et C"⇒"D)⇒((A et C)"⇒"D)
A"⇒"(B et C) ⊢ A"⇒"B
A"⇒"(B et C) ⊢ A"⇒"C
⊢ (A"⇒"(B et C))"⇒"(A"⇒"B)
⊢ (A"⇒"(B et C))"⇒"(A"⇒"C)
`{A, B} ⊢ A "et" B`
`{A, B} ⊢ A "et" B`
`A "et" B ⊢ A`
`A "et" B ⊢ B`
`A⊢A "ou" B`
`B⊢A "ou" B`
`{A "ou" B,A"⇒"C,B"⇒"C}⊢C`
`{A, A"⇒"B}⊢B`
`(A⊢B)⊢(A"⇒"B)`
`{A, "¬"A} ⊢ ⊥`
`(A⊢ ⊥)⊢ "¬"A`
`⊥⊢ A`
`"¬"A"⇒"⊥ ⊢ A`
Dans le langage logique `{¬, "⇒", "et", "ou" }`
`⊢(A⊢A)`
`(E⊢A), (F⊢B) ⊢ E,F⊢ A"et"B`
`(E⊢A"et"B) ⊢ E⊢A,B`
`(E,F⊢A) ⊢ E ⊢ F"⇒"A`
`(E⊢A"⇒"B),(F⊢A)⊢E,F⊢B`
`E,F"⇒⊥" ⊢E⊢"¬"F`
`(E⊢"¬"A),(F⊢A) ⊢E,F⊢"⊥"`
`(E⊢A)⊢E⊢A"ou"B`
`(E⊢B)⊢E⊢A"ou"B`
`(E⊢A"ou"B),(F,A⊢C),(G,B⊢C) ⊢ E,F,G⊢C`
`(E⊢A)⊢(E,B)⊢A`
`E,A,A⊢B ⊢E,A⊢B`
`(E,"¬"A⊢"⊥")⊢E⊢A`
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.
Une proposition simple est une expression logique.
Une proposition unidimensionnelle quantifie une variable. Elle possède une tête et un corps séparé par une virgule. La tête quantifie la variable à l'aide d'un opérateur `AA` ou `EE` et le corps est une expression logique dans le langage augmenté de cette variable. Voici un exemple de proposition avec une variable élémentaire :
`EE x, x!=a`
La variable quantifiée peut être fonctionnelle. Voici un exemple de proposition avec une variable fonctionnelle unaire :
`EE f"(.)", f(a) != a`
Par symétrie, on conçoit qu'il est posssible de quantifier des variables prédicatives. Voici un exemple d'une proposition avec une variable prédicative unaire :
`EE P"(.)", P(a)`
Le corps d'une telle proposition peut également être constitué par une autre proposition unidimensionnelle, auquel cas le résultat est une proposition bidimensionnelle. Et cela peut se répéter, formant ainsi des propositions de dimension `n`, c'est à dire utilisant `n` variables qui sont soient élémentaires, fonctionelles ou prédicatives. Voici un exemple de proposition de dimension 3 utilisant une variable prédicative unaire et deux variables élémentaires, et qui correspond à un axiome de l'égalité :
`AA P"(.)", AA x, AAy, (x=y) => (P(x)<=>P(y))`
Nous avons ainsi définie un langage logique d'une grande puissance expressive.
Sémantiquement, et selon l'approche intuitionniste, une variable élémentaire interne représente un élément calculable du modèle, un terme de l'espace de Herbrand, ou autrement dit un élément de la structure libre `"<"a,s"(.)>"`. De même une variable fonctionnelle représente une fonction calculable du modèle, et une variable prédicative représente une fonction logique calculable dans le modèle.
Selon le principe élémentarien, les éléments du modèle sont énumérables comme tout ce qui est calculable. Les fonctions et prédicats calculable sont énumérables.
Et il n'y a pas de différence essentielle entre une fonction et un prédicat, juste une question accessoire sur la forme du résultat. C'est pourquoi on n'adopte pas d'écriture spécifique pour différentier une variable fonctionnelle d'une variable prédicative, sachant que l'usage qui en est fait après, tranche nécessairement la question.
Le modèle dans lequel les propositions sont réalisées ou non est l'espace de Herbrand munie des fonctions et prédicats calculable.
Considérons une variable élémentaire `x` et un prédicat unaire `P"(.)"`. Considérons la proposition `AA x, P(x)`. Le quantificateur `AA` appliqué à la variable `x` correspond à un `"et"` intégré sur l'ensemble des valeurs calculables de `x`. L'opérateur `"et"` est représenté par le symbole `^^` (tel que l'intersection) . L'ensemble des éléments de l'espace de Herbrand est représenté par `Omega`. Nous avons :
`AA x, P(x) <=> ^^^_(x in Omega) P(x)`
L'ensemble des valeurs possible de `x`, noté `Omega`, est par principe énumérable. Cela entraine que la proposition `AA x, P(x)` est réfutable en un temps fini dans le cas où celle-ci serait fausse. Et il s'agit là d'une périssologie car on définie justement la valeur logique fausse de cette proposition par le fait qu'elle doit être réfutée en un temps fini. Parcontre elle n'est pas assurement affirmable en un temps fini dans le cas où elle ne serait pas fausse. C'est pourquoi l'affirmation d'une telle proposition est parfois appellée un oracle.
En tant qu'idée mathématique sans contrainte matériel d'aucune sorte, on peut se placer à l'infini et ainsi connaître l'oracle. Mais il faut en quelque sorte, être immortel dans un monde immortel et de surcroit régit par la mécanique classique, somme-toute, des présupposés assurement faux, mais qui à notre échelle sont approximativement vrai..
Si on adopte ce principe qui correspond au présuposé des mathématiques, à savoir que le monde dans le quel est développé cette mathématique perdure éternellement et est régis par la mécanique classique, et que nous pouvons nous placer abstraitement à l'infini et ainsi connaitre la valeur logique de la proposition, alors toutes les propositions exprimables dans notre langage ont une valeur logique bien définie.
La négation d'une propostion unidimensionnelle s'obtient alors simplement en inversant le quantificateur de la tête et en négativant le corps.
`¬(AA x, P(x)) <=> (EE x, ¬P(x))`
`¬(EE x, P(x)) <=> (AA x, ¬P(x))`
Le quantificateur `EE` appliqué à la variable `x` correspond à un `"ou"` intégré sur l'ensemble des valeurs calculables de `x`. L'opérateur `"ou"` est représenté par le symbole `vv` (tel que l'union). L'ensemble des éléments de l'espace de Herbrand est représenté par `Omega`. Nous avons :
`EE x, P(x) <=> vvv_(x in Omega) P(x)`
On convient que cette règle de calcul de la négation s'applique quelque soit le type de variable, élémentaire, fonctionnelle ou prédicative d'arité quelconque.
Il est alors nécessaire, pour respecter la sémantique, pour respecter notre vision intuitive des fonctions et des prédicats, d'introduire dans le langage d'opérateurs l'ensemble des moyens nécessaires pour calculer toutes les fonctions et tous les prédicats considérés comme possibles.
Dans les cas dégénérés où nous n'avons pas cette propriété, la signification de la proposition `AA P(.), P(a)` change du sens habituel. Car elle signifie : « Quelque soit la fonction logique `P(.)` que nous pouvons construire avec les moyens qui nous sont données, nous avons la propriété `P(a)` ».
Puis on opère une élémentarisation des fonctions et des prédicats. Deux fonctions `f"(.)", g"(.)"` sont dites égales ssi `AA x, f(x)=g(x)`. Deux prédicats `R"(.)", S"(.)"` sont dits égaux ssi `AAx, R(x)<=>S(x)`. Et de même pour des fonctions et prédicats d'arité supérieur. Il est alors possible de créer pour chaque fonction et pour chaque prédicat modulo l'égalité ainsi définie, un élément qui le désigne. On obtient ainsi une deuxième catégorie d'éléments.
Il est alors possible de définir des variables (élémentaires, fonctionnelles ou prédicative) typées. Le type booléen se note `0`. Le type élément se note `1`. Le type élément de deuxième catégorie se note `2`. Le type `1->0` désigne celui d'un prédicat unaire, le type `(1,1)->1` désigne celui d'une fonction binaire, le type `(2,2)->0` désigne celui d'un prédicats opérant sur deux éléments de deuxième catégorie, le type `(1,2)->1` désigne celui d'une fonction opérant sur un élément de première catégorie et un élément de deuxième catégorie pour produire un élément de première catégorie, etc...
Les fonction et prédicats créés par ce procédé peuvent à leur tour être élémentarisés de la même façon et former les éléments de troisième catégorie, et ainsi de suite.
On cherche à étendre la capacité d'expression du langage, et on veut choisir une voie dans laquelle le langage obtenu permettra d'exprimer de façon simple une opération de raisonnement jugée fondamentale qu'est la récurrence générale.
Puis on opère une fonctionnisation des termes avec varibiable. Un terme avec une variable `x` libre, tel que par exemple `g(g(x,v),x)`, permet de créer une nouvelle fonction `h"(.)"` définie par `h(x) = g(g(x,v),x)` et qui peut alors être ajoutée au langage d'opérateurs. On notera :
`h = x |-> g(g(x,v),x)`
Puis on opère une prédicarisation des propositions avec varibiable. Une proposition avec une variable `x` libre, tel que par exemple `AA v, g(x,v)=g(v,x)`, permet de créer un nouveau prédicat `N"(.)"` définie par `N(x) <=> AA v, g(x,v)=g(v,x)` et qui peut alors être ajouté au langage de prédicats. On notera :
`N = x |-> (AA v, g(x,v)=g(v,x))`
--- 13 septembre 2015 ---
On enrichie le langage logique à l'aide de la notion d'indépendance entre quantificateur `AA` et `EE`, et plus finement encore, entre quantificateur `AA` et opération logique `"ou"`, et symétriquement aussi entre quantificateur `EE` et opération logique `"et"`.
Considérons deux variables élémentaires `x, y` et deux prédicats binaires `A"(.,.)", B"(.,.)"`. Considérons la proposition suivante :
`AAx, AAy, A(x,y) "ou" B(x,y)`
Cela signifie que quelque soit `x` et `y`, il y a toujours une des deux propositions `A(x,y)` ou `B(x,y)` qui est vrai. Maintenant, considérons qu'il existe un prédicat unaire `D"(.)"` tel que nous ayons :
`AAx, AAy, (A(x,y) "et" D(x) ) "ou" ( B(x,y) "et" ¬D(x))`
Le modèle est alors plus simple, puisque l'alternative se fait indépendament de la valeur de `"y"`. On notera ce `"ou"` indépendant de `AAy` avec la notation de Hintikka et Sandu. Les deux propositions suivantes sont équivalentes :
`AAx, AAy, A(x,y) ("ou/"AAy) B(x,y)`
`EE D"(.)", AAx, AAy, (A(x,y) "et" D(x)) "ou" (B(x,y) "et" ¬D(x))`
Le `EEz` se ramenant à une opération logique `"ou"`, la même qualité d'indépendance à l'égard de `AAy` peut se produire. Auquel cas les 4 propositions suivantes sont équivalentes :
`AAx, AAy, (EEz"/"AAy) W(x,y,z)`
`AAx, AAy, W(x,y,z_1) ("ou/"AAy) W(x,y,z_2) ("ou/"AAy) W(x,y,z_3) ("ou/"AAy) ...`
`EE D_1"(.)",EE D_2"(.)",EE D_3"(.)", AAx, AAy,`
`(W(x,y,z_1) "et" D_1(x) "et" ¬D_2(x) "et" ¬D_3(x) "et" ...)`
`"ou"(W(x,y,z_2) "et" ¬D_1(x) "et" D_2(x) "et" ¬D_3(x) "et" ...)`
`"ou"(W(x,y,z_3) "et" ¬D_1(x) "et" ¬D_2(x) "et" D_3(x) "et" ...)`
`"ou" ...`
`EEf(.), AAx, AAy, W(x,y,f(x))`
--- 6 septembre 2010 ---
2.2) le typage
On utilise parfois, après la quantification d'une variable, le symboles ` / ` qui signifie "tel que" pour préciser le domaine où s'étend la quantification. Ainsi l'expression suivante :
`AAx "/" x in A "et" x in B, x in C`
signifie quelque soit `x` tel que `x` appartenant à `A` et que `x` appartient à `B`, nous avons `x` appartient à `C`. Cette formule est équivalente à chacune des expressions suivantes :
`AAx "/" x in A, x in B => x in C`
`AAx, (x in A "et" x in B) => x in C`
`AAx, x !in A "ou" x !in B "ou" x in C`
x !in A "ou" x !in B "ou" x in C`
`AAx in A nn B, x in C`
sur un ensemble au sens large c'est à dire sur un terme du langage non augmenté de cette variable,
Axiome d'extensionnalité : Si deux ensembles ont les mêmes éléments, alors ils sont égaux. ( entraine Axiome de l'ensemble vide : Il existe un ensemble sans élément. (<=schéma d'axiomes de compréhension))
Axiome de la paire : Si x et y sont deux ensembles, alors il existe un ensemble contenant x et y et eux seuls comme éléments. (<=schéma de remplacement)
Axiome de la réunion : Pour tout ensemble X, il existe un ensemble R dont les éléments sont précisément ceux des éléments de X et eux seuls.
Axiome de l'ensemble des parties : Pour tout ensemble E, il existe un ensemble dont les éléments sont précisément les sous-ensembles de E.
Axiome de l'infini : Il existe un ensemble W dont \varnothing est élément et tel que pour tout x appartenant à W, x \cup \{x\} appartient aussi à W. On peut ensuite définir par compréhension l'intersection de tous les ensembles contenant \varnothing et clos par cette opération : il s'agit de l'ensemble des nombres entiers tels que définis par von Neumann.
Schéma d'axiomes de compréhension ou de séparation : pour tout ensemble A et toute propriété P exprimée dans le langage, il existe un ensemble dont les éléments sont les éléments de A vérifiant P. Le schéma de compréhension est conséquence du schéma de remplacement qui suit.
Schéma d'axiomes de remplacement : Pour tout ensemble A et toute relation fonctionnelle P, formellement définie comme une proposition P(x,y) et telle que P(x,y) et P(x,z) impliquent que y = z, il existe un ensemble contenant précisément les images par P des éléments de l'ensemble d'origine A.
Axiome de fondation : Tout ensemble X non vide contient un élément y tel que X et y sont des ensembles disjoints (qui n'ont aucun élément en commun), ce qui se note X \cap y = \varnothing. Cet axiome n'est pas toujours ajouté à Z ou ZF. On peut construire assez facilement comme sous-classe d'un modèle quelconque de ZF, un modèle de ZF vérifiant l'axiome de fondation. Les ensembles utiles au développement des mathématiques usuelles appartiennent à cette sous-classe, et donc cela a peu d'importance d'ajouter celui-ci ou non à la théorie pour ces développements.
L'axiome de fondation n'est par exemple pas mentionné dans le livre de Halmos9, dont le but est de présenter les aspects de la théorie des ensembles utiles pour le mathématicien non spécialiste de ce domaine. L'axiome de fondation est par contre très utile dans le domaine spécialisé de la théorie des ensembles, il permet de hiérarchiser l'univers ensembliste, de définir un rang ordinal (voir l'article axiome de fondation) ...Des théories des ensembles, extensions de ZF sans fondation, ont par ailleurs été développées, qui introduisent un axiome d'anti-fondation (il en existe plusieurs variantes) qui contredit directement l'axiome de fondation. L'anti-fondation est une idée assez ancienne (Dimitri Mirimanoff 1917, Paul Finsler 1926), mais ces théories ont connu un regain d'intérêt pour leur lien avec l'informatique théorique10.
Axiome du choix : (version de Zermelo) Étant donné un ensemble X d'ensembles non vides mutuellement disjoints, il existe un ensemble y (l'ensemble de choix pour X) contenant exactement un élément pour chaque membre de X. L'axiome du choix reste controversé pour une minorité de mathématiciens. Des formes faibles existent, comme l'axiome du choix dépendant, très utile pour le développement de l'analyse réelle.
des variables préalablements déclarée par un quantificateur `AA` ou `EE`.
La négation d'une formule s'obtient en remplaçant les quantificateurs `AA` par `EE` et reciproquement, en laissant intacte les expressions sous les symboles ` / ` et en négativant l'expression logique.
Remarquez que l'expression logique `AA x in Ø, P(x)` est identiquement vrai quelque soit `P` tandis que l'expression logique `EE x in Ø, P(x)` est identiquement faut quelque soit `P`.
Puis on opère une unification des objets. Deux fonctions `f"(.)", g"(.)"` sont dites égales ssi `AA x, f(x)=g(x)`. Deux prédicats `R"(.)", S"(.)"` sont dits égaux ssi `AAx R(x)<=>S(x)`. Il est alors possible de définir pour chaque fonction et pour chaque prédicat modulo l'égalité ainsi définie, un élément qui le désigne. On obtient ainsi une deuxième catégorie d'éléments.
Il est alors possible d'étendre les opérateurs et prédicats à ses nouveaux éléments, faisant que le terme `f(f)` est un sens.
Cela n'engendre pas le paradoxe de Russel "l'ensemble des ensembles qui ne se contiennent pas se contient-il ?" car l'existence de l'ensemble n'est pas obligé. Ainsi la proposition suivante est simplement contraditoire :
`EE P"(.)", AA R"(.)", P(R) <=> R(¬R)`