théorème de Beth

GG

Bonjour,

je suis intrigué par le théorème de Beth dont la preuve me semble hautement non-constructive. Pour prendre un cas concret, je considère l'arithmétique de Peano avec addition, soit les axiomes standard augmentés d'un signe fonctionnel "+" ainsi que les deux axiomes qui définissent l'addition :

x + 0 = x
x + y⁺ = (x + y)⁺.

Avec un nouveau signe * et les deux axiome supplémentaires

x * 0 = x
x * y⁺ = (x * y)⁺,

on montre facilement par récurrence que x + y = x * y. Le théorème de Beth affirme donc, si j'ai bien compris, que le signe "+" est définissable, i.e. qu'il existe un prédicat E(x,y,z) où ne figure pas le signe "+" tel que

E(x,y,z) <=> z = x + y soit un théorème.

Question : est-on capable d'écrire explicitement un tel prédicat ?

@l

Salut à tous,

le théorème de Beth repose sur le théorème de compacité et est donc complètement non-constructif dans le cas général.

Sinon dans le cas qui t'intéresse ici, quel est le langage de départ? Il ne doit évidemment pas contenir $+$.

Si par exemple ce langage de départ contient uniquement $0$ et la fonction successeur $s$ (comme tu le suggères), alors l'addition n'est pas implicitement définissable.
En effet, on peut considérer $E=\{0\}\times \N\cup \R^*_+\times \Z$.

Le $0$ de $E$ est $(0,0)$; la fonction successeur est $s(r,x)=(r,x+1)$.

On peut définir sur $E$ tout d'abord l'opération $+$ suivante:
$$(q,x)+(r,y)=(q+r,x+y)$$
Cette opération satisfait les axiomes que tu as introduit et même d'autres comme la régularité.

Posons maintenant l'opération $*$ suivante:
$$(q,x)*(r,y)=(q\#r,x+y)$$
où $\#$ est une loi de monoïde régulier sur $\R^*_+$ dont le neutre est $0$ (et évidemment $\#$ est différente de $+$); on construit facilement une telle loi grâce à une bijection croissante de $\R$ stabilisant $0$.
La loi $\#$ satisfait les axiomes introduits mais est différente de $+$.

En fait, quand tu dis "on montre facilement par récurrence que x + y = x * y", tu sous-entend que les axiomes de récurrence peuvent utiliser $+$ ce qui n'est pas le cas.

Ainsi $+$ n'est pas implicitement définissable par $0$ et la fonction successeur.

@l

GG

@l&gt; Non, je pensais bien au langage de départ avec 0, s, +.
Je ne suis pas trop sûr d'avoir bien saisi cette notion de "définissable implicitement". Avec un exemple encore plus simple, voici comment je la comprends :

axiomes de la théorie des groupes :

(xy)z = x(yz)
x.1 = 1.x = x
x.I(x) = I(x).x = 1

si j'introduis un I' avec "copie" des axiomes, i.e. en plus x.I'(x) = I'(x).x = 1, je démontre I'(x) = I(x), c'était ça pour moi "I est définissable implicitement". Et il l'est explicitement puisque y = I(x) <=> xy = 1 est un th. Bien entendu, on ne peut pas supprimer le troisième axiome, par contre on peut éliminer le symbole I.
Je parle de la même situation avec Peano.

@l

Si le $+$ est déjà présent dans le langage de base, alors il est forcément définissable dans ce langage.

Le théorème de Beth dit que si $L$ est un langage, si $P$ est un prédicat et si $T$ est une théorie dans le langage $L'=L\cup \{P\}$ tels que toute $L$-structure

-soit ne peut pas être étendue en une $L'$-structure,

-soit ne peut être étendue en une $L'$-structure que d'une seule façon

alors il existe une $L$-formule qui définit $P$.

@l

GG

aïe, je sentais bien que tout ça n'était pas clair dans ma tête
J'espère que je n'abuserai pas trop de ta patience, car je sais d'expérience que dans ce genre de situation confuse, je suis toujours très lent à comprendre

Trois premiers points :

a) es-tu d'accord qu'il manque dans ta phrase deux fois "...en une L'-structure" qui soit un modèle de T ?

b) es-tu d'accord que alors il existe une L-formule qui définit P veut dire précisément "alors il existe une L-formule E telle que P <=> E soit un théorème de T, soit encore "P est explicitement définissable dans T " ?

c) es-tu d'accord que le th peut être adapté pour un signe fonctionnel f avec "f explicitement définissable dans T " = "il existe une L-formule E telle que x = f(...) <=> E(..., x) soit un théorème de T " ?

J'attends ta confirmation, sinon ce que je veux dire maintenant n'a peut-être pas de sens.

@l

a) tu as entièrement raison: il faut toujours retourner 7 fois son clavier dans sa main avant d'écrire :-)

b) Ok aussi

c) Itou

Sinon ne t'inquiète pas, tu n'abuses absolument pas; en plus, ça me permet de me replonger dans mes fondamentaux de théorie des modèles.

@l

GG

d'accord, merci, me voilà rassuré ... provisoirement

dernier point : es-tu d'accord que l'hypothèse du th. de Beth, sémantique, équivaut via le th. de complétude, à la condition syntaxique : si T' est la théorie dans le langage L U {P'} où P' est un signe de prédicat n'appartenant pas à L' (ou dans le langage L U {f'} où f' est un signe fonctionnel n'appartenant pas à L'), obtenue à partir de T en substituant P' à P dans toutes les formules (f' à f), alors P(...) <=> P'(...) est un théorème de T U T' ? (f(...) = f'(...))

Si oui, je reprends mon exemple :

L = {0,s}, L' = {0,s,+},

axiomes de T :

s(x) <> 0
...
schéma de récurrence
x + 0 = x
x + s(y) = s(x + y)

axiomes de T' :

s(x) <> 0
...
schéma de récurrence (où figure * à la place de +)
x * 0 = x
x * s(y) = s(x * y)


Th. dans T U T' : x + y = x * y,

application du th. de Beth : il existe un L-prédicat E(x,y,z) tel que x + y = z <=> E(x,y,z) est un th. de T.

toujours d'accord ?

Si oui, je meurs d'envie de voir (un procédé de construction de) ce prédicat
Si non, je vais me coucher.

@l

Je suis d'accord avec toi sur le début.

Cependant ensuite, le problème est dans ton "théorème" qui affirme que:
"dans T U T' : x + y = x * y"

Je dis que c'est faux: c'est ce que prouve mon premier message. Comme je te le disais, tu as choisi comme langage de base $0$ et $s$. Or dans ce langage $+$ n'est pas implicitement définissable (la preuve est mon premier message).

@l

GG

oui, c'est bien là que je ne comprends plus. Le langage de base c'est L = {0,s}. Mais le langage de T, et tu l'as confirmé, c'est L' = {0,s,+}, et les axiomes de T comprennent les axiomes de récurrence. Quant au langage de T U T', c'est L" = {0,s,+,*}, et x + y = x * y est bien un théorème de T U T'. Il me semble donc que la construction de ton premier message (entre parenthèses, je crois qu'il y a un Z qui devrait être un N) ne saurait être un modèle de T U T' et n'est pas un contre-exemple de l'hypothèse du th. de Beth.

Qu'est-ce qui cloche et qui m'échappe ?

gb

La théorie T du langage {0,s,+) contient
- les axiomes de s
- les axiomes de +
-le schéma de récurrence, + étant admis.

La théorie T' du langage {0,s,*) contient
- les axiomes de s
- les axiomes de *
- le schéma de récurrence, * étant admis.

Lorsque tu envisages la théorie T U T', tu disposes de tout ce qui précède, mais tu ne peux pas introduire x+y=x*y dans un schéma de récurrence.

GG

ah oui, gb, voilà ce qui me crevait les yeux ! Bon, je digère, revois ma copie, et reviendrai sur mon interrogation initiale et qui reste frustrée( un exemple de théorie simple où un signe est définissable mais sans construction explicitée). Merci @l et gb.

GG

@l&gt; ok, j'avais mal compris la définition de ton ensemble E (bien qu'ayant saisi l'idée de tes additions), j'avais stupidement lu {0} x (N U R^*₊) x Z Donc à partir d'une interprétation de {0,s} tu as construit deux modèles distincts de T. Mais comment fais-tu pour vérifier que tous les axiomes de récurrence (contenant 0,s,+) sont valides dans E ?

GG

@l&gt; excuse-moi d'insister, mais j'aimerais vraiment comprendre. Comment montrer que les axiomes de récurrence sont vérifiés pour ton interprétation ? (je viens seulement de découvrir que l'arithmétique avec 0,s,+ s'appelait arithmétique de Presburger). Ne peut-on pas d'ailleurs se passer des réels et prendre comme domaine plus simple {0}xN U N^*xZ ? Question encore plus basique : dans l'arithmétique de Peano, donc avec seulement 0 et s, je ne connais l'existence d'un modèle non-standard qu'indirectement par l'argument classique de compacité avec rajout d'une constante et d'axiomes. Je ne sais même pas si, par exemple, M = {0}xN U {1}xZ est un modèle ou non. Est-ce le cas ? Je n'arrive pas à prouver que toute partie de M définie par un prédicat à une variable libre, stable par s et contenant 0 coïncide avec M.

Désolé pour ces considérations de débutant

gb

Histoire de faire remonter le fil, une réponse qui n'en est pas une, mais dire des bêtises incite les lecteurs à venir les corriger...

On ordonne le modèle $ E=[\{0\}\times \mathbb{N}) \cup (\mathbb{R}^*_+\times \mathbb{Z})$ lexicographiquement, noté $\prec$.

On interprète les atomes, et on montre que l'on ne peut définir ainsi que les intervalles $[a,b]$ et $[a,\to[$ de $(E,\prec)$.

Face à un prédicat, on le met sous forme normale disjonctive, et on montre que l'on ne peut définir que des réunions d'intervalles.

On montre que la seule réunion d'intervalles, non vide et stable par successeur, est $E$.

GG

gb, quand tu dis "on interprète les atomes", tu veux dire que tu considères les parties de E et de E² qui satisfont les formules atomiques (x=0^+..+, x=y^+..+, etc) ou bien que tu associes une nouvelle constante à chaque élément de E ? (en principe un "atome" c'est un élément minimal de E\{plus petit élément} ?). Et pour les formes normales disjonctives, tu remplaces les quantificateurs par des sommes, produits, infinis ?

GG

je ne sais pas si c'est ton idée, mais je me rends compte que si on met une formule P(x) sous forme prénexe disjonctive, on peut éliminer de proche en proche les quantificateurs et aboutir à une formule P'(x) équivalente soit toujours vraie, soit toujours fausse, soit vraie pour un nombre fini de successeurs de 0, ce qui rend valide l'axiome de récurrence correspondant.

Il semblerait donc que les modèles de l'arithm de Peano (0,s) soient tous, à isomorphisme près, de la forme ({u}xN) U (ExZ) avec u hors de E, E quelconque (vide pour le modèle standard), 0 = (u,0), s(x,n) = (x,n+1).

gb

J'avais fait une réponse sur de très vagues souvenirs, espérant qu'un connaisseur vienne apporter ses corrections.
Je n'ai hélas plus touché à ce genre de problèmes depuis l'ENS, ce qui remonte à ...

Il faut effectivement mettre la formule P(x) sous forme prénexe disjonctive. L'interpréter dans le modèle c'est déterminer le sous-ensemble des valeurs de $x$ qui la satisfont.
Pour ce faire on commence par interpréter chaque sous-formule atomique, de la forme t=t' où t et t' sont deux termes du langage, interpréter ensuite les conjonctions de ces sous-formules atomiques puis les disjonctions de ces conjonctions étant purement technique et sans grand intérêt.

Le but du jeu est de montrer que les parties définissables par une formule P(x), c'est-à-dire dont les éléments sont exactement ceux qui satisfont P(x) sont
— soit vide ;
— soit E ;
— soit admettent un plus grand élément pour l'ordre lexicographique sur E.

L'axiome de récurrence est là pour éliminer le premier et le troisième cas, et conclure sur le deuxième.

Ce n'est pas très rigoureux, je m'en excuse.

GG

non, non, tu n'as pas à t'excuser, ça me convient très bien Ce sont les idées qui m'intéressent, et ça me conforte que c'est bien une piste à suivre. Avec quelques exemples, je me suis convaincu que ça doit marcher. Maintenant ce qui m'inquiète, c'est l'arithm de Presburger, donc avec en plus l'addition. Là, je ne vois plus comment faire la réduction. @l m'a parlé du modèle ( {0} x N ) U ( R^*₊ x Z ) avec (a,m) + (b,n) = (a+b,m+n), sans mentionner les axiomes de récurrence, comme si leur vérification ne posait pas de problème. Je me demande si ( {0} x N ) U ( M x Z ) où M est un monoïde quelconque régulier et vérifiant juste x + y = 0 => x = y = 0 est encore un modèle .. et si ainsi on les a tous ?

L'étape d'après, c'est l'introduction de la multiplication et l'arithmétique habituelle. Il me semble que si N est un sous-monoïde de M, on peut introduire (a,m).(b,n) = (ab+an+bm,mn). Mais les axiomes de récurrence sont-ils encore vérifiés ? Et enfin, peut-on simultanément construire une deuxième multiplication, ce qui montrerait que la multiplication n'est pas définissable ? (par curiosité parce que je crois qu'on le montre autrement simplement, mais indirectement).

gb

Au-delà des propriétés les plus simples des modèles non-standards de l'arithmétique, je ne sais plus.
Il me semble que les modèles dénombrables sont tous de la forme indiquée, avec le monoïde M dénombrable bien évidemment ; pour les cardinaux supérieurs, je ne sais pas.
Pour la multiplication, tu vas avoir un problème :
lorsque tu écris (a,m).(b,n) = (ab+an+bm,mn), comment calcules-tu ab+an+bm dans le monoïde ? Il semble que deux lois soient nécessaires sur M pour envisager deux lois sur ({0}xN) U (M*xZ).

GG

oui, bien sûr, je pensais à deux lois, avec distributivité.