Pensez à lire la Charte avant de poster !

$\newcommand{\K}{\mathbf K}$


Les-Mathematiques.net - Cours de mathématiques supérieures
 Les-Mathematiques.net - Cours de mathématiques universitaires - Forum - Cours à télécharger

A lire
Deug/Prépa
Licence
Agrégation
A télécharger
Télécharger
83 personne(s) sur le site en ce moment
E. Cartan
A lire
Articles
Math/Infos
Récréation
A télécharger
Télécharger
Théorème de Cantor-Bernstein
Théo. Sylow
Théo. Ascoli
Théo. Baire
Loi forte grd nbre
Nains magiques
 
 
 
 
 

Un ensemble ordonné fini a un élément maximal

Envoyé par Maxtimax 
Un ensemble ordonné fini a un élément maximal
il y a sept semaines
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 ?

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell



Edité 1 fois. La dernière correction date de il y a sept semaines et a été effectuée par Maxtimax.
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Ah ça y est, je me suis convaincu que ça suffisait ! Enfin modulo un théorème de complétude qui je pense n'est pas très compliqué
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 grinning smiley
(Avec un peu de chance en fait c'est facile et je trouverai au réveil)

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
De mon téléphone sans lunettes :

Si u maximal dans {x/ x=0 ou (x=1 et P)} alors P ou nonP

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Que veut dire un ensemble fini en logique intuitionniste? Les parties d'un ensemble fini sont-elles forcément finies (cf l'argument de christophe c basé sur Diaconescu)? (ces questions se sont posées à votre serviteur lors de sessions coq).
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
C'est tout à fait vrai que la convention retenue par certains intuitionnistes ne décrit pas comme finie forcément une partie d'ensemble fini.

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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Christophe : ton ensemble n'est pas fini en général (s'il l'est, $P$ ou non $P$). Je ne comprends pas ton dernier commentaire d'ailleurs : pourquoi la question perdrait-elle de l'intérêt ? Tu vois bien d'ailleurs que dans mon "contrefemple" (s'il marche) mon ensemble ordonné a $2$ éléments

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.

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Et si ça ne vous va pas comme définition de fini alors on fixe les choses : je dis des "vrais" ensembles finis, au sens suivant : existe-t-il $n\in \N$ fixé tel qu'on (ne) puisse (pas) prouver intuitionnistement que tout ensemble ordonné à $n$ éléments a un élément maximal ?
Mon contrexemple semble suggérer que même pour $n=2$ on ne peut pas

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Ça ne change rien, la question porte sur l'ordre pas vraiment sur l'ensemble de toute façon. Cette situation est d'ailleurs générale... Et une question de choix d'énoncé. Si tu demandes à ton ordre de vérifier "all u,v : u < v ou non(u<v)" tu es en classique. Sinon non.

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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
À la complexité bornée près bien sûr (la LI est PSPACE complète)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Enfin en attendant même si ça ne change rien ton exemple n'en est pas un dans ces conditions winking smiley
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 ?

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Oui ça d'accord. Attention aussi, le fait qu'un topos ne vérifie pas P ne signifie pas l'indemontrabilite intuitionniste. Les topos ne peuvent pas servir de semantique à la TDE intuitionniste. Même si c'est proche.

À 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).

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
À partir du moment où l'on n'a pas $\vdash x\leq y \vee \neg\ x\leq y$, on a un problème pour le raisonnement sur l'existence d'un élément maximal. Si je comprends bien, tu prends un l'ordre sur le faisceau constant $2$ sur $\mathbb R$ où la valeur de vérité de $0\leq 1$ est $]{-\infty},0[$ et celle de $1\leq 0$ est $]0,+\infty[$ (ou vice-versa). Ça coince au-dessus de $0\in \mathbb R$ pour l'existence d'un élément maximal.



Edité 3 fois. La derni&egrave;re correction date de il y a sept semaines et a &eacute;t&eacute; effectu&eacute;e par AD.
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
christophe: ça dépend ce qu'on appelle TDE intuitionniste. Et vu la preuve en question, je pense qu'elle est traduisible dans un truc genre modèle Heyting-valué de la TDE, qui doit marcher pour IZF, non ? (sous réserve qu'elle marche)

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 ? )

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
J'avais envoyé mon message avant de l'avoir terminé, ce qui le rendait incompréhensible.
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"..
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
GBZM : ok, je suis d'accord avec ton message complet !
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.

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell



Edité 1 fois. La derni&egrave;re correction date de il y a sept semaines et a &eacute;t&eacute; effectu&eacute;e par Maxtimax.
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Je ne comprends toujours pas très bien. Ici, tu as un modèle de la théorie des ordres dans un topos, et tu montres que l'interprétation de $\exists x\ \forall y\ (x\leq y \Rightarrow x=y)$ n'est pas le vrai (concrètement, c'est $\mathbb R^*$).
Que voudrais-tu d'autre ?
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Tu as des quantificateurs et des connecteurs. Juste, ils sont totalement types. Idem tu as "in" pour chaque E croix P(E).

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 B) 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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Enlevons un instant l'intuitionnisme de la question pour faire une analogie : on raisonne classiquement dans ZF. On se donne un ensemble $P$ et $R\subset P^2$.
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 grinning smiley )

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Oui, j'ai toujours du mal à voir ce qui te pose problème ici. Tu doutes que ton ordre soit un ordre au sens interne ?
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.
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Au sens interne du topos, oui !
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 ?

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
En gros pour reprendre ton exemple simple : comment relier $\mathrm{Sh}(\R) \models \forall x : \mathbb P, x=0 \lor x=1$ et $\mathbb P\models x=0 \lor x =1$ ?

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Maxtimax écrivait:
-------------------------------------------------------

> 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 ?

confused smiley 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$).



Edité 1 fois. La derni&egrave;re correction date de il y a sept semaines et a &eacute;t&eacute; effectu&eacute;e par GaBuZoMeu.
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Il n'y a pas de problème, il n'y a que moi qui ne sait pas comment marche la logique interne du topos et son rapport avec la sémantique par ouverts.

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 ?

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
La réponse est oui.
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Ok super, merci pour la confirmation ! (promis je me mettrai un jour à la sémantique des topos pour ne plus avoir de problèmes triviaux de ce genre grinning smiley )

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Mais si tu ne veux pas conditionner ça à ton appréciation tissage des topos ici tu as vraiment un problème très simple quand ton ensemble est une paire (un ordre sur une paire!!!).

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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
J'ai oublié de préciser. Tu as tes modeles divers intuitionnistes en 2 lignes et tout au naturel comme suit. Pas besoin d'ingurgiter une théorie. Tu perds évidemment l'extensionnalite mais qui peut le plus peut le moins.

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 grinning smiley ce que j'ignore tu l'as acquis. Ce que tu ignores je l'ai acquis grinning smiley

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
Christophe : oui mais pour relier ça à une théorie intuitionniste des ensembles il faut un truc plus global, d'où le topos (alors oui un topos ne récupère pas IZF, mais ça récupère par exemple ETCS qui est relativement proche, et qui joue un rôle raisonnablement similaire).
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

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell



Edité 1 fois. La derni&egrave;re correction date de il y a sept semaines et a &eacute;t&eacute; effectu&eacute;e par Maxtimax.
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
C'EST le forcing. Après c'est une question de sensibilité. Ça ne peut pas être "difficile à gérer" puisqu' n'y a RIEN à gérer. Plus précisément l'accès aux mystères edt immédiat sans avoir à ingurgiter un gros traité. Évidemment ce n'est pas "plus facile" que quand on a {vrai, faux}. Mais pas moins.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Un ensemble ordonné fini a un élément maximal
il y a sept semaines
C'est difficile à gérer au sens où il faut plus de travail pour avoir l'intuition de comment ça marche. Les faisceaux, l'intuition est simple.

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Seuls les utilisateurs enregistrés peuvent poster des messages dans ce forum.

Cliquer ici pour vous connecter

Liste des forums - Statistiques du forum

Total
Discussions: 137 378, Messages: 1 329 960, Utilisateurs: 24 418.
Notre dernier utilisateur inscrit Edouardo01.


Ce forum
Discussions: 2 116, Messages: 41 192.

 

 
©Emmanuel Vieillard Baron 01-01-2001
Adresse Mail:

Inscription
Désinscription

Actuellement 16057 abonnés
Qu'est-ce que c'est ?
Taper le mot à rechercher

Mode d'emploi
En vrac

Faites connaître Les-Mathematiques.net à un ami
Curiosités
Participer
Latex et autres....
Collaborateurs
Forum

Nous contacter

Le vote Linux

WWW IMS
Cut the knot
Mac Tutor History...
Number, constant,...
Plouffe's inverter
The Prime page