From madore@news.ens.fr Wed Nov 10 23:01:19 1999 Article: 1232 of ens.forum.sciences.maths Path: eleves!not-for-mail From: madore@news.ens.fr (GroTeXdieck) Newsgroups: ens.forum.sciences.maths Subject: Re: Logique du premier ordre Date: 10 Nov 1999 22:01:19 GMT Lines: 190 Sender: madore@clipper.ens.fr Message-ID: <80cpvf$2kv$1@clipper.ens.fr> References: <809k8b$sfu$1@clipper.ens.fr> <809o13$8hg$1@clipper.ens.fr> <80a0a6$s56$1@clipper.ens.fr> <80a2d4$sff$2@clipper.ens.fr> NNTP-Posting-Host: clipper.ens.fr Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: clipper.ens.fr 942271279 2719 129.199.129.1 (10 Nov 1999 22:01:19 GMT) X-Complaints-To: forum@clipper.ens.fr NNTP-Posting-Date: 10 Nov 1999 22:01:19 GMT X-Newsreader: Flrn (0.4.0 - 07/99) X-Wisdom-Of-The-Day: In my opinion, karma should help avoid the essence of magic. X-Mark: BOG Xref: eleves ens.forum.sciences.maths:1232 Bon, on récapitule. Par un « sftf » (lire : spectre fini d'une théorie finie) j'entends une partie de N qui peut s'écrire comme l'ensemble des n pour lesquels il existe un modèle de cardinal n de P, P étant une proposition formulée dans un certain langage (qu'on peut supposer fini, et qu'on peut supposer ne contenant que des relations) du calcul des prédicats du premier ordre (avec une seule sorte de variables, sans conjonctions ni disjonctions infinies, et en logique classique - bref, ce qu'il y a de plus bête). Voyons quelles opérations on sait faire sur les sftf. * Le vide et N sont des sftf (les propositions Faux et Vrai conviennent). * Si U et V sont des sftf alors leur intersection et leur union sont des sftf. Pour le voir, il suffit de prendre des langages disjoints (on se limitera à des symboles de relations, ce qu'on peut faire) et considérer la conjonction, ou la disjonction, des deux propositions. * Tout singleton est un sftf. En effet, si k est un naturel, on peut considérer la théorie ayant k constantes c1...cn (qu'on peut éliminer si on veut mais peu importe) et un axiome qui dit que tout x est égal à c1 ou est égal à c2 ou... ou est égal à cn. * Si U et V sont des sftf alors U+V (l'ensemble des m+n avec m dans U et n dans V) est un sftf. Pour le voir, on prend des propositions P et Q définissant U et V (comme toujours, avec des langages consistant en seulement des symboles de relations, je ne le répéterai plus), on considère l'union des deux langages à laquelle on rajoute encore un symbole de relation unaire, R (lire « est dans le premier cas »). On prend P' formée de P avec tous les quantificateurs restreints à R (i.e. on remplace tous les (pour tout x) par des (pour tout x tel que R(x)) et tous les (il existe x) par des (il existe x tel que R(x))) et Q' formée de Q avec tous les quantificateurs restreints à (non R). Alors la conjonction de P' et Q' a pour modèles des unions disjoints formées d'un modèle de P et d'un modèle de Q, R étant la fonction caractéristique du premier. Donc son sftf est U+V. * Si U et V sont des sftf alors U*V (l'ensemble des mn avec m dans U et n dans V) est un sftf. Pour le voir, on prend P et Q comme ci-dessus. On considère le langage formé de l'union disjointe des langages de P et Q, à laquelle on rajoute deux symboles de relations binaires, <1> et <2>. Pour P', on prend P dans laquelle toutes les égalités sont remplacées par des <1>, et pour Q' on prend Q avec les égalités remplacées par des <2>. On considère la propositions qui est la conjonction de P', Q' et des axiomes suivants pour <1> et <2> : (a)  est réflexive, symétrique et transitive pour i=1,2 ; (b) x=y ssi x<1>y et x<2>y ; (c) pour tous x et y il existe z (unique d'après (b)) tel que x<1>z et y<2>z. Les modèles de cette propositions sont les produits cartésiens d'un modèle de P et d'un modèle de Q donc on a ce qu'on voulait sur les sftf. * Si U est un sftf alors U^k (l'ensemble des n^k avec n dans U) est un sftf pour k quelconque. Pour cela, on fait comme pour le produit de k copies de U (entre autres on aura des relations binaires pour i=1...k), et on rajoute un symbole de fonction unaire T (qu'on pourra transformer en relation si on veut). On met un axiome qui dit que T itérée k fois vaut l'identité. De plus, pour chaque relation Ri (i=1...k, correspondant à la relation R dans le langage du sftf initial U), y compris , on postule Ri(x) ssi R(i+1)(T(x)) (je dis ça pour une relation unaire, adapter de manière évidente pour les relations r-naires), le i+1 étant à prendre modulo k. Ceci implique que T est un isomorphisme entre les différentes composantes : les modèles sont les puissances cartésiennes k-ièmes d'un modèle pour la proposition initiale, et on a ce qu'on voulait sur les sftf. => À ce point, on a montré que si P est un polynôme à coefficients naturels et U un sftf alors P(U) est un sftf (*). Il faut cependant noter que tous ces points (exceptés les deux ou trois premiers) consistaient à _grandir_ des sftf (dans le sens de l'ordre sur N pas de l'inclusion). Peut-on les diminuer aussi ? Là, c'est nettement plus dur. J'ai cependant obtenu : * Si U est un sftf alors U-k (i.e. l'ensemble des n tels que n+k est dans U) en est un pour tout k. Pour cela, on procède en deux étapes. Dans une première étape, on rajoute au langage k symboles de constantes, c1 à ck. On prend une proposition P dont U est un sftf, et on modifie ses quantificateurs : chaque (pour tout x R(x)) est remplacé par (pour tout x R(x) ET R(c1) ET ... ET R(ck)), et chaque (il existe x R(x)) par (il existe x R(x) OU R(c1) OU ... OU R(ck)). À ce niveau-là, les modèles de la théorie sont les modèles de P pointés k fois, donc le sftf est simplement l'intersection de U avec [k;+oo[. Rien de bien palpitant, et ce qu'on a fait sur les quantificateurs est inutile. Mais à la deuxième étape, on fait quelque chose d'horriblement astucieux : on retire les constantes c1...ck. Alors la proposition P' n'a plus de sens. On lui en redonne un en rajoutant virtuellement les constantes, c'est-à-dire que si R est une relation binaire du langage initial, et que R(x,c1) (par exemple) intervient dans la formule, on rajoute R(x,c1) comme une relation unaire (le c1 fait juste partie de la notation). À ce moment-là, les modèles de la proposition P' sont des modèles de P privés de k éléments arbitraires, et on a ce qu'on voulait sur les sftf. En tout cas le principe est de stocker k éléments virtuellement en introduisant des relations supplémentaires ad hoc. [Une note au sujet de l'égalité, dans ce qui précède : l'égalité est une relation comme une autre - donc il faudra rajouter des relations unaires x=ci (de la variable x) et des relations nullaires (variables propositionnelles) ci=cj. Il faut bien sûr faire subir le traitement aux axiomes de l'égalité. On pourra objecter que ceux-ci sont en nombre infini puisqu'il y a la réflexivité, la symétrie, la transitivité et le fait que si x=y alors R(x)<=>R(y) pour tout prédicat R ; mais en fait on peut remplacer cette assertion par un nombre fini d'assertions qui traduisent le fait que l'égalité est compatible à tous les symboles de relation du langage. Donc ça marche.] * Si U est un sftf alors U/k (i.e. l'ensemble des n tels que kn est dans U) est un sftf. On introduit dans un premier temps k symboles de fonctions unaires [i] (que j'écrirai en notation postfixe), remplacer chaque (il existe x R(x)) par (il existe x R(x[1]) OU R(x[2]) OU ... OU R(x[k])) et chaque (pour tout x R(x)) par (pour tout x R(x[1]) ET ... ET R(x[k])). Ensuite on vire ces k fonctions comme dans le cas précédent (chaque relation r-naire se démultiplie en n^r relations r-naires). Donc le principe c'est d'utiliser un élément pour en stocker k d'un coup. * Si U est un sftf alors {n : n^k est dans U} est un sftf. Pour cela, on introduit une fonction k-naire supplémentaire, notée <...> (avec des cornets, quoi). J'explique le cas k=2, le cas général se traitant de même. On modifie de nouveau les quantificateurs : chaque (pour tout x R(x)) se transforme en (pour tout x pour tout y R()), et chaque (il existe x R(x)) se transforme en (il existe x il existe y R()). Ensuite on éliminer cette nouvelle fonction en doublant le nombre de variables de chaque relation. Le principe est donc d'utiliser des couples virtuels. Passons au commentaire moral. Primo, il est clair que l'ensemble des sftf est *BEAUCOUP* plus gros que le plus petit ensemble de parties de n clos par toutes les opérations que j'ai indiquées : je suis très loin d'avoir énuméré toutes les opérations qu'on pouvait faire avec les sftf. Secundo, il y a deux opérations que je ne sais pas traiter : + Si U est un sftf, est-il vrai que N\U (le complémentaire) est un sftf ? + Si U et V sont des sftf, est-il vrai que U-V (l'ensemble des m-n avec m dans U et n dans V) est un sftf ? Quel est le problème ? Pour le premier point, si on regarde les choses en logique du *second* ordre, ce qu'on fait est essentiellement existentiel : dire que n est dans U revient à dire qu'IL EXISTE des symboles de relations (divers) tels que (bla, bla). Il n'est pas surprenant qu'une telle chose passe mal au complémentaire. Pour le second, l'ennui vient du cas où m-n serait petit avec n très grand ; parce qu'alors on est en train d'essayer de contrôler une structure avec m (très grand) éléments et une autre avec n (également très grand) éléments et les représenter avec une structure ayant m-n éléments. Cela est peu plausible quand on étudie les méthodes que j'ai utilisées pour diminuer les sftf, car à chaque fois la « compression » utilisée (simulation d'un modèle virtuel ayant un certain nombre d'éléments par un autre en ayant moins, au prix d'ajout de nouvelles relations ou d'ajout de variables aux relations) était à fibres finies (exercice : qu'est-ce que ça veut dire ?). Je vois mal comment on pourrait éliminer ces contraintes. Possibilité : pour résoudre le problème, on le modifie. On remplace la notion de sftf par celle de sftf', essentiellement cela revient à permettre des soustractions de modèles. Comment ? Si on aime ça, on peut considérer des logiques à deux sortes (ou k sortes, k>1, cela revient au même) et on considère, pour former les spectres, le cardinal des objets d'une seule sorte. Si on n'aime pas les logiques à sortes, on impose que le langage contienne un prédicat unaire distingué R, et on compte non pas le cardinal du modèle mais le cardinal de {x : R(x)}. Attention ! Le modèle tout entier (toutes les sortes si on travaille avec des sortes) doit être fini, sinon c'est trop facile (j'allais dire : « on prend Peano, on écrit x