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 ?