"Intuistionistic Set Theory" IZF — Les-mathematiques.net The most powerful custom community solution in the world

"Intuistionistic Set Theory" IZF

MartialMartial
Modifié (June 2022) dans Fondements et Logique
Bonjour à tous,
Je me suis lancé dans une sacrée aventure. Dans mon chapitre 26 sur les théories alternatives, j'aborde la théorie IZF, et le côté aventureux vient du fait que je ne connais rien en intuitionnisme. Je bosse sur le livre de John Bell : "Set Theory, Boolean-valued Models and Independance Proofs", Third Edition, 2005.
On dit qu'un ensemble $A$ est décidable si $\forall x \in A, \forall y \in A, (x=y \lor x \neq y)$. OK.
Page 159 Bell écrit : "Using the axiom of infinity, the set $\mathbb{N}$ of natural numbers can be constructed as usual. $\mathbb{N}$ is decidable and satisfies the familiar Peano axioms, including induction, but it is well-ordered only if LEM (Law of Excluded Middle) holds".
Ce que je ne comprends pas c'est pourquoi $\mathbb{N}$ est décidable. (Bell ne donne aucune justification). En désespoir de cause je suis allé voir le livre de Pierre Ageron : "Logique, ensembles, catégories - Le point de vue constructif". Page 15 : "Pour $a,b \in \mathbb{N}$ on a toujours $a=b$ ou $a \neq b$". Pas davantage d'explications sauf, un peu plus loin : "Postuler que l'égalité dans $\mathbb{N}$ est décidable n'est donc pas anodin : c'est la traduction mathématique d'une position philosophique, celle selon laquelle notre connaissance des entiers naturels se passe de tout intermédiaire".
Je ne savais pas qu'on pouvait énoncer un théorème de maths sur la base d'une simple profession de foi.
Bref, si quelqu'un a une explication...
Merci d'avance
Martial
«1

Réponses

  • Thierry PomaThierry Poma
    @Martial : bonsoir. Même en mathématique intuitionniste, les entiers sont des ordinaux (finis !). N'y a-t-il pas un résultat bien connu ?
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • FoysFoys
    Modifié (June 2022)
    On propose ci-dessous une démonstration intuitionniste de ce que l'égalité dans $\N$ (tel que défini dans certains traités de théorie des ensembles) est décidable (je pense que c'est de cela dont il s'agit, la phrase "$\N$ est décidable" est étrange sinon).
    $\N$ est l'intersection de tous les ensembles $X$ tels que $\emptyset \in X$ et pour tout $t\in X$, $t \cup \{t\} \in X$ (on appelle "inductifs" de tels ensembles). On note $0:=\emptyset$.
    On note $S(t):=t \cup \{t\}$ pour tout $t$. Ci-dessous, on appelle "entier" un élément de $\N$.
    1°) pour tout $n\in \N$, $n=0$ ou bien il existe $t\in \N$ tel que $S(t)=n$
    L'ensemble des entiers qui vérifient cette propriété est inductif.

    2°) tout entier $n$ est transitif (i.e. $\forall k\in \N$, $k\in n \Rightarrow k \subseteq n$)
    L'ensemble des entiers transitifs est inductif.
    3°) $S$ est injective
    Soient $x,y\in \N$ tels que $x \cup \{x\} = y \cup \{y\}$. Alors $x\in y \cup \{y\}$ et donc soit $x\in y$, soit $x=y$ (ce qui conclut).
    On a $y\in x \cup \{x\}$ et donc soit $y\in x$ soit $y=x$ (ce qui conclut). le seul cas délicat est quand $x\in y$ et $y\in x$. Mais alors comme $x$ et $y$ sont transitifs par 2°), $y\subseteq x$ et $x\subseteq y$ et donc $x=y$ (et non il n'y a pas de problème avec ce cas "impossible". On peut distinguer des cas en logique intuitionniste. Si la situation est "impossible", tout arrive y compris le résultat cible).

    4°) pour tout entier $n$, $n=0$ ou $n\neq 0$
    C'est un corollaire de 1°) puisque quel que soit $t$, $S(t)$ n'est jamais vide i.e. $S(t)\neq 0$.

    5°)  pour tout entier $n$, pour tout $p\in \N$, $p=n$ ou $p\neq n$
    Démontrons que l'ensemble des $n$ vérifiant ça est inductif (autrement dit faisons une récurrence). Le cas où $n=0$ est l'objet du 4°) ci-dessus.
    Supposons le résultat vrai pour $n$. Soit $q$ tel que $S(n)=q$. Alors $q\neq 0$ (cf  preuve du 4°). Donc $q=S(r)$ pour un certain $r$.
    Alors par hypothèse de récurrence, $n=r$ (et donc $S(n)=S(r)$) ou $n\neq r$ (et donc $S(n)\neq S(r)$ par injectivité de $S$ d'après 3°). Le résultat et démontré.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • MartialMartial
    Modifié (June 2022)
    1) Je savais que tu allais intervenir prompto !
    2) Tu réponds exactement à ma question. Il me reste à mettre de l'ordre dans mes idées, et à rédiger tout cela.
    3) (Last but not least) : GRAND MERCI !
    @Thierry Poma  : Salut. Je pense que tu fais allusion à la trichotomie sur les ordinaux. Mais je ne pense pas qu'en LI elle soit vraie pour tous les ordinaux. En tous cas elle est vraie pour $\omega$ : c'est ce que vient de démontrer Foys.
    Encore un grand merci à tous deux.
  • MartialMartial
    Modifié (June 2022)
    @Foys : je trouve qu'Ageron se fout un peu de la gu.... de ses lecteurs. Moi aussi je peux t'en trouver des professions de foi, du genre : "je crois dur comme fer à la LEM, donc ton bouquin tu peux le mettre à la poubelle".
    Aurais-tu une référence simple à me proposer pour une initiation simple et basique à la LI ? (En français ou en anglais).
    La question a dû être posée 74728 fois sur ce forum, mais comme à l'époque je ne m'intéressais pas aux idées intuitionnistes...
  • FoysFoys
    Modifié (June 2022)
    J'ai appris plus de LI en codant en COQ et en pratiquant sous la contrainte (c'est le système par défaut de COQ), qu'en lisant des livres dédiés (pour la sémantique, les algèbres de Heyting, les espaces topologiques ce sont des choses que j'ai découvertes sur le forum au cours des discussions avec Christophe et Gabuzomeu). Le livre de théorie de la démonstration de David-Nour-Raffali lui consacre un chapitre détaillé avec preuves.
    La logique intuitionniste est un peu la rédaction au propre de l'interprétation "BHK" (Brouwer-Heyting-Kolmogorov) de la logique, (cf web) qui est un principe très intuitif (à mon avis) qui a engendré plus tard la correspondance de Curry Howard.
    Tu peux aussi regarder le volumineux poly d'Alain Prouté:

    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Thierry PomaThierry Poma
    Modifié (June 2022)
    @Martial : c'est effectivement à ce résultat que je pensais. Sa démo intuitionniste pour l'ordinal $\omega$ est loin d'être triviale.
    D'autre part, Pierre Ageron nous présente un livre, supposé couvrir le point de vue constructif, mais plus de 95% des résultats sont démontrés en faisant appel à (TE). L'on peut toutefois apprécier la présence de notes historiques intéressantes.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • MartialMartial
    Modifié (June 2022)
    @Foys : Merci pour ces infos. Hélas je n'arrive pas à télécharger le poly d'Alain Prouté.
    @Thierry Poma : Entièrement d'accord avec toi. On y mélange LI, TE, AC, bref on n'y retrouve plus ses petits. Dommage...
  • Médiat_SuprèmeMédiat_Suprème
    On le trouve ici : cours_2010.pdf
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • GGGG
    Modifié (June 2022)
    Martial, à partir des axiomes de Peano,

    Lemme : $\forall n $ $(0 = n \vee 0\neq n)$ :
    Par récurrence sur $n$, vrai pour $0$ : $0 = 0$, donc $0 = 0 \vee 0 \neq 0$.
    Supposons vrai pour $n$ : $0 \neq n^+$, donc $0 = n^+ \vee 0 \neq n^+$ et donc vrai pour $n^+$.

    Lemme : Tout $n$ autre que $0$  a un prédécesseur (unique) : $\forall n $ $(n = 0 \vee \exists m $ $ m^+ = n)$.
    Par récurrence sur $n$, vrai pour $0$. Supposons vrai pour $n$ : $n^+ = n^+$ et donc vrai pour $n^+$.

    $\forall n, m $ $ (n = m \vee n \neq m)$ :
    Pa récurrence sur $n$, vrai pour $0$.
    Supposons vrai pour $n$, c'est-à-dire supposons $\forall m $ $ (n = m \vee n \neq m)$. Pour un $m$ quelconque, on a soit $m = 0$ et $n^+ = 0 \vee n^+ \neq 0$, soit $m$ a un prédécesseur $k$. Dans ce cas, si $n = k, n^+ = m$, et si $n \neq k, n^+ \neq m$. On a donc $\forall m $ $ (n^+ = m \vee n^+ \neq m)$ et la propriété est vraie pour $n^+$.

    (Je m'étais fait la même réflexion que toi en lisant le bouquin d'Ageron !)
  • pldx1pldx1
    Bonjour,
    Foys a dit : $\N$ est l'intersection de tous les ensembles $X$ tels que $\emptyset \in X$ et pour tout $t\in X$, $t \cup \{t\} \in X$ (on appelle "inductifs" de tels ensembles). 
    Que sait-on de l'existence d'au moins un ensemble inductif ? Evidemment, on peut dire $\N$ sert à compter les moutons, qui existent, donc $\N$ existe. Ensuite on peut dire: les moutons existent, car nous les mangeons. Ensuite on peut dire: nous existons, car "cogito ergo sum". Il reste à fixer le cas où Dindenault aurait eu $\N$ moutons au moment de sa rencontre avec Panurge: le vaste Océan aurait-il débordé ? Aurait-ce déclanché un "Gateway timeout" sur l'Unvers tout entier ?

     Cordialement, Pierre.
  • FoysFoys
    Modifié (June 2022)
    pldx1 a dit :
    Que sait-on de l'existence d'au moins un ensemble inductif ?
    L'existence d'un tel ensemble est parmi les axiomes de ZF (c'est l'une des versions de l'axiome de l'infini): cf par exemple https://en.wikipedia.org/wiki/Zermelo–Fraenkel_set_theory#7._Axiom_of_infinity
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • MartialMartial
    Merci à tous pour vos réponses, explications, références, PJs et remarques.
  • MartialMartial
    Modifié (June 2022)
    J'ai encore une question. Les axiomes de IZF sont : extensionnalité, paire, union, parties, infini, schéma de compréhension usuel, et les deux schémas qui suivent.
    Schéma d'induction ensembliste :
    $$\forall \overrightarrow{y} \forall a [\forall x \in a \varphi(x,\overrightarrow{y}) \to \varphi(a,\overrightarrow{y}] \to \forall a \varphi(a,\overrightarrow{y})$$
    Schéma de collection :
    $$\forall \overrightarrow{z} [\forall x \in a \exists y \theta(x,y,\overrightarrow{z}) \to \exists b \forall x \in a \exists y \in b \theta(x,y,\overrightarrow{z})]$$
    Mais dans la littérature on trouve deux versions de l'axiome de l'infini : celle donnée par Foys ci-dessus, et celle-ci :
    $$\exists x [(\exists a (a \in x)) \land \forall y \in x \exists z \in x (y \in z)]$$
    Pensez-vous qu'on puisse démontrer, dans $IZF - \{Infini\}$, que ces deux versions de l'axiome de l'infini sont équivalentes ?
  • MartialMartial
    J'ai oublié de préciser un truc : dans un sens c'est trivial. S'il existe un ensemble inductif il suffit de prendre $z=y \cup \{y\}$ pour assurer la deuxième version. Mon questionnement concerne donc l'autre sens.
  • FoysFoys
    Modifié (June 2022)
    Une idée possible est d'exploiter ce schéma d'induction ensembliste (qui est un axiome de fondation déguisé j'ai l'impression).
    Soit $M$ un ensemble et $H$ une relation fonctionnelle sur l'univers. On peut définir par induction une fonction $r$ telle que pour tout $x\in M$, $r(x)= H(r|_{x\cap M})$ en faisant exactement comme dans le bouquin de Krivine (on définit les fonctions inductives partielles comme les fonctions $s$ définies sur une partie $D$ de $M$ telle que $\forall x\in D, x \cap M \subseteq D$ et $H(s|_{x\cap M}) = s(x)$ puis on prend pour $r$ leur réunion. Si $H$ est définie sur tout l'univers, $r$ est définie sur tout $X$ à nouveau par induction et vérifie l'équation qu'on veut).
    On pose maintenant, pour tous $f,s,t$,
    $Dom (f):= \{x \mid \exists y: (x,y)\in f\}$
    $f(s):= \bigcup \{z\mid (s,z) \in f\}$
    $H(t):= \{\emptyset\} \cup \bigcup \{v \cup \{v\} \mid \exists i \in Dom(t): v \in t(i) \}$.
    Soit $X$ un ensemble vérifiant ton hypothèse bizarre. Soit $\rho$ la fonction définie par récurrence sur $X$ comme ci-dessus, telle que $H(\rho|_{y \cap X})  = \rho (y)$ pour tout $y\in X$. Soit $Y$ l'image de $X$  par $\rho$ (le schéma de collection entraîne le schéma de substitution usuel).
    On a en dépliant la définition ci-dessus, pour tout $t\in X$, $\rho (t) = \{\emptyset\} \cup \{v \cup \{v\} \mid \exists s \in t\cap X; v \in \rho (s)\}$.
    Alors $\bigcup Y = \bigcup_{x\in X} \rho (x)$ est inductif. En effet, comme par hypothèse il y a un $a\in X$, on a $\emptyset \in \rho (a) \in \bigcup Y$.
    De plus soit $r\in \bigcup_{x \in X} \rho (x)$ et soit $m\in X$ tel que $r\in \rho (m)$. Alors il existe $n\in X$ tel que $m \in n$. Donc $\rho (n) = \{\emptyset\} \cup \{v \cup \{v\} \mid \exists s \in n\cap X; v \in \rho (s)\}$. On a $m\in n \cap X$ et donc $r\cup \{r\} \in \rho (n) \subseteq \bigcup Y$.
    CQFD.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • MartialMartial
    Modifié (June 2022)
    @Foys : Merci pour cette belle preuve. Je voyais comment raisonner roughly speaking : on construit l'ensemble inductif $Y$ de façon inductive. Puisque $\emptyset \in X$, on l'envoie dans $Y$. Puisque par hypothèse $\exists y \in X, \emptyset \in y$, en envoie $y$ sur $\{\emptyset\}$. Puisqu'il existe $z \in X$ tel que $y \in z$, on envoie $z$ sur $\{\emptyset, \{\emptyset\}\}$, et ainsi de suite. Mais je ne savais pas comment le formaliser correctement.
    "Une idée possible est d'exploiter ce schéma d'induction ensembliste (qui est un axiome de fondation déguisé j'ai l'impression)."
    Il faut que je regarde mais je pense que la preuve du fait que cet axiome bizarre entraîne l'axiome de fondation ne marche plus en logique intuitionniste. La "preuve" en est que si on remplace le schéma d'induction ensembliste par l'axiome de fondation on récupère la loi du tiers exclu. (Exercice, mais de toutes façons je ne vais pas tarder à publier tout ça). J'en profiterai pour te remercier au passage, si tu n'y vois pas d'inconvénient.
  • MartialMartial
    Désolé, j'ai encore un problème. John Bell énonce sans démonstration le résultat suivant : sous IZF, les propositions suivantes sont équivalentes. On note $\Omega=\mathscr P(1)=\mathscr P(\{0\})$.
    (0) La règle du tiers exclu est vraie.
    (1) Tout ensemble est décidable.
    (2) $\Omega$ est décidable.
    (3) $\Omega=2$.
    (4) L'appartenance est décidable : $\forall x \forall y (x \in y \lor x \notin y)$.
    (5) $\forall x (0 \in x \lor 0 \notin x)$.
    (6) $(2, \leq)$ est bien ordonné.

    Voyons voir : $(0) \to (1)$ est clair.
    $(1) \to (2)$ est trivial.
    (3) est clairement équivalent à (0), donc $(3) \to (4)$ ne pose pas de problème.
    $(4) \to (5)$ est trivial.
    Je sais faire $(6) \to (0)$ (sur une indication de l'auteur).

    Conclusion : il me manque $(2) \to (3)$ et $(5) \to (6)$. Mais là, grand mystère...
  • Thierry PomaThierry Poma
    Modifié (June 2022)
    @Martial : bonsoir. Juste pour info et si tu as le temps, quelle est la définition de Bell adoptée pour un ensemble bien ordonné, s'il te plait ? Je ne pense pas que ce soit la définition classique, vu que l'on travaille dans une mathématique intuitionniste.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • MartialMartial
    @Thierry : Bonsoir. Je n'ai pas vérifié, mais il me semblerait logique, en LI, de définir un ensemble bien ordonné comme tout couple $(X, \leq)$ pour lequel  tout sous-ensemble habité de $X$ admet un plus petit élément.
    Un ensemble habité est un ensemble $X$ tel que $\exists a (a \in X)$.
    Tout ensemble habité est non vide, mais un ensemble non vide n'est pas forcément habité.
    C'est le genre de remarque qui m'a toujours tué.

    Si on considère que Coupable = $\neg$ Innocent, "l'accusé n'est pas coupable" n'implique pas forcément "l'accusé est innocent". Donc en intuitionnisme toute mise en examen est fatale : tu n'iras peut-être pas en prison mais tu ne seras jamais blanchi.

  • Médiat_SuprèmeMédiat_Suprème
    Bon exemple : ne pas avoir la preuve de la culpabilité n'est pas la preuve de l'innocence.
    Il ne faut pas respirer la compote, ça fait tousser.

    J'affirme péremptoirement que toute affirmation péremptoire est fausse
  • MartialMartial
    @Thierry : je confirme. Je viens de tomber par hasard sur la page 17 du livre d'Ageron. Tout en haut de la page, on lit :
    Théorème : Les assertions suivantes sont équivalentes.
    (i) la conjonction du principe du tiers exclu et du principe de récurrence.
    (ii) tout sous-ensemble habité de $\mathbb{N}$ possède un plus petit élément.

    Donc c'est bien ça la définition de "bien ordonné". De toutes façons il est difficile de faire autrement. De plus cela correspond bien avec Bell, car il dit que $\mathbb{N}$ est décidable, qu'il satisfait Peano, mais qu'en revanche il n'est bien ordonné que ssi le tiers exclu est satisfait.
  • Thierry PomaThierry Poma
    @Martial : je possède ce livre. Lis la leçon 14 ; tu vas être surpris.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • Thierry PomaThierry Poma
    Modifié (June 2022)
    Tu vois d'ailleurs que, si toute partie habitée de $\N$ admet un plus petit élément, le principe du tiers exclu en découle en particuliers. La définition classique du bon ordre sur un ensemble est donc irrecevable en Mathématique intuitionniste ; fort heureusement.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • GaBuZoMeuGaBuZoMeu
    Modifié (June 2022)
    Bonsoir
    J'aime bien travailler sur des choses concrètes. Par exemple, le topos des flèches d'ensembles.
    Une flèche d'ensembles, c'est trois ensembles et des applications comme ça : $$\mathbf X=X_0\rightarrow X_1\leftarrow X_2$$ Un morphisme d'une flèche d'ensembles $\mathbf X$ dans une flèche d'ensembles $\mathbf Y$, c'est trois applications $X_i\to Y_i$ qui font commuter les deux carrés.
    L'objet terminal du topos des flèches d'ensembles est $\mathbf1=1\rightarrow 1\leftarrow 1$ et un point d'une flèche d'ensembles $\mathbf X$ est un morphisme $\mathbf 1 \to \mathbf X$.
    La flèche d'ensembles vide, l'objet initial du topos des flèches d'ensembles, est bien sûr $\mathbf 0= 0\rightarrow 0\leftarrow 0$.
    Le support d'une flèche d'ensembles $\mathbf X$ est l'image de l'unique morphisme $\mathbf X\to \mathbf 1$. C'est un sous-objet de $\mathbf 1$ (combien y a-t-il de tels sous-objets, d'ailleurs ?). Une flèche d'ensembles est habitée si et seulement si son support est $\mathbf 1$.
    Si une flèche d'ensembles a un point, alors elle est habitée.
    Si une flèche d'ensembles est habitée, alors elle est non vide.
    Mais aucune des implications réciproques n'est vraie.
    On pourrait aussi s'amuser avec l'objet des entiers naturels du topos des flèches d'ensembles. C'est bien sûr $\mathbf N = \mathbb N\rightarrow\mathbb N\leftarrow \mathbb N$.
  • MartialMartial
    Modifié (June 2022)
    @Thierry : je te reçois 5 sur 5, j'irai voir le chap 14 demain.
    @GaBuZoMeu : Sorry je ne connais rien aux topos, Donc je suis incapable de comprendre ton post. Dommage...
  • GaBuZoMeuGaBuZoMeu
    Mais si, tu es capable, Martial. Il n'y a pas besoin de savoir ce qu'est un topos pour jouer avec les flèches d'ensembles.
    Allez, je t'aide avec un exemple :  $\{a\}\hookrightarrow \{a,b\}\hookleftarrow \{b\}$ est une flèche d'ensembles habitée sans point.
  • Georges AbitbolGeorges Abitbol
    @GaBuZoMeu : c’est quoi l’image d’un morphisme de flèches d’ensembles ? C’est le seul truc imaginable ?
  • GaBuZoMeuGaBuZoMeu
    Oui, c'est bien sûr le truc auquel tout le monde pense. :)
  • Georges AbitbolGeorges Abitbol
    Modifié (June 2022)
    EDIT : Ne pas tenir compte de ce message, tout s'arrange plus loin.

    Hum, je ne suis pas sur ordi et ne peux écrire de formules, mais est-ce que tout morphisme a une image ? 
    Je m’étais dit que le triplet d’ensembles, ça devait être le triplet des images « verticales » (je note les morphismes verticalement) mais je ne vois pas si on peut toujours définir les applications horizontales : on pourrait les définir par chasse au diagramme mais je n’arrive pas à voir si différents choix d’antécédents donnent la même chose.
  • Thierry PomaThierry Poma
    Je n'ai pas vu les topos. Mais si je devais faire un parallèle avec la théorie des ensembles, je trouve deux morphismes : le morphisme d'inclusion $\mathbf 0\to \mathbf 1$ et le morphisme $\mathbf 1\to \mathbf 1$, ce qui nous donne deux sous-objets.


    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • CalliCalli
    Modifié (June 2022)
    Bonjour, 
    Je n'ai pas trop suivi/compris le début du fil, mais c'est amusant ces flèches d'ensembles présentées par @GaBuZoMeu. 

    @Georges Abitbol, je crois qu'il suffit de restreindre les applications horizontales de la 2e flèche d'ensembles aux images des applications verticales, et on vérifie rapidement que ces restrictions débouchent dans l'image du morphisme vertical du milieu (par commutativité des diagrammes). 
  • Georges AbitbolGeorges Abitbol
    Modifié (June 2022)
    Yes, merci @Calli, jme suis un peu emmêlé les pinceaux, j'ai oublié ce qui était donné et ce qui était à construire...

    Soient $X := (X_0,X_1,X_2,f_0,f_2)$ et $Y :=(Y_0,Y_1,Y_2,g_0,g_2)$ deux flèches d'ensembles. Soit $\phi := (\phi_0,\phi_1,\phi_2)$ un morphisme de $X$ vers $Y$.
    L'image de $\phi$ est $(Z_0,Z_1,Z_2,h_0,h_2)$ où chaque $Z_i$ est $\phi_i(X_i)$, et, pour tout $i \in \{0,2\}$, pour tout $z\in Z_i$, $h_i(z) = g_i(z)$.
    Quant à la question du nombre de sous-objets de $\textbf{1}$... Notons $\textbf{1}_G$ ($G$ comme "gauche") le triplet $1\rightarrow 1 \leftarrow 0$. Comme il n'y a pas de morphisme de $\textbf{1}$ vers $\textbf{1}_G$, ces deux-là ne sont pas des représentants du même sous-objet de $\textbf{1}$. De même, il n'y a pas de morphisme de $\textbf{1}_G$ vers $\textbf{0}$, dont ces deux-là ne sont pas des représentants du même sous-objet de $\textbf{1}$. Ca fait donc un troisième sous-objet. On peut définir aussi $\textbf{1}_D$ ($D$ comme droite) qui va donner encore un sous-objet. Ça fait déjà quatre sous-objets.
    Il y aurait encore $\textbf{1}_M := 0 \rightarrow 1 \leftarrow 0$, équivalent à aucun des autres.
  • GaBuZoMeuGaBuZoMeu
    GA, tu as bien trouvé les cinq sous-objets de $\mathbf 1$.
    Ces cinq sous objets forment une algèbre de Heyting. Par exemple, qui est $\neg \mathbf 1_G$ (avec ta notation) ?
  • Thierry PomaThierry Poma
    Je suis à côté de la plaque...
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • GaBuZoMeuGaBuZoMeu
    Modifié (June 2022)
    Un sous-objet habité (et qui a même un point) de l'objet des entiers naturels sans plus petit élément : $\{0,1\}\hookrightarrow \mathbb N\hookleftarrow \{1\}$.
  • MartialMartial
    @Thierry : j'ai lu le chap 14 que tu mentionnes ci-dessus. J'en déduis que Bell et Ageron n'ont pas la même définition de "bien ordonné". Chez Ageron, $\mathbb{N}$ est bien ordonné parce qu'il est totalement ordonné, qu'il vérifie le principe de récurrence et qu'il est décidable grâce à la profession de foi du chap 4 (qui en fait est un théorème, mais passons). Chez Bell, "$\mathbb{N}$ est bien ordonné" entraîne le tiers exclu, donc on n'est pas dans le même monde. En fait, il suffit même que $(2, \leq)$ soit bien ordonné (au sens de Bell) pour pouvoir en déduire le tiers exclu.

    @Tous : Sorry mais je suis complètement largué, je ne comprends rien à ces histoires de flèches d'ensembles. Cela ne me dérange nullement que vous discutiez de cela, mais si quelqu'un pouvait m'éclaircir sur les points $(2) \to (3)$ et $(5) \to (6)$ du théorème ci-dessus, je lui en saurais un plein pot de gré.
  • MartialMartial
    @Thierry : plus j'avance et plus j'ai l'impression qu'Ageron se mord la queue dans son livre. Il n'y a aucune cohérence interne, et à chaque instant $t$ on se demande dans quel monde on vit.
  • GaBuZoMeuGaBuZoMeu
    Modifié (June 2022)
    Les flèches d'ensembles, c'est beaucoup plus rassurant ! On sait parfaitement où on est et ce qu'on fait. :D 
    $\mathbf 2$, c'est $\{0,1\}\rightarrow\{0,1\}\leftarrow\{0,1\}$ et il n'est pas bien ordonné car $\{0,1\}\rightarrow\{0,1\}\leftarrow\{1\}$ n'a pas de plus petit élément.

  • CalliCalli
    Modifié (June 2022)
    @Martial, je suis grand débutant en logique intuitionniste, mais je tente un truc pour $(5)\Rightarrow(6)$. C'est peut-être complètement faux (notamment parce que je ne suis pas sur de la définition de certains objets en logique intuitionniste), auquel cas désolé.

    On veut montrer $(\forall x (0 \in x \lor 0 \notin x))\Rightarrow$ ($2$ est bien ordonné). Soit $A$ un sous-ensemble habité de $2$.

    Cas 1 : Supposons $0\in A$. Alors $0$ est le plus petit élément de $A$ car $\forall x\in A, x\geqslant 0$, puisque $\forall x\in 2, x\geqslant 0$.

    Cas 2 : Supposons $0\not\in A$. On a $2 = 1\cup\{1\} = \{0\}\cup\{1\}$ donc : $\forall x \in A, x=0 \vee x=1$ (si la définition intuitionniste de $\cup$ est bien celle que je pense). Montrons $\forall x\in A,x=1$. Soit $x\in A$.
    1. Supposons $x=0$. Alors $x=0\wedge\neg( x=0)$, donc $\bot$, donc $x=1$.
    2. Supposons $x=1$. Alors $x=1$ (il n'y a rien à faire).
    Or $A$ est habité, donc $1\in A$. Et donc $1$ est le min de $A$.
    Donc dans les deux cas $A$ a un min, et $2$ est bien ordonné.
  • CalliCalli
    @GaBuZoMeu, qu'est-ce que ça veut dire qu'une flèche d'ensembles ait un "plus petit élément" ? Qu'est-ce qu'un "élément" d'une flèche d'ensembles ?
  • Thierry PomaThierry Poma
    @Martial : bonjour. Nous apprenons à marcher dans un monde nouveau, inconnu jusque-là. Dans ce monde, il faut exclure le principe du tiers exclu et tout ce qui s'y rattache directement, voire indirectement. La démarche n'est pas aisée. D'autres sont plus à l'aise. Moi, je prends mon temps ; ce que je ne comprends pas aujourd’hui, je le comprendrai demain. Il ne faut pas renoncer.
    Voici un lien qui va te convenir, où l'on s'attachera au résultat de la page 17 en particuliers.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • GaBuZoMeuGaBuZoMeu
    Modifié (June 2022)
    Excuse-moi, Martial, je continue de polluer avec les flèches d'ensembles.
    C'est, quoi $\Omega$ pour les flèches d'ensembles ? J'assène :
    $$ \Omega = \{0,1/2,1\} \rightarrow\{0,1\}\leftarrow\{0,1/2,1)$$
    où, de chaque côté, $1/2$ s'envoie sur $1$. On a un morphisme "vrai" de $\mathbf 1$ dans $\Omega$ qui sélectionne les $1$, et un morphisme "faux" qui sélectionne les $0$.
    Pour quoi c'est le bon $\Omega$ ? Parce que tout sous-objet $\mathbf Y\hookrightarrow \mathbf X$ a un unique morphisme caractéristique $\chi_{\mathbf Y} : \mathbf X \to \Omega$, tel que $\mathbf Y$ est l'image réciproque de "vrai" par $\chi_{\mathbf Y}$. Ce morphisme caractéristique est défini  à gauche par $\chi_{\mathbf Y,0}(x)=$ :
    • $1$ si $x$ est dans $Y_0$,
    • $1/2$ si $x$ n'est pas dans $Y_0$ mais son image dans $X_1$ est dans $Y_1$,
    • $0$ si l'image de $x$ dans $X_1$ est dans $Y_1$.
    À droite, même chose en remplaçant $0$ par $2$ et au milieu, $\chi_{\mathbf Y,1}$ est simplement la fonction caractéristique de $Y_1\subset X_1$.
    C'est sûr, $\Omega$ n'est pas $\mathbf 2$. Et c'est sûr aussi, $\Omega$ n'est pas décidable (je préférerais dire discret) parce que la diagonale $\Delta : \Omega \hookrightarrow \Omega\times \Omega$ n'est pas complémentée. On peut vérifier que dans la partie gauche de $\neg \Delta$, on n'a pas $(1,1/2)$.
    Exercice : trouver une condition nécessaire et suffisante sur la flèche d'ensembles $X_0\rightarrow X_1\leftarrow X_2$ pour qu'elle soit décidable.



  • MartialMartial
    @Calli : j'ai l'impression que ce que tu écris est juste, il faut que je vérifie.

    @Thierry : merci pour le livre.
  • Thierry PomaThierry Poma
    Modifié (June 2022)
    @Martial : de rien ; il faut remercier l'auteur. Lorsque tu écris un raisonnement, le plus compliqué est de s'assurer qu'il s'agit bien d'un raisonnement intuitionniste, de s'assurer que toutes les nouvelles règles du jeu ont été respectées.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • GaBuZoMeuGaBuZoMeu
    Modifié (June 2022)
    Calli a dit :
    @GaBuZoMeu, qu'est-ce que ça veut dire qu'une flèche d'ensembles ait un "plus petit élément" ? Qu'est-ce qu'un "élément" d'une flèche d'ensembles ?
    Le plus petit élément, s'il existe, est unique et se manifeste alors par un point de la flèche d'ensembles.
    Mais voyons ça de plus près. On a une flèche d'ensembles ordonnée $\mathbf X$, ça veut dire trois ensembles ordonnés avec des applications croissantes $X_0\rightarrow X_1\leftarrow X_2$. Autre façon de voir, un sous objet $\leq \hookrightarrow \mathbf X\times \mathbf X$, vérifiant ce qu'on demande à un ordre ; ce sous objet est l'interprétation de la formule $x\leq y$.
    Comment interpréter $\forall y ,\ x\leq y$ ? C'est le plus grand sous-objet de $\mathbf X$ dont l'image réciproque par la première projection est contenue dans $\leq$. Un moment de réflexion montre que c'est le $\mathbf Y\subset \mathbf X$ ainsi décrit :
    • $Y_1$ est réduit au plus petit élément de $X_1$, ou vide s'il n'y a pas de plus petit élément,
    • $Y_0$ est réduit au plus petit élément de $X_0$ s'il existe et s'envoie sur le plus petit élément de $X_1$, vide sinon,
    • idem pour $Y_2$.
    Quelle est l'interprétation de $\exists x,\ \forall\ y,\ x\leq y$ ? Tout simplement le support de $\mathbf Y$. Si ce support est $\mathbf 1$, C'est que $\mathbf X$ a un point qui sélectionne le plus petit élément de chaque $X_i$, celui de $X_1$ étant l'image de ceux de $X_0$ et $X_2$.
  • Georges AbitbolGeorges Abitbol
    Modifié (June 2022)
    @GaBuZoMeu : C'est quoi, la négation ? C'est le truc qui classifie les morphismes vers $\textbf{1}$ ? Et les éléments d'une flèche d'ensembles ?
    @Martial : Y a rien à comprendre, à part quelques abréviations à connaître !
  • GaBuZoMeuGaBuZoMeu
    La négation d'un sous-truc $\mathbf Y\hookrightarrow\mathbf X$, c'est le plus grand sous-truc $\mathbf Z\hookrightarrow\mathbf X$ dont l'intersection avec $\mathbf Y$ est $\mathbf 0$ (vide).
    La négation se voit aussi comme morphisme $\neg : \Omega\to \Omega$ qui envoie $0$ sur $1$, $1$ sur $0$ et $1/2$ sur $0$. On a bien $\neg\circ \chi_{\mathbf Y}= \chi_{\neg \mathbf Y}$.

    Pauvre Martial, il doit se sentir complètement squatté par les flèches d'ensembles qui ne l'intéressent pas. Serait-il possible de scinder la discussion ?
  • CalliCalli
    Merci @GaBuZoMeu. C'est quand même compliqué ces flèches d'ensembles. Il faut être bien concentré.
  • raoul.Sraoul.S
    C'est intéressant de découvrir ces nouveaux objets, mais sans une connaissance basique des catégories c'est effectivement compliqué.

    Par exemple je cite : GaBuZoMeu a dit :
    La négation d'un sous-truc $\mathbf Y\hookrightarrow\mathbf X$, c'est le plus grand sous-truc $\mathbf Z\hookrightarrow\mathbf X$ dont l'intersection avec $\mathbf Y$ est $\mathbf 0$ (vide).
    GaBuZoMeu ou un autre, c'est quoi l'intersection dans ce contexte ? En regardant un peu je crois qu'il s'agit peut-être du produit fibré (Wikipedia en parle surtout dans la catégorie des ensembles mais j'imagine qu'il y a plein de catégories où il existe un produit fibré).

    PS. il faudra attendre décembre... :mrgreen:
  • GaBuZoMeuGaBuZoMeu
    L'intersection de sous-objets peut effectivement se formuler en termes de produit fibrés.
    Mais ici, restons simples : les sous-objets $\mathbf Y$ et $\mathbf Z$ de la flèche d'ensembles $\mathbf X$ sont simplement donnés par des sous-ensembles $Y_i$ et $Z_i$ des $X_i$ (avec la condition que les images de $Y_0$ et de $Y_2$ dans $X_1$ sont contenues dans $Y_1$, idem pour les $Z_i$).
    L'intersection de $\mathbf Y$ et $\mathbf Z$ est tout bêtement donnée par les $Y_i\cap Z_i$.
Connectez-vous ou Inscrivez-vous pour répondre.
Success message!