AC implique tiers exclus
Dans le fil de Monsieur Pomme de Terre, j'ai signalé une amusante preuve du tiers exclus en utilisant l'axiome du choix, et l'axiome d'extensionnalité.
Jean-Louis Krivine vient de me dire que lors de ses recherches il avait obtenu "en passant" une preuve qu'on peut se passer de l'axiome d'extensionnalité pour prouver le tiers exclus sans utiliser la moindre hypothèse d'extensionnalité (il y a une classe plus grande que tout ensemble d'ensembles vides par exemple).
Essayez de prouver le tiers exclus avec l'axiome du choix et des axiomes intuitifs sur les ensembles, mais ne supposez à aucun moment que 2 ensembles contenant les mêmes éléments sont égaux (ont les mêmes propriétés).
P est une phrase quelconque: voici la preuve "connue" avec l'extensionnalité:
E:=l'ensemble des u tels que u=0 ou (u=1 et P)
F:=l'ensemble des v tels que u=1 ou (u=0 et P)
Vous obtenez facilement que P implique E=F (ont les mêmes éléments)
Soit a dans E et b dans F choisis par une fonction choix, donc tels que si E=F alors a=b.
et donc que P implique a=b
Dans l'autre sens, si a=b, vous arrivez facilement à en déduire P.
Le fait que a=b ou non(a=b) n'a pas besoin d'être supposé car il découle du fait que a est dans E et b dans F et du fait que 0 est différent de 1.
Il s'ensuit que P ou non(P)
On n'utilise très nettement l'extensionnalité: en disant que si E et F contiennent les mêmes éléments, alors la fonction choix les considère comme égaux et leur associe le même élément.
Si le "ou" vous gène (ce qui peut se comprendre en logique intuitionniste) <a href="http://www.logique.jussieu.fr/~chalons/z022008/potpourriclass.php">ce lien vous mène vers une preuve</a> entièrement sans "ou" j'ai juste recopié l'argument en enlevant le "ou".
Rappel de logique intuitionniste (évitez le mot "ou"):
*non(A):=A implique tout (par définition).
*tout implique ce que vous voulez
*(A et
implique C équivaut à A implique (B implique C)
*Pour tout x R(x) implique R(ce que vous voulez comme objet)
Vous n'avez droit à aucun autre axiome. Pour démontrer un truc, vous écrivez un raisonnement normal et tout est "axiome" personnel que vous rajoutez (et votre vraie conclusion finale doit le mentionner).
Les "donc":
si vous avez prouvé A et si vous avez prouvé B vous avez le droit d'inférer "donc A et B"
si vous avez prouvé A et aussi prouvé "A implique B" vous avez le droit d'inférer "donc B"
Si vous avez prouvé B en utilisant A comme hypothèse (ou axiome) personnel, vous avez le droit de dire "je viens de te prouver A implique B sans utiliser A"
Si vous avez prouvé R(w) sans rien supposer, ni vos axiomes, ni dans vos hypothèses à propos de w, vous pouvez dire "donc pour tout x R(x)"
Pas de raisonnement par cas, etc...
Essayez de prouver le tiers exclus avec l'axiome du choix et des axiomes intuitifs sur les ensembles, mais ne supposez à aucun moment que 2 ensembles contenant les mêmes éléments sont égaux (ont les même propriétés).
Le tiers exclus dit que si non(P implique tout) alors P.
Si vous voulez préciser les axiomes de théorie des ensembles autorisés, vous pouvez consulter <a href="http://www.pps.jussieu.fr/~krivine/articles/zf_epsi.pdf">la définition de ZF epsilon de Jean-Louis</a>
Remarque: je ne connais pas (encore) la solution, et Jean-Louis ne s'en rappelle plus précisément, mais il parait que c'est un argument assez court et simple.
Jean-Louis Krivine vient de me dire que lors de ses recherches il avait obtenu "en passant" une preuve qu'on peut se passer de l'axiome d'extensionnalité pour prouver le tiers exclus sans utiliser la moindre hypothèse d'extensionnalité (il y a une classe plus grande que tout ensemble d'ensembles vides par exemple).
Essayez de prouver le tiers exclus avec l'axiome du choix et des axiomes intuitifs sur les ensembles, mais ne supposez à aucun moment que 2 ensembles contenant les mêmes éléments sont égaux (ont les mêmes propriétés).
P est une phrase quelconque: voici la preuve "connue" avec l'extensionnalité:
E:=l'ensemble des u tels que u=0 ou (u=1 et P)
F:=l'ensemble des v tels que u=1 ou (u=0 et P)
Vous obtenez facilement que P implique E=F (ont les mêmes éléments)
Soit a dans E et b dans F choisis par une fonction choix, donc tels que si E=F alors a=b.
et donc que P implique a=b
Dans l'autre sens, si a=b, vous arrivez facilement à en déduire P.
Le fait que a=b ou non(a=b) n'a pas besoin d'être supposé car il découle du fait que a est dans E et b dans F et du fait que 0 est différent de 1.
Il s'ensuit que P ou non(P)
On n'utilise très nettement l'extensionnalité: en disant que si E et F contiennent les mêmes éléments, alors la fonction choix les considère comme égaux et leur associe le même élément.
Si le "ou" vous gène (ce qui peut se comprendre en logique intuitionniste) <a href="http://www.logique.jussieu.fr/~chalons/z022008/potpourriclass.php">ce lien vous mène vers une preuve</a> entièrement sans "ou" j'ai juste recopié l'argument en enlevant le "ou".
Rappel de logique intuitionniste (évitez le mot "ou"):
*non(A):=A implique tout (par définition).
*tout implique ce que vous voulez
*(A et
implique C équivaut à A implique (B implique C)*Pour tout x R(x) implique R(ce que vous voulez comme objet)
Vous n'avez droit à aucun autre axiome. Pour démontrer un truc, vous écrivez un raisonnement normal et tout est "axiome" personnel que vous rajoutez (et votre vraie conclusion finale doit le mentionner).
Les "donc":
si vous avez prouvé A et si vous avez prouvé B vous avez le droit d'inférer "donc A et B"
si vous avez prouvé A et aussi prouvé "A implique B" vous avez le droit d'inférer "donc B"
Si vous avez prouvé B en utilisant A comme hypothèse (ou axiome) personnel, vous avez le droit de dire "je viens de te prouver A implique B sans utiliser A"
Si vous avez prouvé R(w) sans rien supposer, ni vos axiomes, ni dans vos hypothèses à propos de w, vous pouvez dire "donc pour tout x R(x)"
Pas de raisonnement par cas, etc...
Essayez de prouver le tiers exclus avec l'axiome du choix et des axiomes intuitifs sur les ensembles, mais ne supposez à aucun moment que 2 ensembles contenant les mêmes éléments sont égaux (ont les même propriétés).
Le tiers exclus dit que si non(P implique tout) alors P.
Si vous voulez préciser les axiomes de théorie des ensembles autorisés, vous pouvez consulter <a href="http://www.pps.jussieu.fr/~krivine/articles/zf_epsi.pdf">la définition de ZF epsilon de Jean-Louis</a>
Remarque: je ne connais pas (encore) la solution, et Jean-Louis ne s'en rappelle plus précisément, mais il parait que c'est un argument assez court et simple.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Il existe aussi une preuve de Diaconescu beaucoup plus sophistiquée. Cette dernière marche pour n'importe quel topos élémentaire. Deux questions (non indépendantes).
Si l'on adapte la preuve de Diaconescu, obtient-on celle de Krivine (que je ne connais pas) ? Remarque : la preuve est sophistiquée, mais il se pourrait que quand on l'adapte aux ensembles, on obtienne un argument "assez court et simple" ; donc, a priori, il est possible que la réponse soit "oui".
La preuve de Diaconescu utilise-t-elle l'extensionnalité ?
Dans le livre de Mac Lane et Moerdijk, on trouve la preuve de Diaconescu en exercice, livre que j'ai chez moi, mais j'avoue n'avoir jamais fait cet exercice. Il me faudrait un peu de temps pour arriver à faire cet exercice et à comprendre s'il utilise ou non l'extensionalité, temps que je n'ai pas trop en ce moment, même si j'ai très envie de regarder cela un jour, et même dès que je pourrai.
Il y a aussi une preuve du même résultat dans le livre de Lambek et Scott. Les auteurs précisent que la preuve est différente. Donc mêmes questions que ci-dessus pour cette preuve.
Et toi, Christophe, connais-tu ces deux preuves ? Saurais-tu si elles utilisent aussi l'extensionalité ?
Bin, étant donné que Christophe ne la connait pas non plus, et que Krivine himself ne s'en souvient pas, je crois qu'on n'aura jamais la réponse à cette question
En ce qui me concerne, j'ai renoncé à comprendre les posts de Christophe en première lecture.
Je suis donc dubitatif sur la phrase qui suit : J'ai cru comprendre que la preuve mentionnée par Christophe (et donc réputée comme "faisant usage intensif de l'extensionalité") était justement celle de Diaconescu. Bon, comme je viens de le dire, je me trompe sans doute.
Pour moi, la preuve de Diaconescu est la suivante : pour P une proposition, on considère l'ensemble {x,y} tel que x=y si et seulement si P. On considère alors f : {0,1} -> {x,y} définie par f(0)=x et f(1)=y. Ainsi, f est surjective. On utilise alors la forme suivante de l'axiome du choix : toute surjection admet une section. On prend alors une section s de f, on a s(x)=s(y) ou s(x)<>s(y) donc P ou non P.
Daniel, est-ce aussi ce que tu as en tête ?
Christophe, cette preuve est-elle bien (une reformulation de) celle que tu as en tête ? Si oui, peux-tu préciser nous préciser à Daniel et moi en quel sens elle fait usage de l'extensionalité (formulée ainsi) ? Si non, peux-tu me réexpliquer ta preuve ? (je m'engage à faire un max d'efforts pour comprendre, mais il faudra y mettre du tien aussi)
Je profite que tu fasses cette remarque pour te poser trois questions qui s'éloignent du sujet :
1) D'après ce que tu dis, j'ai l'impression que tu es capable d'"isoler" la propriété d'extensionalité dans un topos, c'est à dire de décrire un topos comme un "semi-topos" extensionnel. Est-ce le cas ? J'en suis foncièrement incapable : pour moi, un topos, c'est extensionnel, et la preuve de l'extensionalité (à mes pauvres yeux de béotien) met en oeuvre la plupart des axiomes d'un topos.
2) (suite du 1) Je conjecture depuis un certain temps (mais c'est peut-être un pur délire) qu'un topos est exactement un dogme cartésiennement clos dans lequel on a l'axiome des choix uniques (ce qui permettrait d'isoler l'extensionnalité puisque c'est un axiome à part dans la définition des dogmes). Je vois que tu as le livre de Lambek et Scott, donc tu sais ce qu'est un dogme. Que penses-tu de cette conjecture ("pur délire", "probable", "pas d'avis", "mais voyons la réponse est dans le livre") ?
3) Puisque tu parles de cet exercice 16, et toujours pour rester sur les choix uniques, as-tu fait l'exercice 11 ?
Je regarderai demain (je n'ai pas le livre à la maison) voir si je peux dire quelque chose de pas trop bête là-dessus.
Tilt!! Maintenant que j'ai la preuve de Lambek et Scott sous les yeux, je comprends enfin le message de cc. J'étais bien dans l'erreur en pensant qu'il décrivait la preuve de Diaconescu, en fait il décrivait la preuve de Lambek!
Effectivement, il me semble que cette preuve utilise l'extensionnalité : dans le livre de Lambek, page 162, pour conclure que si p alors α(p) = β(p) (et sans doute en d'autres occurrences).
NB : je ne prétends pas avoir compris cette preuve.
Pour que cc qui n'a probablement pas le bouquin puisse confirmer, je prendrai peut-être un moment ce soir pour recopier cette preuve (en la particularisant aux ensembles, en pointant les utilisations de l'extensionalité et en reprenant les notations de cc), mais je suis profondément convaincu que c'est bien la même.
En ce qui concerne la preuve de Diaconescu, elle utilise apparemment l'extensionnalité des prédicats (qui dans les ensembles est acquis suite à l'axiome d'extensionalité). Enfin, si on en croit les gens :
http://www.mathematik.tu-darmstadt.de/~berg/papers/diaco.pdf
http://en.wikipedia.org/wiki/Constructivism_(mathematics)
http://publish.uwo.ca/~jbell/AC in foundations.pdf
Il est certain que j'apprécierais qu'on m'explique tout ça simplement.
Pour moi, quand j'ai lu la preuve donnée par Christophe, j'ai vu où intervenait l'axiome d'extensionnalité. Par contre, je n'ai pas vu où elle interviendrait dans celle donnée par le Barbant raseur et je ne sais pas si celle-ci est la preuve que l'on trouve dans le Mac Lane - Moerdjik quand on la particularise aux ensembles : il faudrait prendre le temps de regarder.
> "D'après ce que tu dis, j'ai l'impression que tu es capable d'"isoler" la propriété d'extensionalité dans un topos, c'est à dire de décrire un topos comme un "semi-topos" extensionnel. Est-ce le cas ? J'en suis foncièrement incapable : pour moi, un topos, c'est extensionnel, et la preuve de l'extensionalité (à mes pauvres yeux de béotien) met en oeuvre la plupart des axiomes d'un topos."
Non, je n'en suis pas capable. Mais ça ne me semble pas contredire le fait d'être capable de savoir si une preuve donnée pour un topos élémentaire, une fois particularisée aux ensembles, utilise l'axiome d'extensionnalité ou non. Il me semble que c'est comme si on avait :
- une preuve de (A et
- et une preuve de (C et D) => E.
On peut être capable de savoir si l'hypothèse C a été utilisée dans la seconde preuve sans (s)avoir (si) B => D .
C'est tout pour l'instant, désolé.
(J'utilise le mot "ou", sinon c'est assez pénible)
Soit P un énoncé clos ou non.
le signe ":=" est utilisé comme abréviation de "est par définition".
U:=ensemble des x tels que x=0 ou (x=1 etP)
V:=ensemble des x tels que x=1 ou (x=0 etP)
U,V sont non vides.
Soit f une fonction choix telle que f(U) est dans U et f(V) est dans V
Dans la suite, a:=f(U) et b:=f(V).
En particulier a est dans U et b est dans V
Lemme1: a=0 ou a=1
Lemme2: b=0 ou b=1
Ca provient du fait que (a=1 et P) entraine a=1. (idem pour b)
Lemme3: si P alors U et V contiennent les mêmes éléments
(évident?)
Lemme4: P entraine a=b
(Grace à l'axiome d'extensionnalité: si P alors U=V et alors a=b)
Soit Q l'énoncé: "si a=0 alors (P ou nonP)"
Lemme5: si b=0 alors Q
Lemme6: si b=1 alors Q
(exercices)
Les lemmes 2;5 et 6 donnent:
Lemme7: si a=0 alors (P ou nonP)
De la même manière:
Lemme8: si a=1 alors (P ou nonP)
Les lemmes 1;7 et 8 donnent
Théorème: P ou nonP
Remarque:
Le mot "ou" rend moins pur la pratique "intuitionniste" (et peut donner l'impression de raisonnements par cas). J'ai mis une preuve pure sur mon site (lien ci-dessus), mais moins lisible.
Vous pouvez considérer comme définition du mot "ou" la suivante:
Pour tout X si (A--->X) et (B--->X) alors X
qui utilise la logique du 2nd ordre.
Pour info: le mot "et" aussi a une définition:
Pour tout X si A--->(B--->X) alors X
ainsi que le mot nonA:
nonA:="pour tout X A--->X" dont je fais souvent la pub en disant "A--->tout".
"Le faux" a aussi une définition: Pour tout X: X
<a href="http://www.logique.jussieu.fr/~chalons/z022008/absrudeAC.JPG">DESSIN</a>
Merci à db et barbant raseur pour avoir cité les noms des éventuels auteurs, je ne connaissais pas les auteurs de cette preuve. Je ne peux pas confirmer, je n'ai pas les livres.
Quid de l'utilisation de l'axiome de l'extensionnalité dans la preuve donnée par le Barbant raseur ? Est-ce que cette preuve-ci répondrait au problème posé par Christophe ?
Un petit message rapide avant d'aller au lit.
Je n'ai pas eu le temps de rédiger le preuve de Goodman et Myhill version Lambek adaptée aux ensembles, mais je vois que Christophe a super-bien réécrit la version cc, ce qui rend cette velléité inutile (on parle clairement de la même chose). Christophe, je n'ai pas le temps ni la force de reprendre ta preuve et ton dessin ce soir, mais je m'engage à le faire demain.
Concernant la preuve que je propose : on m'a toujours présenté cette astuce (x=y ssi P) comme "le truc de Diaconescu". Maintenant, on m'a peut-être menti. Ca n'est peut-être pas ça, finalement, "la" preuve de Diaconescu. D'ailleurs, ça ressemble finalement beaucoup à Goodman/Myhill. Je suis convaincu que cette preuve (celle que j'ai évoquée, donc) utilise bien l'extensionalité ou du moins des concepts profondément extensionnels. Là encore, j'essaierai d'écrire quelque chose demain à ce propos.
Enfin, Daniel,
<<ça ne me semble pas contredire le fait d'être capable de savoir si une preuve donnée pour un topos élémentaire, une fois particularisée aux ensembles, utilise l'axiome d'extensionnalité ou non>>.
Bien sûr, tu as parfaitement raison. J'ai été emporté par mon fantasme d'obtenir des informations pertinentes vis-à-vis de ma conjecture.
PS : il me semble que la multiplicité des formalismes dans lesquels on peut donner un sens à la question initiale la rend assez complexe.
Je vous lis avec intérêt mais avec "un soupçon de réserve toutefois" : cela me gêne d'aller chercher une théorie du calcul des prédicats pour démontrer un axiome du calcul propositionnel.
C'est sans doute bête puisque ce résultat semble exciter pas mal de gens, mais pourquoi cette démarche ?
Bruno
La question originelle de cc, telle que je la comprends, est la suivante (bien sûr je n'ai peut-être pas ou mal compris) :
1) Constatation : si on se place dans une théorie des ensembles intuitionniste raisonnable (dans toute la suite, disons IZF, même si je ne suis pas certain que c'est ce que propose Christophe - ce cadre formel est donc celui des langages du premier ordre avec axiomes logiques intuitionnistes) alors pour toute formule close P de mon langage, l'axiome du choix (qui est une formule close de mon langage) implique P ou non(P) (qui est une formule close de mon langage).
2) On m'a dit que le résultat se maintient en remplaçant IZF par IZF\{extensionnalité} : quelqu'un peut-il me proposer une preuve ?
En cela, je ne suis pas certain qu'on parle encore des "axiomes du calcul propositionnel".
Par ailleurs, un problème majeur pour moi est qu'on peut interpréter différemment l'énoncé initial, par exemple en remplaçant IZF par une théorie des types (et on est alors dans un formalisme à l'ordre supérieur) ou par un topos (et on est alors dans le formalisme des topos) comme l'a proposé db.
Bruno
Une question est de savoir si l'on peut faire des mathématiques intuionnistes avec axiome du choix. Les preuves données par Christophe et par le Barbant raseur montrent que non. Par contre, on peut faire des mathématiques intuitionnistes avec axiome du choix dénombrable.
Cette question est-elle légitime ? Je le crois. On pourrait objecter que le principal intérêt des preuves intuitionnistes est qu'elles sont constructives et que ce n'est plus le cas si l'on utilise une variante quelconque de l'axiome du choix. Mais en réalité, la frontière entre ce qui est constructif et ce qui ne l'est pas n'est pas quelque chose de tranché définitivement. En particulier, une partie des travaux de Krivine consiste précisément à étendre la correspondance de Curry-Howard à des preuves qui utilisent l'axiome du choix dénombrable.
Bruno
Encore un message court.
Christophe, j'ai regardé le détail de ta preuve et tu es très clair. J'aurais cru qu'on utilisait l'extensionalité à plusieurs reprises mais non, tu as raison, on ne l'utilise que là où tu l'indiques.
En ce qui concerne la preuve que j'ai proposé, je ne sais pas où elle fait usage de l'extensionalité. Toutefois, il y a des détails qu'il faudrait préciser (on fait un quotient sans le dire, on utilise une forme équivalente de l'axiome du choix et je n'ai pas prouvé l'équivalence). Peut-être que dans ces détails se niche des utilisations de l'extensionalité (c'est quelque part dans les quotients à mon avis). J'aurais espéré trouver le temps m'y mettre pour reprendre la démonstration dans ces détails, mais je ne l'ai pas eu (et risque de ne pas l'avoir avant un moment). Cela dit, quelqu'un s'en chargera peut-être. Sinon, je reviendrai à ce fil dans quelques jours.
D'ici là, je serais ravi que quelqu'un propose une preuve sans extensionalité ou prouve que je me trompe en pensant que celle que j'ai indiqué l'utilise.
Bonne soirée à vous.
Pour donner une définition de cet ensemble (qui ici est déclaré exister par un "axiome tacite"), il suffit de construire un ensemble T, plutôt un triplet (x,y,T) avec T ne contenant que x et y:
Précisément le triplet (x,y,T) est tel que
*(Pour tout u: si u est dans T alors u=x ou u=y)
et
**(si P alors x=y)
et
***(si x=y alors P)
Autrement dit, il suffit de démontrer l'existence du triplet (ce qui n'a pas l'air du tout évident au premier abord sans le Tiers Exclu).
Supposons l'existence de ce triplet. La définition que tu donnes de f semble marcher: c'est l'ensemble des couples suivants:
(0,x); (1,y).
Elle est "surjective" à cause de *
Je suppose que ce que tu appelles une section est une application s de T dans {0;1} telle que pour tout élément u de T: f(s(u))=u.
Comme s est à valeurs dans {0;1} on a bien que pour tout u dans T: s(u)=0 ou s(u)=1
Donc, intuitionnistiquement tu as bien le droit de dire que "s(x)=s(y) ou s(x) diffère de s(y)" (vu que x et y sont dans T).
(remarque: supposons par exemple que s(x)=s(y); alors tu vas enchainer en disant que x=f(s(x))=f(s(y))=y qui utilise finement (même si on a l'air de faire du mal aux mouches) le signe "=" et peut-être une certaine forme d'extensionnalité en ce sens que si on traduit "s(x)=s(y)" par "s(x) et s(y) contiennent les mêmes éléments" on en infère que f, qui voit s(x) et s(y) "d'en haut", ne les distingue pas. Mais bon, ces ambiguités sur "quelle "définition" du signe "="...)
Sinon, ton raisonnement repose sur l'existence du triplet, et la suite m'a l'air sans problème.
Y a-t-il d'autres interprétations de ta phrase: ?
***
D'une manière générale, toutes les "habitudes" universitaires prises dans les premiers cycles à propos des injections, surjections, et autres "réflexes" ensemblistes sont construites sur l'axiome d'extensionnalité. Il sert continuellement de base. En particulier les différentes reformulations de l'axiome du choix ne sont pas toutes équivalentes (d'une manière évidente en tout cas) si on n'admet plus cet axiome. Par exemple, rien qu'un singleton**** peut apparaitre fort mystérieux en l'absence d'extensionnalité, donc, les couples, c'est pire encore et les ensembles de couples (ce que sont les fonctions), n'en parlons même pas...
****L'ensemble des u tels que u=1; l'ensemble des u tel que u contient les mêmes éléments que 1; etc...
i R j ssi (i=j ou P)
x = classe de 0 modulo R
y = classe de 1 modulo R
Si P, alors 0 R 1 donc x=y.
Si x=y alors 0 R 1 donc P (car 0 différent de 1).
Reste à voir si vraimenet on utilise l'axiome d'extensionnalité dans cette preuve. Bien sûr, dans le cas où l'on pourrait s'en passer, il faudrait sûrement réécrire les choses différemment : au lieu de considérer l'ensemble {0,1}, il faudra considérer un ensemble qui contient exactement 0 et 1, etc... Mais l'axiome d'extenionnalité intervient-il vraiment de manière cruciale comme dans la preuve donnée par Christophe ? Ca n'est pas clair pour moi.
Ta relation R me semble bien une relation d'équivalence.
x est l'ensemble des u tels que uR0
y est l'ensemble des u tels que uR1
Donc jusqu'ici tout va bien.
Si x=y alors c'est bien garanti que 0R1 et donc 0=1 ou P et donc P.
Si P alors 0R1 et donc x et y contiennent les mêmes éléments. [En inférer qu'ils sont égaux est donné par l'extensionnalité, mais l'est-il sans?]*
On a donc bien équivalence entre P et "x=y" (guillemets à cause de l'éventuelle utilisation de l'extensionnalité)
conclusion: tu as défini un triplet (x,y,T) dont le message de Barbant affirme l'existence qui a la propriété suivante:
(1) x=y si et seulement si P
(2) T={x,y}
* Voyons si prendre comme définition le fait de contenir les mêmes éléments n'est pas fatal à la démonstration.
Pour passer de x=y à 0R1, ça va puisque les u tels que uR0 et les v tels que vR1 sont supposés les mêmes via "x=y"
Si P alors, de même, x et y contiennent bien les mêmes éléments. Je vais noter "==" la relation "contenir les mêmes éléments".
On continue la preuve de Barbant...
On a donc P si et seulement si x==y.
Prenons la paire f formée des 2 couples (0,x) et (1,y)
C'est une surjection de {0,1} sur {x,y}. Soit s une application de {x,y} dans {0,1} avec f(s(x))=x et f(s(y))=y.
(A noter qu'il suffit de construire "nous-même" s: en déclarant que c'est la paire {(x,0); (y,1)}, et le fait que "s soit une application" resterait à justifier, mais bref)
On a le droit de dire s(x)=s(y) ou s(x) différent de s(y).
si s(x)=s(y) il est alors possible de dire s(x)=s(y)=0 ou s(x)=s(y)=1, et dans les 2 cas on obtient un vrai signe "égal" entre x et y dont on déduit x==y et donc P
si s(x) différent de s(y) on a le droit de dire (s(x)=0 et s(y)=1) ou (s(x)=1 et s(y)=0)
Dans le deuxième cas, f(1)=x et comme on sait déjà que f(0)=x CQFD.
Il reste le premier cas, peu étonnant d'ailleurs, qui affirme s(x)=0 et s(y)=1. But du jeu: en déduire non(P). Je vois mal comment se passer de l'argument "si x==y et s(x)=0 et s(y)=1 alors tout" qui est un usage d'extensionnalité?
Le concept de "manière cruciale" est informel. Mais, sinon, oui c'est vraiment une intervention importante. A un moment donné, on a une application disons g, 2 ensembles qui contiennent les mêmes éléments, disons A et B et on affirme "... alors g(A)=g(B)". C'est l'archétype même d'un usage de l'extensionnalité. En fait, l'extensionnalité permet d'utiliser les ensembles d'objets de manière platonique, ie sans tenir compte de la façon dont ils sont construits, et d'affirmer que les fonctions qui les prennent en argument ne les "voient" qu'à travers les éléments qu'ils contiennent. Par exemple, les ordinaux n'ont aucun fondement sans extensionnalité, et même les entiers ont du mal.
Axiome d'extensionnalité:
Pour tout a,b si a==b alors pour tout y (si a est dans y alors b est dans y)
où a==b est défini par "pour tout x x est dans a si et seulement si x est dans b"
où A si et seulement si B est défini par "(A implique
où "C et D" est défini par: "pour tout u,v si C implique (D implique u est dans v) alors u est dans v"
Les seuls atomes du langage autant logique que non logique étant: "pour tout", "implique" et appartenance.
"On considère alors f : {0,1} -> {x,y}" ,
il utilise l'axiome d'extensionnalité, puisqu'en son absence on ne peut parler de l'ensemble {0,1} ou de l'ensemble {x,y}, mais pas "de manière cruciale", car il est facile de prendre ses précautions en rédigeant autrement afin de s'en passer.
Pour l'instant, je ne vois pas de moyen de se passer de l'axiome d'extensionnalité. Ton problème, Christope, reste donc ouvert.