Francis Bessi\`ere Un nouveau regard sur les fondements

TL;DR

The paper explores a translative approach to foundational mathematics aiming to establish consistency through finitist methods, potentially circumventing G"odel's incompleteness results for traditional deductive systems.

Contribution

It proposes a novel translative theory for mathematics that can be shown consistent using finitist methods, challenging traditional views on mathematical foundations.

Findings

Introduces a translative theory for foundations

Shows potential for finitist consistency proof

Addresses G"odel's incompleteness limitations

Abstract

We draw attention to a manuscript submitted to the HAL Open Archives by Francis Bessi\`ere, where he tries to base mathematics on a translative theory that could be shown consistant using only finitist methods, thus bypassing the impossibility shown by G\"odel for deductive theories, such as [ZF], for example.

Equations

$$A^B=\Theta \text{si}{a}_K=1,A^B=\Psi \text{sinon}.$$

$$(\exists x)D(x)\text{et}(\forall y)D(y)⟹y=x.$$

$$B^{/K}\equiv \mathbf{ET}(R(T_1,T_2,\dots ,T_K)|T_1,T_2,\dots ,T_K\in C_K)$$

$$(\forall a,b)((\forall x)(x\in a⟺x\in b))⟹(P(a)⟺P(b))$$

Full text

Francis BessiÈre

un regard original sur les fondements

Labib Haddad

120 rue de Charonne, 75011 Paris, France

labib.haddad@wanadoo.fr

We draw attention to a manuscript submitted to the HAL Open Archives by Francis Bessi re, where he tries to base mathematics on a translative theory that could be shown consistant using only finitist methods, thus bypassing the impossibility shown by G del for deductive theories, such as [ZF], for example.

**On voudrait attirer l’attention sur un manuscrit d pos  aux archives ouvertes HAL par Francis Bessi re o  il essaie de fonder les math matiques   l’aide d’une th orie traductive dont on pourrait  tablir la coh rence [autrement dit, la non contradiction] par des m thodes finitistes, contournant ainsi l’impossibilit  d montr e par G del pour les th ories d ductives, telles que [ZF], par exemple.

$*$  $*$  $*$

Francis Bessi re (1931-2015) est un ancien  l ve de l’École normale sup rieure de la rue d’Ulm, promotion 1950. Agr g  de physique en 1954, il entre au service des Études  conomiques g n rales d’EDF (Électricit  de France) en 1957 puis, apr s un passage au Centre pour la recherche  conomique et ses applications en 1969, il revient finir sa carri re   EDF, jusqu’en 1991.

Je l’ai connu vers l’ ge de 19 ans, superficiellement​; je n’appr ciais pas ses choix politiques du moment. Apr s la sortie de l’École, nous nous sommes perdus de vue. Il  tait physicien, moi, math maticien. Je ne me doutais gu re qu’il s’ tait int ress  de pr s au probl me des fondements. C’est seulement apr s sa mort que j’ai appris l’existence du manuscrit (inachev ) suivant qu’il avait laiss  sur le site d’archives ouvertes HAL :

Ne peut-on pas contourner l’impasse identifi e par G del et prouver la consistance des math matiques usuelles ? 2013. $<$hal-00812912$>$.

Le manuscrit comporte 75 pages. Voici les r sum s qu’il en fait, en français et en anglais.

R sum

Le point de d part de ce travail est le fait que les c l bres th or mes de G del concernent sp cifiquement les «syst mes hypoth tico-d ductifs» - que je pr f re appeler des «th ories d ductives». Il devrait ainsi  tre possible de contourner l’impasse rep r e par G del en consid rant d’autres types de th ories (sous r serve qu’elles ne soient pas  quivalentes   des th ories d ductives). Je d finirai donc des «th ories traductives» puis des «th ories asymptotiques». Le chapitre 1 et les treize «M mos» qui le compl tent en posent les bases et pr sentent (M mo 4) une th orie M dont les Annexes A, B et C prouvent qu’elle est bien  quivalente aux «Maths usuelles», i.e.   [ZF] plus l’axiome de fondation (AF) - mais sans qu’il soit utile de prendre en compte l’axiome du choix (AC). En s’appuyant sur la notion intuitive de «dictif» (M mo 10), les chapitres 2 et 3 introduisent alors des concepts que je crois nouveaux et tout- -fait intuitifs : les «superblocs» de lettres li es, et les dictifs « utiles» et «sub-transitifs». Le chapitre 4 s’attaque   une famille de th ories traductives qui sont toutes consistantes et aboutissant   M. Le chapitre 5, non r dig , esp rait bien achever ce travail, mais mon  ge et d’autres facteurs incontr lables m’ont emp ch  d’y parvenir :   d’autres chercheurs de prendre le relais …

Summary.

The departure point of this study is the fact that the well known G del’s theorems apply specifically to “hypothetico-deductive systems” - which I will rather call “deductive theories”. Then it may be possible to turn around the dead-end identified by G del, by trying to find other kinds of theories (with the condition that they shall not be equivalent to a deductive theory). So I will define “translative theories” and “asymptotic theories”. Chapter 1 and the thirteen following “Memos” lay down their foundations and present (Memo 4) the theory M : the Annexes A, B and C will prove that this theory is equivalent to “usual Mathematics”, i.e. [ZF] plus the axiom of foundation (AF) - but with no necessity to take into account the axiom of choice (AC). Using always the intuitive notion of “dictives” (Memo 10), the chapters 2 and 3 will introduce some new concepts: the “super-blocks” of bounded letters, and the “useful” and “sub-transitive” dictives. The chapter 4 deals with a family of translative theories which are all consistent and leading to M. The unwritten chapter 5 hoped to finish the present work, but my age and other uncontrollable factors prevented me from a real success​: I hope that other researchers will take over … (sic)

$*$  $*$  $*$

Dans les lignes qui suivent, on s’efforce de donner un aperçu, le plus clair, et sobre, possible du travail de Bessi re. Pour la clart , l’expos  est fait d’une succession de petits paragraphes, assez courts. Pour la sobri t , on a  lagu  un grand nombre de d finitions, de notations, de d tails, de remarques et de commentaires qui ne semblaient pas essentiels. Cet aperçu n’est qu’un simple guide pour la lecture du texte lui-m me, foisonnant et volumineux, du manuscrit.

Deux difficult s se pr sentent : le tr s grand nombre de d finitions introduites et les multiples renvois, crois s, qui s’entrem lent, entre 4 chapitres, 13 m mos et 3 annexes. L’une des principales r f rences est, bien  videmment, le petit livre pr cieux de Jean-Louis KRIVINE, Th orie axiomatique des ensembles, P.U.F, Paris, 1969.

{$\looparrowright$  Il faut prendre garde,  galement,   ceci. Souvent, certains mots apparaissent dans le texte avant leurs d finitions lesquelles ne sont pas toujours faciles   rep rer dans la suite du manuscrit (ainsi, par exemple, de constante ou atomique.}

Bessi re cherche    tablir par des m todes finitistes que les math matiques habituelles [il dit usuelles] ont une th orie coh rente [il dit logiquement consistante]. On ne peut pas le faire avec une th orie d ductive classique (qui serait r cursive et engloberait l’arithm tique) car elle tomberait sous le couperet du th or me de G del. En contraste, aux th ories d ductives, commun ment appel es hypoth tico-d ductives, il oppose les th ories traductives qu’il introduit comme on va essayer de l’expliquer.

On commence par d finir des langages ${\sf A,B,C,D,E,F,}$ de plus en plus riches, et des th ories qui leur sont associ es. La th orie $\sf A$ est la plus squelettique. La th orie $\sf B$ est la th orie bool enne. La th orie $\sf C$ est la th orie de la logique classique bivalente. La th orie $\sf D$ est celle des dictifs [mot nouveau forg  par Bessi re].

Tout au long de son texte, Bessi re distingue soigneusement les entiers intuitifs des entiers formels. Les entiers intuitifs seront d sign s par des majuscules $H,K,N,\dots$. On s’en sert   l’ cole  l mentaire lorsque l’on compte les  l ments d’une liste (intuitive) finie. En regard, une suite est index e par des entiers formels.

Langage logique

Un langage logique est un langage formel ayant $\Psi$ et $\implies$ parmi ses symboles et qui les utilise comme dans le langage $\sf E$ d crit ci-dessous.

Transcription et traduction

Soient $\sf R$ et $\sf S$ des langages formels. Une transcription de $\sf S$ dans $\sf R$ est une proc dure intuitive finie qui,   chaque  nonc  $E$ de $\sf S$, associe des  nonc s $E^{R}$ de $\sf R$, des transcriptions :ces  nonc s $E^{R}$ sont, en quelque sorte, des codes de l’ nonc  $E$ dans le langage $\sf R$. Une traduction de $\sf S$ dans $\sf R$ est une transcription univoque :   chaque  nonc  $E$ de $\sf S$, elle associe un unique  nonc  $E^{R}$ de $\sf R$​; autrement dit, c’est une application de $\sf S$ dans $\sf R$, au sens habituel.

On dira qu’une traduction de $\sf S$ dans $\sf R$ est fid le lorsque $\sf R$ et $\sf S$ sont des langages logiques, que la traduction de $\Psi$ est $\Psi$ et la traduction de $E\implies F$ est $E^{R}\implies F^{R}$.

Th orie

Une th orie est un langage logique o  l’on a d fini les seuls  nonc s auxquels on s’int resse et, parmi eux, les  nonc s clos. À chaque  nonc  $E$ est associ  sa n gation $\neg E$. Ce langage est accompagn  d’une m thode de s lection d finie dans un m talangage convenable : les  nonc s ainsi s lectionn s parmi les  nonc s clos sont appel s th or mes de la th orie.

Th ories traductives

Toute traduction d’un langage logique $\sf S$ dans une th orie de r f rence $\sf R$ donn e d finit une th orie traductive dont la r gle est la suivante : un  nonc  T est un th or me de $\sf S$ si et seulement si sa traduction est un th or me de $\sf R$.

Th orie $\sf A$

Le langage de la th orie $\sf A$ est r duit aux seuls symboles $\Psi$ et $\Theta$. Ses seuls  nonc s sont $\Psi$ et $\Theta$, et son seul th or me est l’ nonc  $\Theta$ dont la n gation est $\Psi$.

[Bessi re justifie son choix de $\Psi$ et de $\Theta$ en faisant remarquer que $\Psi$ est l’initiale du grec antique $\psi\epsilon\nu\delta o\varsigma$ (lire : pseudos), qui signifie «faux, mensonger», et $\Theta$ est l’initiale de $\theta\epsilon\omega\rho\eta\mu\alpha$, «th or me» bien s r.]

Th orie $\sf B$

Le langage de la th orie bool enne $\sf B$ est le langage logique le plus simple, celui dont les seuls symboles sont $\Psi$ et $\implies,$ sans aucun  nonc  atomique. Tous les  nonc s de $\sf B$ sont d clar s clos. La r gle d’inf rence et trois sch mas d’axiomes de logique  l mentaire d finissent sur $\sf B$ une th orie d ductive et logique, la Th orie bool enne.

L’inf rence

Si $A$ et $A\implies C$ sont des th or mes, alors $C$ est un th or me.

Les trois sch mas d’axiomes

Ce sont

$\neg\neg F\implies F$,

$D\implies(E\implies D)$,

$(A\implies(B\implies C))\implies((A\implies B)\implies(A\implies C))$.

Th orie $\sf C$

Le langage $\sf C$ poss de trois symboles : $\Psi$, $\implies$, $\lambda$. Ses seuls  nonc s atomiques, appel s variables, sont produits par la r gle suivante : $\lambda\Psi$ est une variable et, si $v$ est une variable, alors $\lambda v$ est une variable. Les variables forment ainsi une liste (intuitive) infinie. Sur ce langage, on d finit la Th orie logique $\sf C$ par la r gle d’inf rence et les trois sch mas d’axiomes pr c dents. Les th or mes de cette th orie sont, par d finition, les sch mas logiques. On sait (depuis longtemps) que cette th orie est coh rente, compl te et d cidable.

Th orie $\sf D$

Le langage $\sf D$ poss de 5 symboles : $\Psi,\implies,\delta,\varsigma,\in.$ On y distingue les dictifs et les  nonc s, d finis par les r gles suivantes : le symbole $\varsigma$ est un dictif et, si (Dictif) est un dictif, alors $\delta$(Dictif) est un dictif. De m me, $\Psi$ est un  nonc  ainsi que $\implies$(Enonc )(Enonc ) et $\in$(Dictif)(Dictif). Pour chaque entier intuitif $K$, on d signe par $D_{K}$ le dictif $\delta\delta\delta\dots\delta\delta\delta\varsigma$ form  par un $\varsigma$ pr c d  $K$ fois par $\delta$. Les dictifs se pr sentent ainsi comme une liste index e par les entiers intuitifs.

On d signe encore par $\sf D$, la th orie traductive associ e   ce langage, ayant la th orie $\sf B$ comme r f rence, munie de la traduction binaire suivante. Soit $A$ un  nonc  de la forme $\in D_{K}D_{N}$. On  crit l’entier $N$ sous sa forme binaire, $a_{0}a_{1}a_{2}\dots$ [par exemple, l’entier 6 s’ crit $011$, sous forme binaire]. On prend

[TABLE]

Cette traduction est fid le, de sorte que la th orie $\sf D$ est  galement coh rente, compl te et d cidable.

Interpr tation

On dit que le dictif $X$ est un  l ment du dictif $Z$ lorsque $\epsilon XZ$ est un th or me. Tout dictif $Z$ s’interpr te ainsi comme un ensemble intuitif fini de dictifs, le dictif $\varsigma=D_{0}$  tant interpr t  comme l’ensemble vide. R ciproquement, tout ensemble intuitif fini de dictifs est l’interpr tation du dictif $D_{N}$ o  $N$ est la somme des $2^{K}$ pour lesquels $\in D_{K}D_{N}$ est un th or me. Cela donne un contenu pr cis aux notions intuitives de partie d’un dictif, de successeur, d’inclusison, d’ galit , de r union, d’intersection, etc, pour les dictifs.

{$\looparrowright$  Disons que cette interpr tion est calqu e sur un mod le classique, bien connu, de la th orie des ensembles finis}

En particulier, on introduit une liste (intuitive) illimit e, utile dans les prochains d veloppements, la liste des $P_{N}$, en prenant $P_{0}=\varsigma$ puis, par r currence, $P_{N+1}=$ ensemble des parties de $P_{N}$.

Le langage $\sf E$

Son alphabet poss de 6 symboles : $\Psi,\implies,\lambda,\varsigma,\in,\forall.$ C’est un langage pour les  nonc s des math matiques habituelles.

On y d finit deux types de «textes» : les litt mes et les  nonc s.

R gles de formation. Les seuls litt mes et  nonc s sont ceux que l’on obtient par les deux r gles de formations suivantes.

(1) Les litt mes. Le texte $\lambda\varsigma$ est un litt me et, si $L$ est un litt me, alors $\lambda L$ est un litt me.

La hauteur H d’un litt me est le nombre de ses $\lambda$, de sorte que l’on a toujours $H\geqslant 1$.

(2) Les  nonc s. Le symbole $\Psi$ est un  nonc  et, si $A$, $B$, $C$ sont des  nonc s, et $L$, $M$ sont des litt mes, alors , $\forall A$, $\in LM$, $\implies BC$ sont des  nonc s.

$\forall A$ est un  nonc  universalis ; sa port e est le sous-texte $A$.

$\in LM$ est une appartenance; sa port e est le sous-texte $LM$.

$\implies BC$ est une implication; sa port e est le sous-texte $BC$.

Comme c’est l’usage, au lieu de $\in LM$, on peut  crire $L\in M$. De m me, au lieu de $\implies BC$, on peut  crire $B\implies C$.

Trascription du langage $\sf E$

Un saturateur est une occurrence de $\Psi$ ou d’un litt me. Tout  nonc  finit donc par un saturateur, (un $\Psi$ ou un $\varsigma$).

Un signe est une occurrence de $\forall,\implies,\in$, ou d’un saturateur.

Par d finition, la profondeur du premier signe d’un  nonc  est nulle; elle augmente de 1 apr s chaque $\forall$; elle diminue apr s chaque saturateur $s$ du nombre de sous- nonc s universalis s que ce saturateur $s$ compl te.

Dire qu’un signe d pend d’un autre signe donn  veut dire qu’il est dans sa port e.

Un signe de profondeur $P$ d pend d’une unique occurrence d’un ‘$\forall$’ de profondeur $K$, pour chacun des $K$ tels que $0\leqslant K<P$. Au total, il d pend ainsi de $P$ signes ‘$\forall$’.

Le niveau $N$ d’un litt me est  gal, par d finition,   sa hauteur $H$ moins sa profondeur $P.$

Ainsi, «lorsque N est positif, on dit que ce litt me est une occurrence du litt ral positif de niveau $N$. Lorsque N est n gatif ou nul, on dit que c’est une occurrence du **litt ral li **   l’unique ‘$\forall$’ de profondeur $-N$ dont il d pend. Ce litt ral li  est donc identifi  par la position de ce ‘$\forall$’ dans l’ nonc  consid r . De plus, chaque signe ‘$\forall$’ introduit un litt ral li  (qui peut  tre : “vide”, ou encore : “inoccup ”, i.e. sans aucune occurrence effective).»

Comme il est d’usage, $(\exists x)E$ abr ge $\neg(\forall x)\neg E$.

Les lettres des math matiques habituelles transcrivent les litt raux, pas les litt mes. On dit qu’une lettre est libre lorsqu’elle transcrit un litt ral positif. On dit qu’elle est li e lorsqu’elle transcrit un litt ral li .

Un  nonc  clos est un  nonc  dont toute lettre libre est une constante.

Les objets math matiques

On dit que l’ nonc  $D(x)$ d finit l’objet $x$ lorsque $x$ est sa seule lettre libre et que l’ nonc  suivant est un th or me (d’existence et d’unicit ) :

[TABLE]

Lorsque l’on fait de $D(a)$ un axiome explicite, on appelle constante toute lettre non li e qui figure dans un tel axiome.

Pr nexe et d nexe

On sait qu’un  nonc  peut se pr senter sous plusieurs formes  quivalentes. Parmi elles, il y a les formes pr nexes celles o  tous les quantificateurs, $\forall$ et $\exists$, sont regroup s   gauche, en d but d’ nonc . Ici, un ** nonc  maxi-d nect ** est, par d fintion, un  nonc   crit avec des quantificateurs $\forall$ dont chacun est repouss  le plus   droite possible. Pour plus de d tails, on se reportera au manuscrit de Bessi re.

La th orie d ductive $\sf M$

On d signe, habituellement, par [ZF] la th orie d ductive classique de Zermelo-Fraenkel, par [ZFC] la th orie [ZF] augment e de l’axiome du choix et par (AF) l’axiome de fondation [1, p. 50]. On ne peut pas  tablir la coh rence de la th orie [ZF] par des moyens finitistes : c’est l’un des r sultats de G del. On sait, cependant, que les trois th ories, [ZF], [ZFC] et [ZF] + (AF) sont  quicoh rentes, autrement dit, si l’une d’elles est coh rente, les deux autres le sont aussi.

Par commodit , Bessi re convient de s’en tenir   la th orie [ZF] + (AF) comme repr sentant des math matiques habituelles. D’autres choix sont possibles et pourraient tout aussi bien faire l’affaire. Il introduit, dans le langage $\sf E$, une th orie d ductive $\sf M$, ad hoc, puis il  tablit, m ticuleusement, qu’elle est  quivalente   la th orie [ZF] + (AF) : tout th or me de l’une est un th or me de l’autre. Pour faire court, nous omettrons tous les d tails de la d monstration en renvoyant au manuscrit lui-m me, en particulier, aux trois Annexes A, B, C.

Le langage $\sf F$

Il a pour ambition de rassembler les deux langages $\sf D$ et $\sf E$ en un langage unique. L’alphabet du langage $\sf F$ poss de ainsi les 7 symboles $\Psi,\implies,\delta,\lambda,\varsigma,\in,\forall.$ Les deux langages $\sf D$ et $\sf E$ sont des sous-langages de $\sf F$. Par d finition, les substantifs de $\sf F$ sont les litt mes et les dictifs. On y distingue deux types d’ nonc s atomiques : les  nonc s universalis s et les appartenances, respectivement de la forme $\forall$(Énonc ) et $\in$(Substantif)(Substantif). On dit qu’un  nonc  est clos lorsqu’il est sans litt raux positifs.

À chaque dictif non vide $Z$, on associe une traduction fid le de $\sf F$ dans $\sf F$, comme suit. [Voir M mo 12 B et chapitre 4.1]. Si un  nonc  atomique autonome $A$ est une appartenance, on prend pour $A^{Z}$ l’ nonc  $A$ lui-m me. Si $A$ est de la forme $(\forall x_{1}x_{2}\dots x_{H})R(x_{1},x_{2},\dots,x_{H})$ o  $R(x_{1},x_{2},\dots,x_{H})$ ne commence plus par $\forall$, on prend pour $A^{Z}$ la conjonction des $N^{K}$  nonc s que l’on obtient en substituant, de toutes les mani res possibles,   chaque $x_{H},H=1,2,\dots K$, un  l ment de $Z$, ce que l’on pourra  crire en bref :

$A^{Z}\equiv{\bf ET}(R(T_{1},T_{2},\dots,T_{K})\ |\ T_{1},T_{2},\dots,T_{K}\in Z)$

o  ET d signe une conjonction (globale), comme pour le symbole

de r union $\bigcup$.

On d signe par $\sf F^{C}$ le sous-langage des  nonc s clos : il englobe $\sf D$ et les  nonc s strictement clos de $\sf E$, autrement dit les  nonc s de $\sf E$ o  aucun litt ral positif ne figure. On d signe par $\sf F^{D}$ le sous-langage de $\sf F^{C}$ form  des  nonc s maxi-d nect s,

Th orie asymptotique

Sur un langage $\sf L$, on se donne une liste illimit e, $\sf L_{1}$, $\sf L_{2},\dots,\sf L_{R},\dots$, de th ories ayant les m mes  nonc s clos. On d signe par $\sf L^{*}$ la th orie (dite asymptotique) d finie sur le langage $\sf L$ en d cidant qu’un  nonc  est un th or me de $\sf L^{*}$ si et seulement si c’est un th or me de chacune des th ories $\sf L_{R}$   partir d’un certain rang donn  $R$. Bien entendu, il suffit que chacune des th ories $\sf L_{R}$ de la liste soit coh rente pour que la th orie $\sf L^{*}$ le soit.

Bessi re se pose la question suivante sans y r pondre, laissant   chacun le soin de le faire (pour lui-m me) : le recours   des th ories asymptotiques peut-il  tre encore consid r  comme «finitiste»?

Le chapitre 4

C’est le plus long des quatre chapitres r dig s. Il comporte 11 pages; il est dense et tr s technique. Il est consacr   un type de traductions de $\sf F$ dans $\sf D$ qui sont donc des th ories traductives. Apr s avoir introduit un type de traductions fid les de $\sf F^{D}$ dans $\sf D$, on les prolonge en traductions de $\sf F$ dans $\sf D$ puis on  tudie les conditions qui permettent aux th ories traductives ainsi d finies sur $\sf F$ de v rifier, chaque fois, certains axiomes et sch mas d’axiomes «math matiques» de la th orie $\sf M$. Ce chapitre comporte 5 longs paragraphes.

Disons quelques mots de chacun d’eux.

Un type de traductions fid les de $\sf F^{D}$ dans $\sf D$

On se donne, une fois pour toutes, une liste de dictifs, $C_{1},C_{2},\dots$ que l’on appelle les conteneurs. Par exemple, la liste des $P_{N}$ d finis ci-dessus en m me temps que le langage $\sf D$, et on introduit une fonction intuitive $\mu$ qui d finit une liste strictement croissante d’entiers $\mu K$. On suppose que $\varsigma$ appartient   chacun des $C_{K}$ et que chaque $C_{K}$ est contenu dans $C_{\mu K}$.

À Chaque  nonc  $B$ de $\sf F^{D}$ de la forme $(\forall t_{1}t_{2}\dots t_{N})R(t_{1}t_{2}\dots t_{N})$ o  $R$ n’est pas universalis  et $N\geqslant 1$, on choisit une entier intuitif positif $K$ et on traduit $B$ par

[TABLE]

comme on l’a fait ci-dessus pour le dictif $Z$, dans le paragraphe qui

introduit le langage $\sf F$.

Les traductions  tudi es vont appliquer une formule analogue   la formule (1)   chaque sous- nonc  universalis  d’un  nonc  de $\sf F^{D}$, mais en modifiant le choix de l’indice $K$ suivant le sous-  nonc  qu’on consid re.

À chaque indice $H$, on asscocie une ** tape** de traduction de $\sf F^{D}$ dans lui-m me que l’on d signe par ∙H et qui laisse invariants, en particulier, les  nonc s de $\sf D$. À chaque valeur de $K$, on associe la traduction de $\sf F^{D}$ dans $\sf D$, compos e des  tapes d’indices $K,\mu K,\mu\mu K,\dots$ jusqu’  obtenir un  nonc  de $\sf D$, ce qui arrive n cessairement, comme on le montre. Cette traduction est fid le. On la d signe par [K. Toute th orie d finie sur $\sf F^{D}$ par une traduction de ce type est donc coh rente, compl te et d cidable.

Prolongement vers $\sf F^{C}$ et vers $\sf F$

On prend une th orie $\sf R$ engendr e sur $\sf F^{D}$ par une traduction du type [K d finie ci-dessus. On la prolonge d’abord vers $\sf F^{C}$, en composant avec la traduction d de $\sf F^{C}$ vers $\sf F^{D}$ appel e maxi-d nexion que l’on d finit, au pr alable [dans 2.3]. Cette traduction de $\sf F^{C}$ dans $\sf D$ est fid le. On la d signe par d[k.

On prolonge encore vers $\sf F$ en composant d[K avec une traduction u de $\sf F$ dans $\sf F^{C}$ [voir le d tail dans le manuscrit]. On obtient une th orie traductive que l’on d signe encore par $\sf F$. Bien que la traduction u ne soit pas fid le, on montre que la th orie $\sf F$ est coh rente, compl te et d cidable.

On montre aussi que la r gle d’inf rence est valable dans cette nouvelle th orie $\sf F$ et que les trois sch mas d’axiomes de la th orie $\sf B$ sont encore des sch mas d’axiomes de $\sf F$.

Le sch ma d’ galit

Dans la th orie $\sf M$, figure le sch ma d’axiome d’ galit  sous la forme suivante

[TABLE]

On dit qu’un dictif $X$ est sub-transitif lorsque $A$ et $B$  tant des  l ments de $X$, l’ galit  $A\cap X=B\cap X$ implique $A=B$.

Il suffit de supposer que tous les conteneurs $C_{K}$ sont sub-transitifs pour que l’on ait la propri t  importante suivante. Un  nonc  du type (2) dont tous les dictifs appartiennent   $C_{K}$ est un th or me de la th orie traductive que ud[K d finit sur $\sf F$.

Dictifs-tests,  l ments visibles et virtuels

Ce paragraphe est techniquement tr s laborieux. Il est tr s difficile d’en donner un aperçu. Il pr pare les d monstrations du paragraphe suivant, le dernier.

Un exemple : l’axiome de fondation

On y montre, en particulier ceci. Moyennant certaines conditions sur les conteneurs, l’axiome de fondation (AF) est un th or me de toute th orie traductive sur $\sf F$ d finie par une traduction ud[K.

$*$  $*$  $*$

Bessi re projetait de conclure son travail par un chapitre 5 qu’il a renonc    r diger apr s la mort de son  pouse, Marie-Jeanne,  tant lui-m me d j  atteint d’une d g n rescence maculaire   l’œil droit.

L’essai de Bessi re m rite d’ tre repris, prolong  et achev .

Bibliographie

[1] Jean-Louis KRIVINE, Th orie axiomatique des ensembles, P.U.F, Paris, 1969.