Un ensemble ordonné fini a un élément maximal
Récemment, j'ai vu à plusieurs reprises sur le forum des personnes qui utilisaient dans des contextes plus spécifiques le principe du titre, mais dans la spécificité du contexte ne se rendaient pas compte de son évidence/le reprouvaient dans leur cadre spécifique alors que la preuve générale est facile.
J'y ai réfléchi un peu, le résultat est évident mais on utilise une disjonction de cas dans sa preuve classique par récurrence. Cela m'a fait soulever la question de savoir si le résultat était vrai constructivement, plus précisément en logique intuitionniste.
Je pense que non, et je vous présente mon raisonnement, seulement je ne suis pas sûr de pouvoir complètement le raccrocher au problème :
Mon idée est de trouver un modèle de faisceaux qui contredit le résultat. Je regarde des faisceaux sur $\R$ et en particulier mon ordre sera sur le faisceau constant $\underline 2$. Je verrai cet ordre comme un morphisme $e: \underline 2 \times \underline 2 \to \Omega$, où $\Omega$ est le faisceau des valeurs de vérité : $\Omega (U) := \{V, V\subset U\}$ avec comme restriction l'intersection. J'appellerai $\mathbb P$ le "faisceau en ordres" obtenu.
Alors Je regarde $\underline 2 \times \underline 2 \to \Omega$ défini sur $U = \bigsqcup_{n\in \N} ]a_n, b_n [$ par: si $f$ est localement constante sur $U$ à valeurs dans $2\times 2$ alors elle est envoyée sur $\bigsqcup_{n\in \N} C_n$ où $C_n$ est
- $]a_n, b_n[$ si $f$ est constante égale à $(x,x)$ sur $]a_n, b_n[$
- $]a_n, b_n[ \cap \R_-^*$ si elle est constante égale à $(0,1)$ sur $]a_n, b_n[$
- $]a_n, b_n[ \cap \R_+^*$ si elle est constante égale à $(1,0)$ sur $]a_n, b_n[$
On vérifie que ça définit un ensemble ordonné via la sémantique des faisceaux (c'est mon premier doute) :
réfléxivité : pour toute section $s\in \mathbb P (U)$, $(s,s) \in \mathbb{ P\times P} (U)$ est envoyée sur $U$ dans $\Omega (U)$
transitivité : si sur $U$, $s\leq t, t\leq r$, ou bien $0\in U$, auquel cas sur sa composante connexe $s=t$ et $t=r$ de sorte que $s=r$ et $s=r$ donc $s\leq r$, et on traite le reste indépendamment , ou bien $0\notin U$ auquel cas on se ramène à $U\cap R_-^* $ et $U\cap \R_+^*$ sur lesquels c'est facile.
antisymétrie : si $s\leq t, t\leq s$ sur $U$, alors même chose qu'avant : on sépare selon que $0$ est dans $U$ ou non et sur le reste on traite la chose facilement.
Il reste à vérifier (c'est là mon doute : est-ce qu'en vérifiant ça j'aurais conclu qu'on ne peut pas prouver, disons dans IZF ou dans ETCS, qu'un ensemble ordonné a un élément maximal ? Peut-être plus précisément est-ce que la sémantique des faisceaux pour mon $\mathbb P$ coïncide avec la logique interne du topos $\mathrm{Sh}(\R)$ restreinte à ce faisceau ?) que "$\exists x, \forall y, x\leq y \implies x=y$" n'est pas vérifiée sur $\R$ tout entier.
Pour ça on suppose que c'est le cas, de sorte qu'il existe un recouvrement $(U_i)$ de $\R$ avec des sections $s_i \in \mathbb P (U_i)$ qui sont des "éléments maximaux" localement. Soit $i$ tel que $0\in U_i$, je note $U:= U_i$ et $s=s_i$ et alors on a $U \Vdash \forall y, s\leq y \implies s=y$.
Je peux alors restreindre à la composante connexe de $0$ dans $U$, $C = ]a,b[$ et on a $C\Vdash \forall y, s_{\mid C} \leq y \implies s_{\mid C} = y$.
Mais maintenant $s_{\mid C}$ est une section de $\underline 2$ sur un connexe, et donc elle est constante. Disons, par exemple qu'elle est égale à $0$. Alors soit $t$ la section constante égale à $1$ : $C\Vdash 0\leq 1 \implies 0=1$. Je spécialise alors à $V=C\cap \R_-^*$ (qui est non vide et connexe) et on obtient $V\Vdash 0\leq 1 \implies V\Vdash 0=1$, ce qui est naturellement faux. Donc $\R \nVdash \exists x, \forall y, x\leq y \implies x=y$
Au final, qu'ai-je démontré ? (si je n'ai pas fait d'erreur irrécupérable) Que $\R \Vdash [ \mathbb P$ est un ordre ] et que $\R \Vdash [ \mathbb P$ n'a pas d'élément maximal]. De plus, je sais (externalement) que $\mathbb P$ est fini. Est-ce que cela suffit ? Je ne m'y connais pas assez en sémantique des topos, c'est là que j'ai besoin de votre aide ! En particulier peut-être que GaBuZoMeu pourra m'aider à y voir plus clair ?
J'y ai réfléchi un peu, le résultat est évident mais on utilise une disjonction de cas dans sa preuve classique par récurrence. Cela m'a fait soulever la question de savoir si le résultat était vrai constructivement, plus précisément en logique intuitionniste.
Je pense que non, et je vous présente mon raisonnement, seulement je ne suis pas sûr de pouvoir complètement le raccrocher au problème :
Mon idée est de trouver un modèle de faisceaux qui contredit le résultat. Je regarde des faisceaux sur $\R$ et en particulier mon ordre sera sur le faisceau constant $\underline 2$. Je verrai cet ordre comme un morphisme $e: \underline 2 \times \underline 2 \to \Omega$, où $\Omega$ est le faisceau des valeurs de vérité : $\Omega (U) := \{V, V\subset U\}$ avec comme restriction l'intersection. J'appellerai $\mathbb P$ le "faisceau en ordres" obtenu.
Alors Je regarde $\underline 2 \times \underline 2 \to \Omega$ défini sur $U = \bigsqcup_{n\in \N} ]a_n, b_n [$ par: si $f$ est localement constante sur $U$ à valeurs dans $2\times 2$ alors elle est envoyée sur $\bigsqcup_{n\in \N} C_n$ où $C_n$ est
- $]a_n, b_n[$ si $f$ est constante égale à $(x,x)$ sur $]a_n, b_n[$
- $]a_n, b_n[ \cap \R_-^*$ si elle est constante égale à $(0,1)$ sur $]a_n, b_n[$
- $]a_n, b_n[ \cap \R_+^*$ si elle est constante égale à $(1,0)$ sur $]a_n, b_n[$
On vérifie que ça définit un ensemble ordonné via la sémantique des faisceaux (c'est mon premier doute) :
réfléxivité : pour toute section $s\in \mathbb P (U)$, $(s,s) \in \mathbb{ P\times P} (U)$ est envoyée sur $U$ dans $\Omega (U)$
transitivité : si sur $U$, $s\leq t, t\leq r$, ou bien $0\in U$, auquel cas sur sa composante connexe $s=t$ et $t=r$ de sorte que $s=r$ et $s=r$ donc $s\leq r$, et on traite le reste indépendamment , ou bien $0\notin U$ auquel cas on se ramène à $U\cap R_-^* $ et $U\cap \R_+^*$ sur lesquels c'est facile.
antisymétrie : si $s\leq t, t\leq s$ sur $U$, alors même chose qu'avant : on sépare selon que $0$ est dans $U$ ou non et sur le reste on traite la chose facilement.
Il reste à vérifier (c'est là mon doute : est-ce qu'en vérifiant ça j'aurais conclu qu'on ne peut pas prouver, disons dans IZF ou dans ETCS, qu'un ensemble ordonné a un élément maximal ? Peut-être plus précisément est-ce que la sémantique des faisceaux pour mon $\mathbb P$ coïncide avec la logique interne du topos $\mathrm{Sh}(\R)$ restreinte à ce faisceau ?) que "$\exists x, \forall y, x\leq y \implies x=y$" n'est pas vérifiée sur $\R$ tout entier.
Pour ça on suppose que c'est le cas, de sorte qu'il existe un recouvrement $(U_i)$ de $\R$ avec des sections $s_i \in \mathbb P (U_i)$ qui sont des "éléments maximaux" localement. Soit $i$ tel que $0\in U_i$, je note $U:= U_i$ et $s=s_i$ et alors on a $U \Vdash \forall y, s\leq y \implies s=y$.
Je peux alors restreindre à la composante connexe de $0$ dans $U$, $C = ]a,b[$ et on a $C\Vdash \forall y, s_{\mid C} \leq y \implies s_{\mid C} = y$.
Mais maintenant $s_{\mid C}$ est une section de $\underline 2$ sur un connexe, et donc elle est constante. Disons, par exemple qu'elle est égale à $0$. Alors soit $t$ la section constante égale à $1$ : $C\Vdash 0\leq 1 \implies 0=1$. Je spécialise alors à $V=C\cap \R_-^*$ (qui est non vide et connexe) et on obtient $V\Vdash 0\leq 1 \implies V\Vdash 0=1$, ce qui est naturellement faux. Donc $\R \nVdash \exists x, \forall y, x\leq y \implies x=y$
Au final, qu'ai-je démontré ? (si je n'ai pas fait d'erreur irrécupérable) Que $\R \Vdash [ \mathbb P$ est un ordre ] et que $\R \Vdash [ \mathbb P$ n'a pas d'élément maximal]. De plus, je sais (externalement) que $\mathbb P$ est fini. Est-ce que cela suffit ? Je ne m'y connais pas assez en sémantique des topos, c'est là que j'ai besoin de votre aide ! En particulier peut-être que GaBuZoMeu pourra m'aider à y voir plus clair ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
En effet le principe implique "axiomes d'ordre $\implies \forall x,y, x\neq y \implies (\neg (x\leq y) \lor \neg (y\leq x))$" (on regarde l'ordre induit sur $\{x,y\}$ qui est de cardinal $2$ car $x\neq y$, il a un maximum. Si c'est $x$ blablabla, si c'est $y$ blablabla).
Or mon exemple (hors de toutes questions toposiques) fournit un truc où les axiomes d'ordre sont vérifiés, qui satisfait aux déductions intuitionnistes, mais où la fin n'est pas vérifiée, donc bim.
Le théorème de complétude qui me manque c'est que la conclusion soit démontrable à partir des axiomes d'ordre. Mhm. Plus subtil que je ne le pensais. Je ne suis plus aussi convaincu qu'au début de ce message :-D
(Avec un peu de chance en fait c'est facile et je trouverai au réveil)
Si u maximal dans {x/ x=0 ou (x=1 et P)} alors P ou nonP
Mais dans l'esprit de la question de Max c'était ces parties (habitées) d'ensembles finies qui importait car sinon la question perd son contenu.
Foys : fini veut dire "en bijection avec un entier" où les entiers sont définis comme ça t'arrange, juste de sorte à pouvoir faire une récurrence.
Mon contrexemple semble suggérer que même pour $n=2$ on ne peut pas
C'est toujours comme ça. La logique intuitionniste commence vraiment à faire des étincelles quand infini. Sinon, les questions sont très à peu près toujours "la même".
De mon téléphone d'une aire d'autoroute.
Ce n'est d'ailleurs pas ce que je demande à l'ordre: par exemple si je le demande pour les ordres de taille $2$, alors je demande pour tout ordre : $\forall x,y, x\neq y \implies \neg (x\leq y)\lor \neg (y\leq x)$, dont je me rends bien compte que ça a peu de chance de marcher, mais c'est pour ça que je demandais - en particulier est-ce que ma preuve que ça ne marche pas convient ?
À part ca la.maximalite de u entraîne non (v>u) et celle de v entraîne non(u>v). De l'autoroute je ne peux guère te répondre à plus basse résolution. Mais je pense que tu sais bien qu'on ne peut pas prouver la disjonction de ces deux trucs (même en mettant autant de non devant que tu veux.
Par.contre le truc que tu dis après "je demande que" me semble carrément demander la conclusion non? (Car sans perte de généralité tu peux supposer l'ordre mis sur un entier).
GBZM : je ne comprends pas ton commentaire : effectivement mon ordre ne vérifie pas ça (en tout cas avec la sémantique des faisceaux, mais "concentrée" sur ce faisceau, c'est ça mon problème - comment passer de ça à la sémantique du topos ? )
Il y a quelque chose que je ne comprends pas dans ton message, c'est la distinction que tu fais entre "sémantique concentrée sur un faisceau" et "sémantique du topos"..
Ok alors j'essaie de préciser mon problème (je précise un truc : je ne suis pas du tout à l'aise avec la sémantique du topos, ce qui explique mes tatônnements et les erreurs que je fais). D'un côté, je connais la sémantique de faisceaux, qui est définie par exemple dans ce poly.
Cette sémantique là (de ce que je comprends) c'est "j'ai un faisceau qui a une structure dans un langage du premier ordre, et j'évalue des formules du premier ordre de ce langage dans ce faisceau". Je l'appelle (version 1)
De l'autre côté, je suis au courant de l'existence (mais ne maîtrise pas) de la sémantique d'un topos : si je ne me méprends c'est quelque chose comme son langage de Mitchell-Benabou, que tu décris notamment dans ton poly sur les faisceaux (il me semble) ou encore dans la plupart des ouvrages qui traitent de topos (The categorial analysis of logic, Sheaves in Geometry and Logic, ...); celle-là je ne la connais pas mais a priori elle traite de formules dans le langage de Mitchell-Benabou et elle répond à "est-ce que le topos satisfait cette formule ?". Je l'appellerai (version 2)
Le lien dont je ne suis pas sûr entre les deux c'est : si la sémantique de faisceaux (version 1) dit que $\mathbb P$ satisfait les axiomes d'ordre et satisfait "il n'y a pas d'élément maximal", est-ce qu'alors la sémantique "de Mitchell-Benabou" (version 2) dit que le topos des faisceaux vérifie "$\mathbb P$ est un ordre sans élément maximal" ?
Intuitivement, je dirais oui, puisqu'il me semblerait étonnant qu'on ait deux sémantiques qui diffèrent, mais comme je suis au courant qu'il y a des subtilités à ce sujet ("être projectif" a un sens différent si on regarde le topos de dehors ou de dedans par exemple !) et comme je ne maîtrise pas la version 2, je préfère ne pas m'avancer.
Que voudrais-tu d'autre ?
Avec tout ça tu fais toutes les compositions que tu veux ce qui te donne toutes les phrases (typées) que tu veux.
Il n'y a pas de variables. Tel "Forall " par exemple va de P(À croix dans P(B), etc.
Mais de toute façon ici si la valeur de u<v ainsi que celle de v<u sont prises suffisamment "moyennes", ni u ni v ne seront maximaux dans {u;v} même s'ils sont parfaitement différents.
Si on oublie tout de la définition, a priori "$R$ est une relation d'ordre transitive réfléxive et antisymétrique sur $P$" n'est pas le même énoncé que "$P\models \forall x, y, [...]$" (bon ça dépend des conventions de définition, mais syntaxiquement ces énoncés sont différents). a priori ils ne sont donc pas équivalents.
Il s'avère qu'ils sont équivalents (voire, si on élimine toutes les abréviations, peut-être égaux mais ça ça dépend de la définition de $\models$) et tout. Mais ça je peux le dire parce que je sais comment ça marche, et comment l'énoncé "$R$ est une relation blabla" s'interprète.
J'en suis moins sûr dans le cadre des topos; i.e. que la sémantique par "je calcule l'interprétation de ma formule du premier ordre dans $\mathbb P$" donne le même résultat que la sémantique par "je regarde ce que mon topos dit". Mais peut-être que c'est trivial une fois qu'on sait comme la sémantique du topos marche (ça a l'air, tellement trivial même que tu ne comprends pas ce qui me gêne :-D )
Vu qu'ici on a deux constantes $0$ et $1$ (deux flèches de l'objet terminal dans le faisceau) et que le faisceau vérifie (de façon interne) $0=1\vdash\bot$ et $\vdash x=0\vee x=1$, il n'y a pas de loup.
Pareil pour la non maximalité
Enfin je n'en doute pas, mais je prends des précautions vu que je ne m'y connais pas.
Mais tu vois, toi même tu dis "le faisceau vérifie patati", alors que j'imagine qu'il faudrait plus "le topos vérifie patata", non ?
> Mais tu vois, toi même tu dis "le faisceau vérifie patati", alors que j'imagine qu'il
> faudrait plus "le topos vérifie patata", non ?
:-S On parle bien d'un objet dans le topos des faisceaux sur $\mathbb R$, et d'un sous-objet de son produit avec lui-même qui interprète la relation d'ordre. Après, toutes les formules de la théorie des ordres sont interprétées par la logique interne du topos, bien sûr. Je dois être bouché, je ne vois pas le problème.
edit : la formule $x=0\vee x=1$ ($x$ de type $\mathbb P$) s'interprète comme $\mathbb P$ tout entier si et seulement si la formule $\forall x(x=0\vee x=1)$ s'interprète comme l'objet terminal tout entier (ici comme $\mathbb R$, si on identifie l'ensemble des sous-objets de l'objet terminal à l'ensemble des ouverts de $\mathbb R$).
Mon "problème" c'est que d'un côté on a un truc (la sémantique par ouverts - je cherche d'autres noms) où on définit la validité analytiquement : on sait qu'on a affaire à un faisceau et on utilise la structure de faisceau pour définir la validité. C'est ça que j'ai fait pour déterminer que $\mathbb P$ n'avait pas d'élément maximal.
De l'autre on a un truc (la sémantique du topos) où on définit la validité synthétiquement : la définition est valable pour n'importe quel topos et n'utilise pas le fait qu'on a affaire à des faisceaux. A priori (ce n'est sûrement pas le cas) il serait possible que ces deux trucs donnent des résultats différents, puisqu'ils ne sont pas définis pareil ! Ma question c'est "est-ce que effectivement ça donne le même résultat ?"
En d'autres termes : quand on fait la définition "synthétique" en utilisant que "on a un topos", on utilise plein d'opérations : $\implies$, $\land$, ... --> est-ce qu'elles correspondent aux opérations analytiques, qu'on utilise quand on fait la définition analytique (où on sait qu'on a un faisceau) ?
Ah ! je crois que j'ai trouvé le moyen de formuler ma question : si j'ai une formule $\varphi$ dans le langage des ordres, je peux faire tourner deux machines dessus :
1- je l'évalue avec ma sémantique des faisceaux, j'obtiens un ouvert $U_1$ : les lieux où $\varphi$ est vrai (le document que j'avais cité notait $U_1\Vdash \varphi$ pour dire que $\varphi$ est vraie sur $U_1$)
2- Je l'évalue avec ma sémantique des topos : des morphismes $\mathbb P \to \Omega, \mathbb{P\times P}\to \Omega$ etc. à la fin puisque ma formule est close j'obtiens un morphisme $1\to \Omega$, qui correspond donc à un ouvert $U_2$.
Ma question est : $U_1 =^? U_2$
Alors maintenant je me doute que la réponse est oui; mon souci est que je ne maîtrise pas la "machine 2", et donc je ne peux pas l'affirmer sans arrière-pensée. Tu sembles dire que oui ?
Disons que c'est {5:7} ta paire.
Et bien puisque tu as l'air d'aimer IR, tu affectes à [ 5<7 ] la valeur ]4,60[ par exemple et à [ 7<5 ] l'intérieur du reste.
Ainsi ils sont chacun négation l'un de l'autre et tu as bien un ordre.
La disjonction de leur négation n'edt pas IR (il manque 4 et 60). Or la phrase "il y a un elt maximal parmi eux deux est incluse dans cette disjonction. De mon téléphone.
Tu choisis l'espace topologique qui t'arrange. Puis tu remplace la valeur de "u in v" habituellement dans {vrai;faux} (tacitement) par la réunion des ouverts X tels que (u,X) est dans v.
Pour le paradigme topos je ne pourrai te résumer les points que tu ignores que d'un PC. Besoin de latex. On a de la chance on est complémentaire :-D ce que j'ignore tu l'as acquis. Ce que tu ignores je l'ai acquis :-D
Si tu t'en tiens à ça, ce que tu obtiens c'est que la théorie des ordres ne prouve pas intuitionnistement la disjonction, mais a priori (on peut imaginer qu'il n'y ait pas de théorème de complétude !) il se pourrait que ta théorie des ensembles intuitionnistes, elle, la prouve à partir des axiomes d'ordre (en faisant je-ne-sais-quel détour).
Ok pour ton deuxième message (je l'ai vu après avoir posté), mais ce truc là devient plus difficile à gérer que des faisceaux, non ? Enfin ça ressemble vachement à une affaire de type forcing et c'est un peu lourd à gérer. Alors que les faisceaux c'est facile, et la sémantique des faisceaux (qui, d'après ce que dit GBZM, coïncide avec celle du topos) est facile aussi