From madore@clipper.ens.fr Fri Jun 16 03:49:11 2000 Article: 2894 of ens.forum.sciences.maths Path: eleves!not-for-mail From: madore@clipper.ens.fr (GroTeXdieck) Newsgroups: ens.forum.sciences.maths Subject: Systeme formel pour faire des maths Date: 16 Jun 2000 01:49:11 GMT Lines: 212 Sender: madore@clipper.ens.fr Message-ID: <8ic12n$5sq$1@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 961120151 6042 129.199.129.1 (16 Jun 2000 01:49:11 GMT) X-Complaints-To: forum@clipper.ens.fr NNTP-Posting-Date: 16 Jun 2000 01:49:11 GMT X-Newsreader: Flrn (0.4.0 - 07/99) X-Start-Date: 16 Jun 2000 00:03:48 GMT X-Mark: BOG Xref: eleves ens.forum.sciences.maths:2894 Bon, à la demande de JML, je vais tenter de décrire un système formel complet qui devrait permettre de formaliser toutes les maths (c'est-à-dire : toute la théorie des ensembles ;-) et dans lequel il n'est peut-être pas entièrement impossible de travailler vraiment (mais je ne garantis rien). Je ne sais pas si j'irai jusqu'au bout dans ce message. On va voir. Pour commencer, je vais préciser que je ne définirai pas les formules syntaxiquement correctes. Les règles doivent produire des formules syntaxiquement correctes, donc on se fout un peu de les définir. Commençons par le calcul propositionnel. T désignera le vrai, F le faux (normalement noté par un T à l'envers mais je n'ai pas ça dans mon petit latin-1), /\ le « et », \/ le « ou », => l'implication et ~ la négation. Ce qu'on manipule, ce sont des séquents, c'est-à-dire des choses de la forme f1,...,fm|-g1,...,gn où f1,...,fm,g1,...,gn sont des formules. Le signe |- (lire « thèse ») est un T couché. m ou n peuvent éventuellement être nuls (notamment, « |- » tout seul est un séquent, qui d'ailleurs n'est pas démontrable, enfin, on l'espère). Mettre des virgules *entre* les formules est peu commode, en fait, si on veut s'en tenir à de la stricte typographie par substitution de chaînes. Convenons donc que plusieurs virgules successives, ainsi que d'éventuelles virgules initiales ou finales, n'ont pas d'importance. Si on est vraiment maniaque, on posera cela comme règles : (a) si on a montré X,,Y|-Z alors on a montré X,Y|-Z ; (b) si on a montré ,X|-Z ou X,|-Z alors on a montré X|-Z ; (c) si on a montré X,Y|-Z alors on a montré X,,Y|-Z. Là-dedans, X, Y et Z représentent des suites finies de formules ou de chaînes vides séparées par des virgules. Pareil à droite du signe |- (interchanger les deux côtés dans ces règles). Il va de soi que je ne considère pas qu'on ait besoin de ces règles mais qu'on peut manipuler des « suites de formules séparer par des virgules », les concaténer et tout ça. L'ordre des f1,...,fm et des g1,...,gn n'importe pas. Si on tient vraiment à manipuler des choses strictement typographiques, il faudra donc prendre les règles suivantes : si Xa,Y1,Xb,Y2,Xc|-Z est démontré alors Xa,Y2,Xb,Y1,Xc|-Z aussi, où Xa,Xb,Xc,Y1,Y2,Z sont des suites de formules séparées par des virgules ; et pareil à droite. Mais je considère qu'on sait manipuler directement des multi-ensembles de formules. Commençons par les règles structurales. Elles vont dire que non seulement on manipule des multi-ensembles de formules mais qu'en fait même la multiplicité ne compte pas ; et d'autre part qu'on peut toujours rajouter des formules à gauche ou à droite du signe thèse (affaiblissement du séquent). C'est ici qu'on voit qu'on ne fait pas de la logique linéaire. Dans ce qui suit, X, Y et variations désignent des multi-ensembles quelconques de formules (ou, si on est maniaque, des suites finies de formules séparées par des virgules) et P, Q et variations désignent des formules individuelles quelconques. (DOUBLEMENT-G) : Si « X,Y,Y|-Z » alors « X,Y|-Z ». (DOUBLEMENT-D) : Si « X|-Y,Z,Z » alors « X|-Y,Z ». (AFFAIBLISSEMENT-G) : Si « X|-Z » alors « X,Y|-Z ». (AFFAIBLISSEMENT-D) : Si « X|-Z » alors « X|-Y,Z ». Passons maintenant aux règles régissant les différents connecteurs. (DÉDUCTION) : Si « X,P|-Q,Y » alors « X|-(P)=>(Q),Y ». (MODUS PONENS) : Si « X1|-P,Y1 » et « X2,Q|-Y2 » alors « X1,X2,(P)=>(Q) |- Y1,Y2 ». (INTRO ET) : Si « X1|-P1,Y1 » à « Xn|-Pn,Yn » alors « X1,...,Xn |- (P1)/\.../\(Pn),Y1,...,Yn ». (ÉLIM ET) : Si « X,P1,...,Pn|-Y » alors « X,(P1)/\.../\(Pn) |- Y ». (INTRO OU) : Si « X|-Pk,Y » alors « X|-(P1)\/...\/(Pn),Y ». (ÉLIM OU) : Si « X,P1|-Y » à « X,Pn|-Y » alors « X,(P1)\/...\/(Pn) |- Y ». (INTRO VRAI) : « |- T ». (ÉLIM VRAI) : Si « X|-Y » alors « X,T|-Y » (cette règle est listée par souci de complétude, mais c'est un cas particulier de la règle d'AFFAIBLISSEMENT-G). (Il n'y a pas de règle INTRO FAUX.) (ÉLIM FAUX) : « X,F |- Y ». (INTRO NON) : Si « X,P |- Y » alors « X |- ~(P),Y ». (ÉLIM NON) : Si « X |- P,Y » alors « X,~(P) |- Y ». Il faut dire qu'il y avait un certain choix dans la formulation des règles. J'aurais pu par exemple, faire les choix suivants pour le ET et le VRAI : (INTRO ET) : Si « X|-P1,Y » à « X|-Pn,Y » alors « X |- (P1)/\.../\(Pn),Y ». (ÉLIM ET) : Si « X,Pk|-Y » alors « X,(P1)/\.../\(Pn) |- Y ». (INTRO VRAI) : « X |- T,Y ». (Pas de règle ÉLIM VRAI.) Et les règles auraient été bien plus symétriques entre la gauche et la droite du signe thèse. Modulo emploi des règles structurales, cela revient au même ; on peut d'ailleurs combiner ces deux formulations comme on veut (précisons que la 2e que j'ai donnée pour le ET et le VRAI est dite « additive » tandis que la première est « multiplicative » ; on peut de même donner une formulation « multiplicative » pour le OU et le FAUX). En logique linéaire cela conduit à des opérations différentes. Mais peu importe : j'ai fait un choix un peu arbitraire. Rajoutons encore deux règles un peu spéciales : (IDENTITÉ) : « P |- P ». (COUPURE) : Si « X1|-P,Y1 » et « X2,P|-Y2 » alors « X1,X2 |- Y1,Y2 ». C'est un fait qu'on peut éliminer la règle de COUPURE. Pourtant, son élimination n'est pas du tout naturelle. Ceci conclut les règles du calcul propositionnel. Passons au calcul des prédicats. Je vais faire du second ordre pur avec abstraction et bêta-réduction. Ce sera le plus commode. Je note @ pour le quantificateur universel, $ pour l'existentiel. La syntaxe sera « @x.P » et « $x.P ». Les variables minuscules désignent des variables d'individus, les variables majuscules des variables d'espèce (ou de premier ordre). La spécification de l'arité des variables d'espèce se fait au niveau de la quantification : donc la notation correcte sera « @P(x1,...,xn).Q » pour quantifier universellement sur les prédicats à n variables (ces x1,...,xn ne jouent absolument aucun rôle par ailleurs et servent juste à compter l'arité : elles ne sont pas liées par la quantification). Je passe sur la définition de variables libres et liées. On sait bien ce que c'est. Les termes d'individus, pour le moment, il n'y a que les variables d'individus. Pour les termes d'espèce, il y a la notation lambda : si « P » est une formule, alors « (^(x1,...,xn).P) » est un terme d'espèce d'arité n (et les variables x1 à xn sont liées dans P dans cette écriture). Il est à noter que j'écrirai « (^x.P) » pour « (^(x).P) » et « P » pour « (^().P) », cette dernière convention me permettant de confondre les formules avec des termes d'espèce d'arité nulle. Pour l'application, si P est un terme d'espèce (par exemple une variable d'espèce ou une expression lambda) d'arité n et x1,...,xn des termes d'individu alors « P(x1,...,xn) » est une formule. Là aussi, je me permets de noter « P » plutôt que « P() » (ce n'est pas du C!) pour le cas d'arité nulle. Pour P une formule, x une variable et t un terme, je note comme d'habitude « P[t/x] » la substitution de x par t dans P. Ceci vaut tant pour des variables d'individus que d'espèce. Notons que ceci est une méta-notation, et ne fait pas partie du langage considéré (de même que les points de suspension plus haut) mais sert juste à écrire les règles. Comme d'habitude, dans la substitution, il faut faire attention à la capture des variables. Tout le monde est censé connaître ça, je ne détaille pas. Voici donc les règles du calcul des prédicats : (BÊTA-RÉDUCTION) : On peut remplacer « (^(x1,...,xn).P)(t1,...,tn) » (avec P une formule, x1,...,xn des variables d'individus et t1,...,tn des termes d'individus) par « P[t1/x1,...,tn/xn] » ; ou inversement. Et ce, dans toute partie d'une formule quelconque d'un séquent. (INTRO UNIV) : Si « X|-P,Y » alors « X|-@x.P,Y » à condition que x ne soit pas libre dans X ou Y ; et ce, que x soit une varibable d'individu ou d'espèce (auquel cas @x doit s'écrire en suivant la variable proprement dite de variables bidon pour indiquer l'arité). (ÉLIM UNIV) : Si « X,P[t/x]|-Y » alors « X,@x.P|-Y » où x est une variable (d'individu ou d'espèce comme ci-dessus), et t un terme (de même ordre). (INTRO EXIST) : Si « X|-P[t/x],Y » alors « X,$x.P|-Y », comme pour ÉLIM UNIV. (ÉLIM EXIST) : Si « X,P|-Y » alors « X,$x.P|-Y » comme pour INTRO UNIV. Voilà. Définissons maintenant l'égalité. Par « (u)=(v) » (u et v étant des termes d'individus) on entend « @P(x).(P(u))=>(P(v)) ». Montrons par exemple que l'égalité est symétrique, autrement dit « |-@x.@y.((x)=(y))=>((y)=(x)) ». Pour cela, je pars de « P(x) |- P(x) » (IDENTITÉ) donc « |-(P(x))=>(P(x)) » (DÉDUCTION). D'autre part, « (P(y))=>(P(x)) |- (P(y))=>(P(x)) » (IDENTITÉ), donc (MODUS PONENS) « ((P(x))=>(P(x)))=>((P(y))=>(P(x))) |- (P(y))=>(P(x)) ». Or j'en déduis, par BÊTA-RÉDUCTION que « ((^t.(P(t))=>(P(x)))(x)) => ((^t.(P(t))=>(P(x)))(y)) |- (P(y))=>(P(x)) ». Par ÉLIM UNIV (sur le terme « (^t.(P(t))=>(P(x))) »), j'ai alors « @Q(t).(Q(x))=>(Q(y)) |- (P(y))=>(P(x)) ». Par INTRO UNIV j'ai donc « @Q(t).(Q(x))=>(Q(y)) |- @P(t).(P(y))=>(P(x)) », ce qui est exactement « (x)=(y) |- (y)=(x) ». Et par DÉDUCTION j'ai « |- ((x)=(y))=>((y)=(x)) » d'où le résultat voulu se déduit par deux applications de INTRO UNIV. Bon, je crois que j'arrête là pour le moment. Je garde la théorie des ensembles proprement dite pour plus tard. From madore@clipper.ens.fr Sat Jun 17 22:04:38 2000 Article: 2907 of ens.forum.sciences.maths Path: eleves!not-for-mail From: madore@clipper.ens.fr (GroTeXdieck) Newsgroups: ens.forum.sciences.maths Subject: Re: Systeme formel pour faire des maths Date: 17 Jun 2000 20:04:38 GMT Lines: 68 Sender: madore@clipper.ens.fr Message-ID: <8iglkm$3ok$1@clipper.ens.fr> References: <8ic12n$5sq$1@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 961272278 3860 129.199.129.1 (17 Jun 2000 20:04:38 GMT) X-Complaints-To: forum@clipper.ens.fr NNTP-Posting-Date: 17 Jun 2000 20:04:38 GMT X-Newsreader: Flrn (0.4.0 - 07/99) X-Start-Date: 17 Jun 2000 18:39:02 GMT X-Mark: BOG Xref: eleves ens.forum.sciences.maths:2907 Voici la suite tant attendue. Pour définir la théorie des ensembles, on va donner des « axiomes ». Ces axiomes sont des propositions. La manière dont on utilise un axiome A, c'est en rajoutant une règle (d'« anti-introduction ») aux règles de manipulation des séquents, à savoir : si « X,A|-Y » alors « X|-Y ». On a un certain nombre de choix possibles pour les axiomes. Je propose de profiter du fait qu'on est en logique du second ordre et donc d'imiter plus Gödel-Bernays que Zermelo-Fraenkel. J'enrichis le langage de trois constructions : premièrement, si x et y sont des termes d'individus alors « (x):(y) » sera une proposition (lire : « x élément de y ») ; deuxièmement, si P est un terme d'espèce d'arité 1 (prédicat à une variable) alors « *P » sera un terme d'_individu_ (moralement, la classe des x tels que P(x)) ; et enfin, si x est un terme d'individu alors « %x » sera une formule (moralement, « x est un ensemble »). Les axiomes sont alors : (ENSEMBLE) : @t.@x.((t):(x))=>(%t) (CONTENU) : @P(t).@x.((x):(*P))=>(P(x)) (EXHAUSTIVITÉ) : @P(t).@x.((P(x))/\(%x))=>((x):(*P)) Convenons à présent de noter (x)<(y) pour « @t.((t):(x))=>((t):(y)) ». (EXTENSION) : @x.@y.(((x)<(y))/\((y)<(x)))=>((x)=(y)) (VIDE) : %*(^t.F) On convient de noter 0 pour « *(^t.F) ». (PAIRE) : @x.@y.((%x)/\(%y))=>(%*(^t.((t)=(x))\/((t)=(y)))) (PARTIES) : @x.(%x)=>(%*(^y.(y)<(x))) (UNION-REMPLACEMENT) : @P(t).@x.((%x) /\ (@u.((u):(x))=>(%*(^v.P(u,v))))) => (%*(^v.$u.((u):(x)) /\ (P(u,v)))) On convient de noter +x pour « *(^t.((t):(x))\/((t)=(x))) ». Il peut être utile, à ce point, de noter le théorème « |- @x.(%x)=>(%+x) ». (INFINI) : %*(^n.@o.(((0):(o))/\(@x.((x):(o))=>((+x):(o)))) => ((n):(o))) (moralement : la classe de tous les n (appelés « entiers naturels ») qui appartiennent à tous les ensembles o contenant 0 et stables par l'opération +, est un ensemble). (CHOIX) : @x.((@u.((u):(x))=>($t.(t):(u))) /\ (@u.@v.(((u):(x))/\((v):(x))/\($t.((t):(u))/\((t):(v))))=>((u)=(v)))) => ($y.@u.((u):(x))=>($t.((t):(y))/\((t):(u)) /\ (@w.(((w):(y))/\((w):(u)))=>((w)=(t))))) (si vous n'arrivez pas à lire ceci, c'est assez normal ; si je ne me suis pas gourré, ça dit que si x est une classe dont tous les éléments sont non vides et deux à deux disjoints, alors il existe une classe y qui intersecte tout élément u de y en un unique élément t). (RÉGULARITÉ) : @x.(@y.(@t.((t):(y))=>((t):(x))) => ((y):(x))) => (@t.((t):(x))) (formulation assez élégante : si une classe x contient tout ensemble y dont elle contient tous les éléments t, alors x est la classe universelle). Et voilà. Si je ne me suis pas complètement gourré, quand on a lu ce post et le post précédent, moralement, on connaît toutes les mathématiques.