La notion d'ensemble est centrale en mathématique. Même les ensembles finis peuvent faire l'objet de disputes comme nous allons le voir. Mais c'est véritablement lorsqu'il deviennent de taille infinie qu'aparaissent des problèmes inextricables. C'est pourquoi l'étude des ensembles correspond en fait à l'étude de l'infini.
Comme nous n'avons pas d'autres moyens d'étude que le calcul de formules qui sont de taille finie par principe, nous passerons par une étape intermédiaire que sont les ensembles de formules énumérables par une grammaire non-contextuelle selon la hierarchie de Chomsky.
Zermelo propose en 1908 une théorie des ensembles. Nous nous proposons d'en rediscuter la génèse, de reformuler les différentes étapes et de développer d'éventuelles alternatives, sous l'éclairage des avancées mathématiques contemporaines et en particulier de la hierarchie de Chomsky, du théorème d'incomplétude de Godel, du problème de l'arrêt de Turing, du lambda calcul de Church. La hierarchie de Chomsky esquissée en 1956 et démontrée en 1959, est une classification des langages avec leur grammaire qui constitue une programmation de leur énumérateur. Cette classification des grammaires est un théorème fondamentale d'une importance considérable comme il y en a un tous les milles ans, et Noam Chomsky est sans doute le seul savant encore vivant pouvant s'enorgueillir d'une telle avancée pour l'humanité.
Zermelo propose d'écrire axiomatiquement le comportement des ensembles sans pour autant les construire. Et pour éviter les incohérences dues à l'absence de procédé de construction de tous les ensembles, Zermelo propose de n'utiliser que le langage logique du premier ordre, c'est à dire le langage formel du calcul des prédicats.
La théorie des ensembles décrit les propriétés de ce prédicat binaire `"∈"(".,.")` avec une syntaxe centrée, et commence par 4 premiers axiomes, et par un shéma d'axiomes appelé « Schéma d'axiomes de séparation » :
Extensionalité : Deux ensembles ayant les mêmes éléments sont égaux. `AA A AA B,(AAx, x"∈"A<=> x "∈"B) <=> A"="B`
Paire : A partir de deux éléments quelconques, il existe un ensemble qui contient exactement ces deux éléments. `AAaAAbEEpAAx, x "∈"p<=> (x"="a ∨ x"="b)`
Réunion : Pour tout ensemble `E`, il existe un ensemble contenant tous les éléments de tous les ensembles appartenant à `E`. `AAE EE R AAx, x"∈"R<=> (EE p, x"∈"p ∧ p"∈"E")`
Ensemble des parties : Pour tout ensemble `E`, il existe un ensemble de toutes les parties de `E`. `AAE EEP AA A, A"∈"P <=> (AAx, x"∈"A => x"∈"E)`
Schéma d'axiomes de séparation : Pour toute formule unaire `varphi(".")`, et pour tout ensemble `E`, il existe un ensemble qui contient exactement les éléments appartenants à `E` et satisfaisant `varphi"(.)"`. `AAE EE S AAx, x"∈"S<=> (x"∈"E ∧ varphi(x))`
À ce stade, le langage de la théorie ne comprend qu'un seul prédicat binaire `"∈"(".,.")` car on ne mentionne pas le prédicat d'égalité qui est spécifique à la logique du premier ordre.
Pour compléter la présentation, il convient de décrire toutes les formules qui peuvent être utilisées dans le schéma d'axiomes. On le fait en présentant une grammaire qui engendre toutes les formules :
Grammaire des formules : `sfQ ← {AA, EE}` # Quantificateurs `sfV← {x_1,x_2,x_3,...}` # Variables `sfL← {"⊤", sfV"="sfV, sfV"∈"sfV}` # Littéraux affirmatifs `sfF← {sfL,"¬"sfF, sfQsfV & sfF, sfF"⇔" sfF, sfF"⇒" sfF, sfF"∧" sfF, sfF"∨"sfF}` # Formules
Le symbole `"←"` construit un ensemble par une déclaration d'inclusion pouvant être réccurcive, et comprenant des compositions par emboitement. Les parenthèses sont donc nécessaires et implicites autours de chaque composition. Mais la plus part d'entre-elles sont retirées à l'écrit grâce aux règles de priorité syntaxique (qui devront être prédéclarées), et grâce aux propriétés d'associativité (qui devront être préalablement démontrées). Ces inclusions récursives forment une grammaire.
`sfF` représente l'ensemble des formules, mais pas dans la théorie des ensembles de Zermelo, dans une autre théorie où les ensembles sont complètement construit par des grammaires. Se pose alors la question: « L'ensemble des formules constitue-t-il un ensemble selon la définition de Zermelo ? ». Quand bien même ce ne serait pas le cas, cela ne changerait pas la définition du shéma d'axiome de séparation qui décrit un procédé effectif de production de démonstration. Ces ensembles d'un autre type que ceux de Zermelo sont appelés des ensembles énumérables (ou semi-décidables). On pourra discuter plus tard comment introduire formellement ces ensembles énumérables dans la théorie de Zermelo.
On note une formule quelconque de `sfF` ayant par exemple deux variables libres `x_1, x_2` c'est à dire des variables non quantifiées et ne faisant pas partie des constantes du langage, en la nommant par exemple `varphi(".,.")`, comme suit :
`varphi(x_1,x_2)`
Cette nomination correspond à la définition d'un prédicat définissable. C'est pourquoi `sfF` représente l'ensemble énumérable des prédicats définissables. Les propositions sont des prédicats nullaires (ou dit zéro-aire).
On a utilisé le perluéte `&` dans la grammaire pour désigner la virgule dans les formules. Ainsi le terme `sfQsfV & sfF` peut s'instentié par exemple en la formule `EEx,x"∈"x`. Cette virgule n'est à ce stade qu'une décoration pour augmenter la lisibilité.
Les variables peuvent toujours être renommées de façon distincte. Cela ne change pas le sens logique des formules.
Les variables non-quantifiées sont dites libres et constituent des variables muettes servant de variables d'entrée. Leur présence dans une formule indique que c'est une fonction propositionnelle. Par exemple, la formule `AAa, varphi(a,b)` possède une variable libre `b` qui, ne faisant pas partie des constantes du langage, va servir de variable muette, et la formule désigne ainsi une fonction propositionnelle que l'on peut noter fonctionnellement par : `x |-> AAa, varphi(a,x)` et que l'on peut nommer par exemple `P(".")` en définissant un nouveau prédicat comme suit :
`P(x) <=> AAa, varphi(a,x)`
Où d'une manière fonctionnelle explicite :
`P(".") = (x |-> AAa, varphi(a,x))`
Où le suffixe `(".")` indique l'unarité du prédicat `P`. Ainsi, une formule est soit :
Chaque quantification crée un espace de noms contenant le nom d'une nouvelle variable, et qui couvre la formule placée en deuxième argument de la quantification. Cet espace de noms peut venir masquer le nom d'une variable provenant de l'espace de nom de la formule parente ou d'une formule ascendante, ce qui arrive lorsque l'on quantifie un nom de variable déjà utilisé. Ce mode de fonctionnement par emboitement formant une arborescence est propre aux langages algébriques dits déclaratifs.
Lorsque plusieurs quantifications ont lieu d'affilée et peuvent se regrouper pour s'appliquer sur une seule formule, on omet la virgule séparateur, faisant que par exemple `AAx,EEy,varphi(x,y)` s'écrira `AAxEEy,varphi(x,y)`. Ainsi dans la formule `AAxEEy,varphi(x,y)`, les quantificateurs créent un espace de noms contenant les noms de variable `x` et `y` qui couvre la formule `varphi(x,y)`.
Autre simplification, on remplace `"¬"⊤` par `⊥`. On désigne la proposition tautologique par le symbole `"⊤"` qui ressemble à la première lettre de « Tautologie », et qui évoque le ciel, la plus haute valeur logique, le vrai. Tandis que sa négation est représentée par le symbole `"⊥"` qui évoque le sol, la plus basse valeur logique, le faux, l'antilogie.
Ce choix de grammaire et de simplification d'écriture appelé sucre syntaxique, correspond à un compromis équilibré entre lisibilité et simplicité du formalisme.
La grammaire énumère par un procédé effectif toutes les formules qui, regroupées, forment donc un ensemble énumérable noté `sfF`. Un programme rudimentaire calcul l'arité de la formule. Ainsi toutes les formules d'arité `n` sont énumérées par un procédé effectif et forment donc un ensemble énumérable noté `sfF_n`. Toutes les propositions (qu'elles soit vrais ou fausses) sont ainsi énumérées et forment donc un ensemble énumérable noté `sfF_0`. Mais à ce stade, les ensembles énumérables ne sont pas des ensembles (de Zermelo).
Les premier axiomes étant posées, on remarque que la logique étant du premier ordre, il ne peut y avoir qu'un seul type d'élément, et que cet élément est donc nécessairement un ensemble. Ce n'est pas choquant en soit, car qu'est-ce qui différencie un élément d'un autre si ce n'est ses composantes.... parcequ'il est composé différemment par des sous-éléments. On pourrait faire une analogie avec la physique des particules où par exemple, un neutron se caractérise par le fait d'être composé de quarks qui le définissent.
Néanmoins, la construction d'une donnée par le choix d'éléments se fait sans perte d'information par la constitution d'une liste d'éléments et non d'un ensemble d'éléments, parceque nous ne savons pas faire plusieurs choix en même temps.... Mais, il s'agit là d'un biais ontologique. Soit les choix sont fait en même temps... et c'est un ensemble. Soit les choix sont fait les un après les autres... et c'est une liste.
La logique du premier ordre ne manipule qu'un seul type d'élément. Cela signifit que le prédicat d'égalité peut s'appliquer à chacun d'eux, et qu'il est donc toujours possible de supposer l'égalité entre deux éléments quelconques. Dans le cadre de sa théorie, Zermelo désigne le type des éléments vérifiant sa théorie des ensembles, par la lettre `ccB` qui représente ainsi intuitivement le domaine de tous les ensembles sans être lui-même un ensemble.
Considérons une théorie des ensembles alternatives. Si nous voulons faire côtoyer les deux théories des ensembles, il nous faut distinguer les éléments de l'une, des éléments de l'autre, par des types distincts `ccB_1` et `ccB_2`, qui doivent être refondu en un seul type. Chaque élément possède un type `ccB_1` s'il est présent et compatible dans la première théorie, et possède un type `ccB_2` s'il est présent et compatible dans la seconde théorie. Et donc, si par supposition, ils sont supposés égaux, il doivent alors pouvoir posséder les deux types à la fois. Pour permettre cela, il faut poser au départ une typologie non exclusive. Cela se fait en posant deux prédicats unaires `ccB_1(".")`, `ccB_2(".")` désignant les types possibles. Ainsi, un élément `x` peut avoir les deux types en supposant la propriété `ccB_1(x) ∧ ccB_2(x)`.
Etudier la théorie des ensembles de Zermelo consiste d'abords à étudier le calcul des prédicats, la logique du premier ordre et des théories énumérables du premier ordre, où l'on entend par énumérable le fait qu'elle soit produite par un procédé effectif c'est à dire par un programme, et cela signifie qu'elle est engendré par une grammaire. Et nous nous restreindrons aux seuls grammaires non-contexuelles comme celle qui engendre l'ensemble des formules.
On ne peut pas utiliser la théorie des ensembles pour définir la théorie des ensembles. On part donc d'une conception des ensembles plus modeste, celle des ensemble finis qui ne pose pas de difficulté puisque leur définition complète tient en une formule, puis celle un peu plus compliquée des ensembles de formules dans un langage fini, énumérables par un procédé effectif, c'est à dire engendrées par une grammaire. Et nous n'utiliserons pas le type le plus générale de grammaire de la hierarchie Chomsky, mais des procédés mélangeant des grammaires hors-contextes (synonyme de non-contextuelle) comme celles présentées en introduction, et des programmes rudimentaires.
On voit donc, comment la naissance du concept d'ensemble dans sa plus grande généralité est à la croisée des chemins des mathématiques et de la programmation, de la logique et de la calculabilité.
Les 4 premiers axiomes permettent de construire des ensembles par agrandissement à partir d'ensembles, tandis que le shéma de séparation permet de construire des sous-ensembles, donc des ensembles plus petits. Mais pour pouvoir procéder à ces constructions, il faut au moins un ensemble, qui sert de point de départ.
À ce stade il existe un ensemble particulièrement simple qu'est l'ensemble vide. Sa définition est qu'il ne contient aucun élément. Est-il unique ? Oui, grâce à l'axiome d'extensionalité. Existe-t-il ? Pour cela il faut l'ajouter parmi les axiomes, car sinon l'alternative toujours possible est qu'il n'existe aucun ensemble.
C'est pourquoi est ajouté au langage l'ensemble vide, `Ø`, et l'axiome le caractérisant :
Ensemble vide: `"Ø"` est l'ensemble vide. `AAx, x"∉Ø"`
Nous faisons la distinction entre un ensemble (sous entendu de Zermelo) et un ensemble énumérable qui désigne une énumération d'expressions par un procédé effecif, c'est à dire un langage engendré par une grammaire.
Dans la théorie de Zermelo, comment définir des ensembles finis ? Il faut pouvoir définir des éléments. Le premier élément disponible est celui générateur du langage, l'ensemble vide, `"Ø"`. À partir de celui-ci et à l'aide des 4 premiers axiomes, on peut énumérer une infinité d'ensembles finis distincts.
Mais on ne peut pas prouver l'existence d'un ensemble infini. L'énumération que nous évoquons crée un ensemble énumérable d'ensembles finis, mais ne constitue pas pour l'instant un ensemble (de Zermelo).
La construction la plus simple consiste en une infinité d'ensembles inclus les uns dans les autres et construit itérativement à partir du précédent, Si l'on part de l'ensemble `"Ø"` que l'on identifie au nombre zéro, on peut ainsi définir les entiers naturels `NN`.
Mais à ce stade on ne peut pas prouver que `NN` est un ensemble.
`0 = Ø`
`1 = {0} = {Ø}`
`2 = {0,1} = {Ø,{Ø}}`
`3 = {0,1,2} = {Ø,{Ø},{Ø,{Ø}}}`
`n= {0,1,2,...,(n"-"1)}`
L'entier `n` est défini comme étant l'ensemble contenant les entiers inférieurs. L'entier suivant `n+1` est égale à l'union de `n` et de `{n}`.
Les premiers axiomes n'empêchent pas les ensembles de se contenir en tant qu'élément. Considérons deux ensembles `e_1,e_2` chacun contenant uniquement lui-même :
`AAx, x"∈"e_1 <=> x"="e_1`
`AAx, x"∈"e_2<=> x"="e_2`
En quoi `e_1` et `e_2` sont-ils différent ? En rien, le nom des variables ne constitue pas une information car les variables peuvent être renommées toujours de façon distincte sans que cela de change le sens de la formule, c-à-d sans que cela ne change sa sémantque. On peut donc vouloir augmenter l'axiome d'extensionalité afin que dans une telle situation, nous puissions déduire que `e_1"="e_2`, autrement dit, qu'il existe un unique ensemble qui contient exactement un élément qui est lui-même.
Nous verrons après l'introduction des opérateurs comment procéder pour étendre la théorie des ensembles en ce sens.
On ne peut pas utiliser la théorie des ensembles pour définir la théorie des ensembles, alors qu'est-ce que l'on utilise ? Les règles de raisonnement logique en logique du premier ordre. Le système de démonstration permet de calculer tout ce qui est calculable... ce qui fait d'un programme une méthode de démonstration... où l'exécution du programme correspond à la démonstration. Apparait alors la notion d'ensemble énumérable de formules, qui n'est pas concidéré comme un ensemble, juste comme regroupant toutes les formules produisibles par un énumérateur (un programme) sachant que, dans le cas général, on n'est jamais sûr qu'une formule ne finisse pas par être énuméré par l'énumérateur. Ainsi, l'énumérateur ne donne jamais de réponse négative, c'est pourquoi l'ensemble énumérable est qualifié de semi-décidable, et en générale son complément n'est pas énumérable. Etant donné une formule, si cette formule est produisible par l'énumérateur, il suffit d'attendre suffisament longtemps la prodution de cette formule qui constitue la preuve (la preuve que cette formule est produisible par l'énumérateur). En revanche si elle n'est pas produisible par l'énumérateur, celui-ci ne donnera jamais la réponse, et il n'y a donc pas de preuve, pas de démonstration (pas de démonstration que cette formule n'est pas produisible par l'énumérateur).
Dans la suite du document on ne retiendra comme propriété des ensembles énumérables de formules, non pas qu'ils sont des ensembles au sens où on l'entend classiquement, mais le seul fait qu'il existe un programme de taille fini (une grammaire de type 0 dans la hierarchie de Chomsky) qui énumère toutes ses formules. Et c'est ce seul procédé sans aucune autre propriété qui sera intégré dans les démonstrations.
Etant donné un ensemble énumérable `E`, la formule `AAx "∈" E, varphi(x)` abuse de la notation d'appartenance à un ensemble et doit donc être intérprété plus faiblement : Elle signifie seulement que l'énumérateur `E` ne produit que des éléments `x` qui satisfont `varphi(".")`.
Avant d'étudier le calcul des prédicats, on étudie la logique propositionnelle aussi appelé logique d'ordre zéro car il n'y a pas de variable élémentaire, il y a seulement des variables booléennes. Les propositions sont par principe de taille finie, elles ne peuvent donc comprendre qu'un nombre fini d'inconnus booléens, et donc ne possédent qu'un langage fini. Toutes les propositions d'ordre zéro sont énumérées par la grammaire suivante :
Grammaire des propositions d'ordre zéro : `sfV← {A_1,A_2,A_3,...}` # Variables `sfP← {sfV,"¬"sfP, sfP"⇔" sfP, sfP"⇒" sfP, sfP"∧" sfP, sfP"∨"sfP}` # Propositions
Comme il n'y a pas de variable élémentaire, il n'y pas de variables élémentaires muettes, et donc toute formule est une proposition. Les règles de déduction sont décites dans le chapitre Logique propositionnel, un système de démonstration à peine plus simple que celui de la logique du premier ordre, mais qui nous permet de distinguer et de maitriser complètement la notion de démonstration qui relève de la syntaxe, et la notion du sens réel des propositions qui relève de la sémantique.
En logique propositionnelle, il n'y a pas d'élément, juste des inconnus booléens. Et les propositions étant par principe de taille fini, il n'y a qu'un nombre fini d'inconnus booléens. Le nombre de monde possibles est fini. Leur regroupement forme un ensemble fini appelé « univers » que l'on note `Omega`. C'est l'ensemble des réalités possibles.
Le sens réel d'une formule, c'est sa sémantique, c'est l'ensemble des réalités possibles où la formule est vrai. C'est l'ensemble des mondes où la formule est vrai. C'est aussi la connaissance de l'ensemble des mondes où elle est fausse, et dans le cas de la logique propositionnelle cela correspond exactement au complément dans `Omega`.
En logique propositionnelle la sémantique est simple à définir, car l'ensemble des mondes possibles est finis. Considérons un langage comprenant 3 variables booléennes `{A,B,C}`. Ce sont trois constantes booléennes inconnues. Chaque monde est défini par les valeurs booléennes de ces trois variables. Il y a donc `2^3` mondes possibles représentées par la table de vérité et regroupé dans l'univers `Omega`.
Chaque monde est désigné par une forrme normale conjonctive, c'est à dire une conjonction dans laquelle chaque variable du langage apparait une seule fois, soit de façon affirmative ou soit de façon négative. Exemple de monde : `A∧"¬"B∧C`.
Il y a deux formes normales pour désigner un monde :
L'ensemble des mondes étant fini, il n'y a pas de problème de fondation, un monde est une formule et il n'y a pas de différence entre théorie et proposition. La sémantique d'une proposition logique d'ordre zéro (c-à-d sans variable élémentaire mais qu'avec des inconnus booléens) dans un langage donné c'est à dire comprenant `n` constantes booléennes inconnues, se définit comme étant la signification complète de la dite proposition, c'est à dire comme étant l'ensemble des mondes possibles du langage où la dite proposition est vrai. Et c'est aussi la connaissance de l'ensemble des mondes où elle est fausse, et dans le cas de la logique propositionnelle cela correspond exactement au complément dans `Omega`.
Une proposition telle que `(A∨B)` peut être vrai ou fausse dans chaque monde. Pour indiquer que dans le monde `ccM`, la proposition `varphi` est vrai, on dit que `varphi` est satisfaite dans le monde `ccM`, et on utilise l'expression suivante :
`ccM ⊨ varphi`
Nous avons par exemple :
`(A∧"¬"B∧C) ⊨ (A∨B)`
Si le premier membre n'est pas un monde (une forme normale conjonctive) mais une proposition, sa sémantique étant l'ensemble des mondes où elle est satisfaite, l'expression signifie alors que chaque monde où le premier rmembre est satisfait, satisfait également le second membre. Ainsi, pour indiquer que chaque monde satisfaisant `varphi_1`, satisfait `varphi_2` on note :
`varphi_1 ⊨ varphi_2`
C'est pourquoi l'opération `"⊨"` s'appelle une implication sémantique.
La contraposée n'est pas évoquée. Elle est évidente en logique propositionnelle, mais pas dans les extensions de la logique. Faut-il alors ajouter cette condition à la définition de l'implication sémantique, à savoir que chaque monde satisfaisant `"¬"varphi_2` doit satisfaire `"¬"varphi_1` ? On n'a as de réponse pour l'instant. C'est pourquoi on définit une seconde notation de satisfaisabilité avec contraposée qui sera utile dans les extensions de la logique. Ainsi, pour indiquer que chaque monde satisfaisant `varphi_1`, satisfait `varphi_2`, et que chaque monde satisfaisant `¬varphi_2`, satisfait `varphi_1`on notera `varphi_1 ⊫ varphi_2`. On étend la relation de satisfaisabilité aux ensemble de propositions. Mais de quelle définition d'ensemble parlons-nous ? Un ensemble fini pour commencer qui ne pose pas de problème, puis un ensemble de propositions énumérable par une grammaire hors-contexte par la suite. Considérons donc de tels ensembles de propositions, `A, B`. L'ensemble `A` implique sémantiquement l'ensemble `B`, si et seulement si, chaque monde satifaisant toutes les propositions de `A`, satisfait également toutes les propositions de `B`.
`A ⊨ B`
Une théorie, comme nous le verrons plus-tard, est un ensemble de propositions énumérables par une grammaire hors-contexte, et interprété comme une conjonction. La théorie étant par définition une conjonction, si elle est vide alors elle est tautologique. Sa sémantique contient tous les mondes. Ainsi pour signifier qu'une proposition `varphi` est vrai dans tous les mondes possibles, on peut noter `"⊤"⊨ varphi`, ou bien `{}⊨ varphi`, ou plus simplement :
`⊨ varphi`
Lorsque la supposition d'une proposition `varphi_1` permet de démontrer une proposition `varphi_2`, à l'aide du système de démonstration classique, on note alors cette propriété par l'expression suivante :
`varphi_1 |-- varphi_2`
Et nous avons alors la poposition `varphi_1"⇒"varphi_2` qui est une tautologie, ce qui se note:
`|-- (varphi_1"⇒"varphi_2)`
où le membre de gauche est l'hypothèse vide qui est la théorie vide, c'est à dire la tautologie `"⊤"`.
On étend la relation de démontrabilité aux ensemble de propositions interprétés comme des conjonctions de propositions. Mais de quelle définition d'ensemble parlons-nous encore ? et ce sera la même réponse, un ensemble fini pour commencer qui ne pose pas de problème, puis un ensemble de propositions énumérable par une grammaire hors-contexte par la suite. Considérons donc de tels ensembles de propositions, `A, B`. L'ensemble `A` démontre `B`, si et seulement si, chaque proposition de `B` est le résultat d'une démonstration n'utilisant que les propositions de `A` et le système de démonstration classique de la logique propositionnelle. Comme une démonstration est par principe de taille finie. Cela signifie, si et seulement si, pour chaque proposition `p` de `B`, il existe des propositions de `A` en nombre fini qui permettent de démontrer `p`.
`A|--B`
Le système de démonstration classique de la logique propositionnelle est dit complet. Cela signifie que pour toute proposition `varphi`, si elle est vrai dans tous les mondes alors elle est démontrable à l'aide du système de démonstration classique de la logique propositionnelle :
`(⊨ varphi) => (|-- varphi) `
La relation de satifaisabilité est au départ une relation incluse dans `Omega"×"sfP` vérifiant 3 axiômes. On dit quelle est tautologue, cohérente et complète :
Tautologue : Les mondes satisfont les tautologies. `AA ccM "∈" Omega, AA A"∈"sfP, (|--A) => (ccM|==A)`
Cohérente : Un monde ne satisfait pas à la fois une proposition et sa négation. `AA ccM "∈" Omega, AA A "∈" sfP, (ccM|==A) => "¬"(ccM|=="¬"A)`
Complète: Si un monde ne satisfait pas la négation d'une proposition, alors il satisfait la proposition. `AAccM"∈" Omega, AA A "∈" sfP, ¬(ccM|==¬A) => (ccM|==A)`
On étend la relation de satisfaisabilité pour que le second membre puisse être un ensemble énumérable de propositions comme suit:
`AA E "⊆" sfP, AAccM "∈" Omega, ccM|==E <=> AA A"∈"E, M|==A`
On étant la satisfaisabilité pour que le premier membre soit une formule comme suit:
`AA (E,A) "∈" sfP^2, A|==E <=> AAccM "∈" Omega, ccM|==A <=> ccM|==E`
Et on étant la satisfaisabilité pour que le premier membre soit un ensemble énumérable de formules comme suit:
`AA (E,A) "∈" sfP^2, A|==E <=> AAccM "∈" Omega, ccM|==A <=> ccM|==E`
Les ensembles énumérables de formules sont visiblement utilisés ici comme des conjonctions de formules, c'est pourquoi l'ensemble vide de formule désigne la tautologie. Et que l'on autorise la notation `(|--A)` pour dire que `A` se démontre sans hypothèse, et `(|==A)` pour dire que tous les monde satisfont `A`, qui s'étend aux ensembles énumérables de formules. `(|--E)` signifie que toute formule appartenant à `E` se démontre sans hypothèse. `(|==E)` signifie que tous les mondes satisfont toutes les propositions énumérées à `E`.
Comment prouver que l'ensemble des formules constitue un ensemble selon Zermelo ? Il faut d'abord ajouter un shéma d'axiomes pour prouver qu'une formule est un élément. Pour cela, on a besoin d'un certain nombres de symboles `AA, EE, "⊤", "=", "∈","¬","⇔","⇒","∧","∨", sfQ, sfV,sfL,sfF,"←"` et d'une liste non bornée de symboles désignant les variables élémentaires `x_1,x_2,x_3,...`, qui doivent pouvoir être définis comme des éléments. Puis les formules engendrées par la grammaires doivent pouvoir être définies comme des éléments. Puis le regroupement de toutes ces formules doit pouvoir être défini comme un ensemble. Il faudra donc à la fin de notre étude ajouter un shéma d'axiomes garantissant cela.
Néanmoins, les ensembles énumérés de formules sont semi-décidables, c'est à dire que leur complément dans un ensemble mère plus vaste n'est pas forcement énumérable c'est à dire qu'il n'existe aucun procédé effectif, aucun programme de taille fini, capable d'énumérer toutes ses formules. Dans ce chemin emprunté, cela entraine de facto une contradiction. C'est pourquoi on se restreint aux seuls énumérateurs correspondant aux grammaires non-contextuelles On utilise alors la propriété que le complément d'un sous-langage récursivement énumérable d'un langage lui-même récursivement énumérable est récurcif, et donc que le complément d'un sous-langage énuméré par une grammaire hors-contexte, d'un langage lui-même énuméré par une grammaire hors-contexte, est énumérable par une grammaire générale.
Lorsque l'on conçoit un prédicat non-nullaire avec la possibilité de supposer à chaque instant l'existence d'un élément dépendant d'une finitude d'autres éléments, on passe alors à la logique du premier ordre.
Dans cette logique, il est toujours possible de supposer l'existence de nouveaux éléments. C'est pourquoi la liste des mondes possibles n'est plus finie.
La logique est dite du "premier ordre", car il n'y a qu'un seul type d'éléments, dans le sens où deux éléments quelconques peuvent toujours faire l'objet d'une hypothèse d'égalité. Les formules étant par principe de taille finie, elle ne contiennent qu'un nombre fini de suppositions d'existence d'élément dépendant d'une finitude d'autres éléments. Considérons par exemple la proposition suivante, où `varphi` est une formule quaternaire c'est à dire appartenant à `sfF_4` :
`AAxEEyAAzEEt, varphi(x,y,z,t)`
Cette proposition affirme l'existence d'un élément `x` dépendant de `y` et l'existence d'un élément `t` dépendant de `(x,y,z)` tel que `varphi(x,y,z,t)`.
Le domaine des éléments n'étant pas limité, on ne peut plus utiliser les seuls ensembles finies pour définir les mondes. Qu'est ce qu'un monde ? Qu'elle sont les propriétés que doit satisfaire un monde ? Le chapitre suivant répond à cette question.
Qu'elles sont nos outils ? Nous utilisons les ensembles finis de formules, et un autre type d'ensembles un peu plus sophistiqué que sont les ensembles énumérables de formules par une composition de programmes rudimentaires et de grammaires hors-contextes, qui constitue encore un ensemble de formules engendrée par une grammaire hors-contexte.
Pourquoi ce choix ? Le langage logique du premier ordre étant de syntaxe engendrée par une grammaire hors-contexte (voir la grammaire des formules en introduction), il est naturelle de se restreindre aux seuls théories du premier ordre engendrée par des grammaires hors-contextes. C'est pourquoi dans la suite du document, toute théorie est un ensemble de propositions engendrées par une grammaire hors-contexte. Et si les théories, qui correspondent aux caractéristiques exprimables des mondes, sont construites ainsi, alors il est raisonnable de penser qu'il puisse en être de même pour les mondes.
Les grammaires hors-contextes engendrent les langages avec des parenthèses bien équilibrées, qui constituent la syntaxe de base des langages de programmation. La grammaire hors-contexte n'est pas la grammaire générale mais elle peut potentiellement programmer l'énumérateur d'une grammaire générale. C'est pourquoi on se limite à cette grammaire hors-contexte aussi appelé grammaire algébrique.
Nous tentons ainsi d'aborder la théorie des modèles d'une façon plus modeste fondée par un procédé calculatoire.
On note `bbbT` l'ensemble des théories (engendrées par des grammaires hors-contextes), On note `Omega` l'univers regroupant l'ensemble des mondes. L'ensemble `bbbT` existe et est énumérable, en énumérant toutes les grammaires hors-contextes possibles. Par contre nous ne savons pas encore si un tel ensemble de mondes `Omega` existe.
Ne pouvant appliquer les mêmes règles que pour la logique propositionnelle, on propose une approche plus flexible en redéfinissant plus faiblement la relation de satisfaisabilité et de monde. À la différence de la logique propositionnelle, un monde dans la logique des prédicats n'est pas obligé de trancher toutes les propositions, il est seulement obligé, s'il ne tranche pas la proposition, d'être inclus dans deux mondes, l'un affirmant la proposition, l'autre réfutant la proposition.
La relation de satifaisabilité est au départ une relation incluse dans `Omega×sfF` vérifiant 3 axiômes :
Tautologue : Les mondes satisfont les tautologies `AA ccM "∈" Omega, AA A"∈"ssF_0, (|--A) => (ccM|==A)`
Cohérence: Un monde ne satifait pas à la fois une proposition et sa négation `AA ccM "∈" Omega, AA A "∈" sfF_0, (ccM|==A) => "¬"(ccM|=="¬"A)`
Complétion: Si un monde ne satisfait pas la négation d'une proposition, alors il est inclus dans un monde qui satisfait la proposition. `AAccM"∈" Omega, AA A "∈" sfF_0, ¬(ccM|==¬A) => EEccN"∈" Omega, (ccM sube ccN) "et" (ccN|==A)`
On étend la relation de satisfaisabilité pour que le second membre puisse être un ensemble énumérable de propositions comme suit:
`AA E sube sfF_0, AAccM "∈" Omega, (ccM|==E) <=> AA A"∈"E, (M|==A)`
On étant la satisfaisabilité pour que le premier membre soit une proposition comme suit:
`AA (E,A) "∈" sfF_0^2, (A|==E) <=> AAccM "∈" Omega, (ccM|==A) <=> (ccM|==E)`
Et on étant la satisfaisabilité pour que le premier membre soit un ensemble énumérable de propositions comme suit:
`AA (E,A) "∈" sfF_0^2, (A|==E) <=> AAccM "∈" Omega, (ccM|==A) <=> (ccM|==E)`
Délors la définition d'un monde coïncide avec la définition d'une théorie, et nous avons la propriété de complètude. Pour toutes théories `T` engendrée par une grammaire hors-contexte, et pour toute proposition `P` exprimés dans le langage de la théorie `T`, nous avons :
`(T|==P) <=> (T|--P)`