Logique (mathématiques)/Complétude de la logique du premier ordre
Le théorème de complétude du calcul des prédicats du premier ordre a été prouvé par Kurt Gödel[1]. Il affirme que le calcul des prédicats est complet au sens où on connait des listes finies et complètes de tous ses principes.
Nous allons donner plusieurs définitions équivalentes de cette notion de complétude.
Le théorème de complétude
[modifier | modifier le wikicode]On peut donner un nombre fini d’axiomes, de schémas d’axiomes ou de règles de déduction tel que toutes les preuves logiquement valides formulées avec la grammaire du calcul des prédicats du premier ordre soient obtenues à partir de ces principes.
La notion de validité logique d’une preuve est précisée par la théorie des modèles. Une règle de déduction est valide lorsque tout modèle de ses prémisses est aussi un modèle de sa conclusion. Un axiome logique est valide lorsqu’il est vrai dans tous les modèles. Un schéma d’axiomes est un principe logique valide lorsque tous les axiomes produits par ce schéma sont des axiomes logiques valides. Un système de principes logiques est valide lorsque ses axiomes, ses schémas d’axiomes et ses règles de déduction sont valides. Une preuve est logiquement valide lorsqu’elle peut être formalisée dans le cadre d’un système logique valide.
Nous allons prouver que la liste des quinze règles de déduction naturelle est un système complet des principes de la logique du premier ordre. Ce théorème est équivalent à celui de Gödel. Mais la preuve de Gödel est basée sur une autre formulation des principes logiques, celle des Principia Mathematica de Whitehead et Russell.
Donnons d’abord de ce théorème plusieurs formulations équivalentes.
Il faut quelques définitions : conséquence logique, prouvabilité, cohérence et incohérence dans un système logique, possiblement et absolument vrai et faux.
Si p et q sont deux formules du calcul des prédicats, on dira que q est une conséquence logique de p lorsque tout modèle de p est aussi un modèle de q, autrement dit, pour tout modèle m, si p est vrai dans m alors q est vrai dans m.
On peut remarquer qu’il y a une circularité dans cette définition, au sens où on ne peut pas la comprendre si l’on ne sait pas déjà ce qu’est une conséquence logique. Le but d’une telle définition n’est pas d’apprendre au lecteur ce qu’est une conséquence logique. On suppose qu’il le sait déjà, ou qu’il en a une idée, peut-être un peu vague. Le but ici est seulement de préciser une notion intuitive, de lui donner une formulation sans équivoque.
Si p et q sont deux formules du calcul des prédicats, q est prouvable à partir de p dans un système logique L, lorsqu’il existe une preuve de q à partir de p dans L, au sens où les règles de déduction de L suffisent pour déduire q en un nombre fini d'étapes à partir de p et des axiomes logiques de L.
Une formule p est cohérente dans L lorsque pour toute formule q, (q et non-q) n’est pas prouvable à partir de p dans L.
Une formule p est incohérente dans L lorsqu’il existe une formule q telle que (q et non-q) soit prouvable à partir de p dans L.
Une formule p du calcul des prédicats est possiblement vraie lorsqu’elle est vraie dans au moins un modèle. Elle est absolument vraie, ou est une loi logique, lorsqu’elle est vraie dans tous les modèles. Elle est possiblement fausse lorsqu’elle est fausse dans au moins un modèle. Elle est absolument fausse, ou est une contradiction logique, lorsqu’elle est fausse dans tous les modèles.
On peut alors énoncer le théorème de complétude sous la forme suivante.
Il existe des systèmes logiques valides L qui satisfont aux trois conditions équivalentes suivantes.
- pour toutes formules p et q (du calcul des prédicats du premier ordre), si q est une conséquence logique de p, alors q est prouvable à partir de p dans L ;
- pour toute formule p, si p est cohérente dans L, alors p est possiblement vraie ;
- pour toute formule p, si p est absolument fausse, alors p est incohérente dans L.
La déduction naturelle ne contient pas d'axiomes logiques ou de schémas d'axiomes mais seulement des règles de déduction. On peut alors définir les vérités anhypothétiques comme les formules prouvables, en un nombre fini d’applications des quinze règles, à partir d'aucune hypothèse. Dans ce cas particulier, on peut alors donner au théorème de complétude la forme suivante.
- Pour toute formule p, si p est absolument vraie, alors p est une vérité anhypothétique.
Ou encore :
- Pour toute formule p, si p est absolument fausse alors (non-p) est une vérité anhypothétique.
Il faudra prouver au préalable que la déduction naturelle est un système logique valide, ce qui reviendra à prouver que si p est une vérité anhypothétique alors p est absolument vraie, pour toute formule p (du calcul des prédicats du premier ordre).
On peut enfin remarquer qu'un ensemble défini par induction avec un nombre fini de principes (axiomes, schémas d'axiomes et règles de déduction) est énumérable. Autrement dit, toutes les théories axiomatiques sont des ensembles énumérables. Le théorème de complétude dit qu’il existe des théories axiomatiques complètes de la logique du premier ordre, ou plus précisément.
L'ensemble des lois logiques est énumérable
[modifier | modifier le wikicode]Nous verrons plus loin qu’on peut relier ce théorème de complétude à la théorie de l'indécidabilité, parce qu'on peut prouver que l’ensemble des lois logiques est indécidable. Autrement dit, l’ensemble des formules possiblement fausses n’est pas énumérable, ou, de façon équivalente, l’ensemble des formules possiblement vraies n’est pas énumérable. Cela revient à dire que l'imagination déborde tous les cadres.
Les sections suivantes, jusqu’à la fin du chapitre sur la logique, sont d’un niveau un peu plus élevé que ce qui précède. Elles peuvent être omises sans que cela nuise trop à la compréhension des chapitres suivants.
Validité du calcul des prédicats du premier ordre
[modifier | modifier le wikicode]Le calcul des prédicats est valide au sens où si une formule c est déductible avec les règles de la déduction naturelle à partir d’une formule h, alors c est une conséquence logique de h, au sens de la théorie des modèles, rappelé ci-dessus.
Pour le prouver, il est plus commode de raisonner sur un calcul de séquences, inventé par Gerhard Gentzen, et dont une formalisation a été exposée ci-dessus (Autres formulations des principes de la logique du premier ordre).
Une séquence est valide lorsque tout modèle de ses prémisses est aussi un modèle de sa conclusion.
Montrons que toutes les séquences prouvables sont valides.
Une séquence est prouvable si elle est ou bien un axiome, ou bien déduite des axiomes par un nombre fini d’applications des règles de la déduction naturelle des séquences. Les axiomes sont ici toutes les séquences de la forme (p implique p) où p est une formule du calcul des prédicats. Ils sont évidemment valides. On peut alors montrer, à partir de la définition de la vérité des formules complexes (voir théorie des modèles), qu'en partant de séquences valides, on ne peut déduire que des séquences valides si on applique une des règles de la déduction naturelle des séquences. Le principe d'induction complète suffit alors pour conclure que toutes les séquences prouvables sont valides.
La façon dont les règles de calcul ont été formulées montre que si la formule c est déductible à partir de h avec les règles de la déduction naturelle alors (h implique c) est une séquence prouvable, donc valide. Cela termine cette preuve de la validité des règles de la déduction naturelle.
On peut aussi en déduire que les vérités anhypothétiques sont absolument vraies. Si p est une vérité anhypothétique alors (silence implique p) est une séquence prouvable, donc valide. Comme silence est vrai dans tous les modèles, p est absolument vraie.
Existence d’un modèle sous l'hypothèse de cohérence
[modifier | modifier le wikicode]Nous allons prouver le théorème de complétude sous la forme suivante :
- « Si une formule est cohérente alors elle est possiblement vraie. »
Cohérente veut dire qu'aucune contradiction n'est prouvable si on prend cette formule comme hypothèse.
En fait nous prouverons une version renforcée de ce théorème :
- « Si un ensemble d'axiomes est cohérent alors il est possiblement vrai. »
Un ensemble d'axiomes est cohérent lorsqu'aucune contradiction n'est prouvable à partir d’un nombre quelconque, fini, de ces axiomes. Il est possiblement vrai lorsqu’il y a un modèle dans lequel les axiomes sont tous vrais. Cette version renforcée du théorème est utile en particulier pour énoncer le paradoxe de Skolem, parce qu’elle permet d’appliquer le théorème de complétude à des systèmes infinis d’axiomes.
Commençons par montrer comment remplacer un système d’axiomes du calcul des prédicats par un système équivalent d’axiomes du calcul des propositions. Pour cela, on commence par mettre chaque axiome sous une forme prénexe.
Une formule du calcul des prédicats est toujours équivalente à une formule mise sous forme prénexe, c'est-à-dire une formule dans laquelle tous les quantificateurs universels et existentiels sont placés au début et non à l'intérieur des sous-formules. On peut toujours prouver qu'une formule est équivalente à une formule prénexe avec les règles de déduction suivante :
- de ((il existe x tel que p) et q) déduire (il existe x tel que (p et q)), pourvu que q ne contienne pas x comme variable libre. Si elle la contient, il suffit de substituer à x dans (il existe x tel que p) une autre variable qui n'apparait pas dans q.
- de ((il existe x tel que p) ou q) déduire (il existe x tel que (p ou q)) , pourvu également que q ne contienne pas x comme variable libre. Si elle la contient, il suffit de substituer à x dans (il existe x tel que p) une autre variable qui n'apparait pas dans q.
- deux autres règles semblables pour le quantificateur universel « pour tout x ».
- de non-(il existe x tel que p) déduire (pour tout x, non-p).
- de non-(pour tout x, p) déduire (il existe un x tel que p).
Toutes ces règles sont des règles dérivées dans le système de déduction naturelle et elles font toutes passer d’une prémisse à une conclusion équivalente. Par itération elles fournissent une formule prénexe équivalente à la formule initiale.
De la forme prénexe d’un axiome, on passe à sa forme de Skolem en introduisant de nouveaux opérateurs fondamentaux, autant qu’il en faut pour faire disparaître tous les quantificateurs existentiels dans les axiomes.
Par exemple, l’axiome prénexe (pour tout x)(il existe un y tel que x+y = 0) est remplacé par (pour tout x) (x+(-x) = 0) où - est un nouvel opérateur unaire.
Pour un axiome de la forme (pour tout x)(pour tout y)(il existe un z tel que Pxyz), on introduit un opérateur binaire, * par exemple, et on prend pour axiome (pour tout x)(pour tout y)( Pxy(x*y) ).
On construit alors un univers, un domaine des êtres nommés. Les noms des objets de base sont ceux qui sont mentionnés dans les axiomes. S’il n’y en a pas, on en introduit un, qu’on peut appeler comme on veut, 0 par exemple.
L’ensemble des noms d’objet est celui obtenu par induction à partir des noms des objets de base et des noms de tous les opérateurs mentionnés dans les axiomes d’origine ou introduits par la méthode ci-dessus exposée. L’univers U est l’ensemble de tous les êtres ainsi nommés.
Chaque forme de Skolem d’un axiome peut être conçue comme un schéma d’axiomes à l'intérieur du calcul des propositions. On supprime tous les quantificateurs universels et on remplace toutes les variables alors libres par des noms d’objet. À chaque axiome de départ on associe ainsi un ensemble infini de formules du calcul des propositions. La réunion de toutes ces formules associées à tous les axiomes de départ, est le nouveau système d’axiomes, non quantifiés, équivalent au système d’origine.
Montrons maintenant que si un sous-ensemble fini du système d'axiomes non-quantifiés est incohérent alors le système d'axiomes d'origine est lui aussi incohérent. Soit C une conjonction incohérente d'axiomes non-quantifiés. Soit C’ la formule obtenue à partir de C en remplaçant tous ses constantes par des variables distinctes, de telle façon que C ne contienne plus d'opérateurs d'objet, et en quantifiant existentiellement sur toutes ces variables. Comme C est incohérente, C’ l'est aussi. Mais C' peut être prouvée à partir d’un nombre fini des axiomes d'origine, qui sont donc eux aussi incohérents.
Si un système d'axiomes est cohérent tous les sous-ensembles finis du système d'axiomes non quantifiés sont également cohérents. D'après le théorème de complétude du calcul des propositions - démontré en annexe - ils sont donc tous possiblement vrais. D'après le théorème de compacité - également démontré en annexe - le système - infini - d'axiomes non quantifiés est lui aussi possiblement vrai. Comme un modèle du système d'axiomes non-quantifiés est également un modèle du système d'origine, on a prouvé l’existence d’un modèle pour tout système cohérent d'axiomes.
Théorème de complétude du calcul des propositions
[modifier | modifier le wikicode]Le calcul des propositions est un calcul restreint aux formules logiques non quantifiées. Le théorème de complétude du calcul des propositions peut être énoncé de la façon suivante.
Les règles de la déduction naturelle suffisent pour prouver toutes les lois logiques propositionnelles, c’est-à-dire les lois logiques non-quantifiées, ou propositions vraies dans tous les modèles.
Ce théorème a été prouvé par Paul Bernays en 1926.
Vérité d’une proposition dans un modèle
[modifier | modifier le wikicode]Pour le calcul des propositions, il n’est pas nécessaire d’analyser la structure des formules atomiques en prédicat et objet(s). La seule propriété des propositions atomiques qui compte dans les calculs de la logique classique est leur vérité ou leur fausseté. On peut représenter les propositions par des lettres, p, q, r… et les concevoir comme des variables qui peuvent recevoir deux valeurs, V pour vrai, et F pour faux.
Un modèle est défini par l’attribution de valeurs de vérité, V ou F, aux propositions atomiques. Par exemple (Vp, Fq, Vr) nomme le modèle dans lequel il y a trois propositions atomiques p, q, et r, la seconde étant fausse et les deux autres vraies.
On peut définir un calcul des vérités semblable au calcul des nombres. Ses axiomes sont les suivants.
- (non-V) = F , (non-F) = V , (V et V) = V , (V et F) = (F et V) = (F et F) = F
On peut alors calculer, par exemple, que dans le modèle (Fp),
- non-(p et non-p) = non-(F et non-F) = non-(F et V) = (non-F) = V
On en conclut que non-(p et non-p) est vraie dans le modèle (Fp). Comme elle est aussi vraie dans le modèle (Vp) et qu’elle ne contient que p comme proposition atomique, elle est vraie dans tous les modèles et est donc une loi logique.
Les opérateurs logiques « ou » et « si … alors » peuvent être définis à partir de « non » et « et » :
- (p ou q) = non-((non-p) et non-q )
- (si p alors q) = non-(p et non-q)
Avec ces définitions, les règles de déduction pour la disjonction et l’implication peuvent être dérivées à partir de celles pour la conjonction et la négation (règles d’analyse, de synthèse, de suppression de la double-négation et du raisonnement par l’absurde).
Montrons le sur l’exemple de la règle de détachement.
- si p alors q (hyp)
- p (hyp)
- non-(p et non-q)
- °°°°° non-q (hyp)
- °°°°° p et non-q
- °°°°° non-(p et non-q)
- non-non-q
- q
1 et 2 sont les hypothèses principales. 3 est obtenu de 1 par définition. 4 est une hypothèse provisoire. 5 est obtenu par synthèse de 2 et 4 . 6 répète 3. 7 est obtenu de 4, 5 et 6 par le principe du raisonnement par l’absurde. 8 est obtenu de 7 par suppression de la double négation.
Preuve du théorème
[modifier | modifier le wikicode]Le théorème de complétude va être prouvé sous la forme suivante :
- (i) « Si une proposition est absolument vraie alors elle est une vérité anhypothétique. »
Absolument vraie veut dire ici que la proposition est vraie dans tous les modèles.
(i) est obtenu à partir de la formulation initiale du théorème par contraposition.
On se donne un ensemble infini dénombrable, ordonné par les entiers positifs, de propositions atomiques, toutes distinctes, p(1), p(2), p(3)…
Un modèle initial de longueur n contient ou bien Vp(i) ou bien Fp(i), mais pas les deux, pour tout i de 1 à n.
Comme une proposition q ne contient qu’un nombre fini de propositions atomiques, il y a toujours un nombre max(q) tel que p(max(q)) a au moins une occurrence dans q mais p(n) n’a pas d’occurrences dans q pour n>max(q).
Si une proposition q est vraie dans tous les modèles (initiaux) de longueur égale à max(q) alors elle est vraie dans tous les modèles où sa vérité est définie, parce que les propositions p(n) pour n>max(q) n’ont pas d’influence sur elle.
Pour prouver (i), on va d’abord prouver (ii) et (iii) :
- (ii) « Si p est vraie dans le modèle m alors (si h(m) alors p) est une vérité anhypothétique » ;
- (iii) « Si p est fausse dans le modèle m alors (si h(m) alors non-p) est une vérité anhypothétique ».
h(m) est la conjonction de toutes les formules atomiques p(n) telle que Vp(n) est dans m et de toutes les négations des formules atomiques p(n) telles que Fp(n) est dans m.
On va prouver (ii) par induction sur la complexité des formules. Celle-ci est mesurée par le nombre maximal d’opérateurs emboités. Par exemple dans ((non-p) ou (q et r)) , le « ou » et le « non » sont emboités l’un dans l’autre. Mais le « non » et le « et » ne le sont pas. Cette proposition est de complexité 2 parce qu’elle au maximum deux opérateurs emboités.
Soit p(i) une proposition de complexité 0, c’est-à-dire une proposition atomique.
( Si p(i) alors p(i) ) est une vérité anhypothétique, par les règles de répétition et d’abandon d’une hypothèse provisoire. Il en va de même pour (si h alors p(i) ) où h est n’importe quelle conjonction de propositions atomiques ou de leurs négations qui contient p(i) parmi elles. Si p(i) est vraie dans le modèle m, h(m) contient p(i). (ii) est donc prouvée pour les propositions de complexité 0. La preuve de (iii) est identique.
Supposons que (ii) et (iii) soient vraies pour toutes les propositions de complexité au plus égale à n.
Soit p une proposition de complexité n+1. Deux cas sont possibles.
- a) il y a un q tel que p = non-q
- b) il y a r et s tels que p = (r et s)
a)
- Si p est vraie dans le modèle m alors q est fausse dans m. Comme q est de complexité n, l’hypothèse d’induction donne, (si h(m) alors non q) est une vérité anhypothétique. (ii) est donc prouvée dans ce cas.
- Si p est fausse dans le modèle m alors q est vraie dans m. (Si h(m) alors q) est donc une vérité anhypothétique. Le principe du raisonnement par l’absurde permet de prouver que (si q alors non non q) est une vérité anhypothétique. (Si h(m) alors non non q) est donc aussi une vérité anhypothétique. (iii) est donc prouvée dans ce cas.
b)
- Si p est vraie dans le modèle m alors r et s sont toutes les deux vraies dans m. (si h(m) alors r) , et, (si h(m) alors s)) sont donc deux vérités anhypothétiques. Les règles de la déduction naturelle permettent de conclure que (si h(m) alors (r et s)) aussi. (ii) est donc prouvée dans ce cas.
- Si p est fausse dans le modèle m alors l’une au moins de r ou de s est fausse dans m. Supposons que ce soit r. (si h(m) alors non r) est une vérité anhypothétique. De (non r) on peut déduire non(r et s). (iii) est donc prouvée dans ce cas.
Cela termine cette preuve de (ii) et (iii).
Prouvons maintenant (i), le théorème de complétude, par induction sur la longueur des modèles.
Soit (i)(n) l’énoncé.
Si p est vraie dans tous les modèles de longueur n alors p est une vérité anhypothétique.
Prouvons d’abord (i)(1).
Supposons que p est vraie dans tous les modèles de longueur 1, c’est-à-dire les deux modèles (Vp(1)) et (Fp(1)), (si p(1) alors p) , et, (si (non p(1)) alors p) sont deux vérités anhypothétiques. Par la règle de disjonction des hypothèses (si (p(1) ou non p(1)) alors p) est aussi une vérité anhypothétique mais (p(1) ou non p(1)) est une vérité anhypothétique, c’est le principe du tiers-exclu. La règle de détachement suffit alors pour prouver que p est une vérité anhypothétique.
Supposons que (i)(n) soit vrai.
Soit p une proposition vraie dans tous les modèles de longueur n+1.
Soit m un modèle de longueur n. p est vraie dans (m, Vp(n+1)) et dans (m, Fp(n+1)). (si (h(m) et p(n+1)) alors p) , et, (si (h(m) et non p(n+1)) alors p) sont donc des vérités anhypothétiques, d’après (ii). On en conclut que (si h(m) alors p) est une vérité anhypothétique. Comme m un modèle quelconque de longueur n, (i)(n) permet de conclure que p est une vérité anhypothétique. (i)(n+1) est donc vrai.
Cela termine cette preuve du théorème de complétude du calcul des propositions.
Théorème de compacité
[modifier | modifier le wikicode]Il s'agit d'énoncer et de prouver le théorème de compacité du calcul des propositions.
Ce théorème a un rôle très important pour la logique du premier ordre, notamment pour la preuve du théorème de complétude de Gödel.
Sa preuve est basée sur le lemme de König, tout arbre infini à branchement fini a une branche infinie.
Soit A un ensemble infini dénombrable de propositions, c’est-à-dire de formules sans quantificateurs. On suppose que pour chaque sous-ensemble fini de A, il existe un modèle dans lequel toutes ses propositions sont vraies. S’ensuit-il qu’il existe un modèle dans lequel toutes les propositions de A soient vraies ?
Le théorème de compacité répond par l’affirmative.
Si tout sous-ensemble fini d’un ensemble infini dénombrable de propositions est possiblement vrai alors l’ensemble complet est aussi possiblement vrai.
Soit P(n) une suite infinie dénombrable des propositions de A.
Soit p(n) une suite infinie dénombrable des propositions atomiques avec lesquelles les propositions de A sont construites.
Considérons l’arbre construit de la façon suivante.
Il y a un seul nœud initial, vide, de niveau 0.
S’il y a modèle dans lequel p(1) et P(1) sont tous les deux vrais alors p(1) est un nœud de niveau 1 rattaché à l’unique nœud de niveau 0.
S’il y a un modèle dans lequel (non p(1)) et P(1) sont tous deux vrais alors (non p(1)) est aussi un nœud de niveau 1 rattaché à l’unique nœud de niveau 0.
Quand un nœud y est rattaché à un autre x alors x précède y. Cette relation est transitive. Si un nœud x précède y et qu'y précède z alors x précède z.
À un nœud de niveau n, on rattache p(n+1) au niveau n+1 s’il y a un modèle dans lequel p(n+1) , tous ses prédecesseurs, et tous les P(i) pour i de 1 à n+1 sont vrais.
À un nœud de niveau n, on rattache (non p(n+1)) au niveau n+1 s’il y a un modèle dans lequel (non p(n+1)) , tous ses prédecesseurs, et tous les P(i) pour i de 1 à n+1 sont vrais.
On engendre de cette façon un arbre. Comme tout sous-ensemble fini de propositions de A est possiblement vrai, cet arbre peut être indéfiniment poursuivi, il est donc infini, il a un nombre infini de nœuds. Comme chaque nœud ne peut avoir que deux successeurs au plus, il est à branchement fini. D’après le lemme de König il a donc une branche infinie. Cette branche définit un modèle dans lequel tous les P(i) sont vrais.
Cela termine cette preuve du théorème de compacité.
Lemme de König
[modifier | modifier le wikicode]
Tout arbre infini à branchement fini a une branche infinie.
Un arbre est un ensemble d'objets, appelés nœuds, tels qu’il y ait une relation binaire de succession immédiate et un nœud d'origine O qui satisfont aux conditions suivantes.
- O n'est le successeur immédiat d'aucun nœud.
- Tout nœud sauf O est le successeur immédiat d’un unique nœud.
- Tous les nœuds sont des successeurs de O.
Un nœud A est un successeur d’un autre D s'il existe une suite finie de nœuds qui commence par D, qui finit par A, et qui est telle que tout nœud est un successeur immédiat (au sens de la structure de l'arbre) de celui qui le précède dans la suite.
Un arbre est à branchement fini lorsque tous les nœuds n'ont qu'un nombre fini de successeurs immédiats.
Un arbre est infini lorsqu’il a un nombre infini de nœuds.
Une branche d’un arbre est une suite finie ou infinie de nœuds N(i), qui commence par O, et qui est telle que pour tout i, N(i+1) est un successeur immédiat de N(i).
Donnons maintenant la preuve telle qu'elle a été proposée par König.
Un nœud est dit infini s'il a un nombre infini de successeurs.
Supposons qu'on ait un arbre infini d'origine O à branchement fini.
O est infini. Comme O n'a qu'un nombre fini de successeurs immédiats, l'un d'entre eux au moins N(1) est infini, sinon O ne serait pas infini. De même l'un au moins N(2) des successeurs immédiats de N(1) est infini. On définit ainsi un nombre infini de nœuds N(i), pour tout entier positif i, qui ensemble forment une branche infinie.
Notes et références
[modifier | modifier le wikicode]- ↑ Thèse de doctorat, « Sur la complétude du calcul logique », 1929.
