"Intuistionistic Set Theory" IZF

2»

Réponses

  • raoul.S
    raoul.S
    Merci, je vois mieux.
  • GaBuZoMeu
    GaBuZoMeu
    Solution de l'exercice : la flèche d'ensembles $\mathbf X= X_0\rightarrow X_1\leftarrow X_2$ est décidable si et seulement si les deux applications $X_0\to X_1$ et $X_2\to X_1$ sont injectives.
    Pour tout ensemble $X$ (et en particulier pour $\mathbb N$), $X\stackrel{\mathrm {Id}}\longrightarrow X\stackrel{\mathrm{Id}}\longleftarrow X$ est décidable.
  • Martial
    Martial
    Modifié (June 2022)
    @Thierry : Merci pour ce livre, c'est une véritable mine d'or !
    @calli : je viens de vérifier, ton raisonnement est parfaitement juste. En fait tu raisonnes comme Bell (voir page 17 dans le livre joint par Thierry ci-dessus), mais tes explications sont plus claires que les siennes. Merci.
    @Tous : En revanche je ne suis pas très convaincu par la preuve que donne Bell du fait que $(2) \to (3)$. Je la reproduis ici for convenience.
    On suppose que $\Omega$ est décidable. Soit $\omega \in \Omega$. Par hypothèse on a $\omega = \{0\}$ ou $\omega \neq \{0\}$. Dans le premier cas on a $\omega = 1 \in 2$. Dans le second cas on a $\omega = \emptyset \in 2$. Donc $\Omega = \{0,1\}=2$.
    Ce qui me gêne c'est la phrase qui commence par "Dans le second cas".
    Vous en pensez quoi ? Merci.
  • GaBuZoMeu
    GaBuZoMeu
    Modifié (June 2022)
    @Martial : c'est parce que $\neg \omega=1$ équivaut à $\omega = 0$ (et $\neg \omega=0$ équivaut à $\omega=1$). Ça, c'est tout le temps vrai : on le voit par exemple avec les flèches d'ensembles $\neg(\mathbf 1\hookrightarrow \mathbf 1)= \mathbf 0\hookrightarrow \mathbf 1$ ; ou encore
    $$\mathbf 1\stackrel{\mathrm{vrai}}\longrightarrow \Omega \stackrel{\neg}\longrightarrow \Omega = \mathbf 1\stackrel{\mathrm{faux}}\longrightarrow \Omega\;.$$
    Je t'assure, un peu de manipulation des flèches d'ensembles permet de consolider son intuition intuitionniste.
    Mon illustration ne va pas : je n'ai pas assez collé aux flèches d'ensembles ! Je vais réparer ça bientôt.
  • Martial
    Martial
    OK, merci @GaBuZoMeu
  • GaBuZoMeu
    GaBuZoMeu
    Modifié (June 2022)
    Je m'y recolle plus sérieusement.
    La formule $\omega=1$, comment s'interprète-t-elle ? Puisque $\omega$ est une variable de type $\Omega$, comme un sous-objet de $\Omega$, et ce sous objet est $\mathrm{vrai} : \mathbf 1\to \Omega$. Son morphisme caractéristique est $\mathrm{Id} : \Omega\to \Omega$. Si on compose avec $\neg : \Omega\to \Omega$, on a toujours $\neg$. Et maintenant, $\neg$ est le morphisme caractéristique de $\mathrm{faux}:\mathbf 1\hookrightarrow \Omega$, qui est bien l'interprétation de $\omega=0$.
    Avec les flèches d'ensembles, $\{1\}\rightarrow \{1\}\leftarrow \{1\}$ contenu dans $\Omega = \{0,1/2,1\}\rightarrow\{0,1\}\leftarrow\{0,1/2,1\}$ (rappel les $1/2$ s'envoient sur $1$), sa négation est bien $\{0\}\rightarrow \{0\}\leftarrow \{0\}$.
    Maintenant recommençons avec $\omega=0$. Le morphisme caractéristique de son interprétation est $\neg :\Omega\to \Omega$, et $\neg\neg$ n'est pas l'identité, le morphisme caractéristique de l'interprétation de $\omega=1$.
    Avec les flèches d'ensembles, $\{0\}\rightarrow \{0\}\leftarrow \{0\}$ contenu dans $\Omega = \{0,1/2,1\}\rightarrow\{0,1\}\leftarrow\{0,1/2,1\}$, sa négation est $\{1/2,1\}\rightarrow \{1\}\leftarrow \{1/2,1\}$ et pas $\{1\}\rightarrow \{1\}\leftarrow \{1\}$.

    (correction suite à la lecture attentive de Thierry Poma)
  • Thierry Poma
    Thierry Poma
    @GaBuZoMeu : bonjour. Ne serait-ce pas plutôt $\Omega = \{0,1/2,1\} \rightarrow\{0,1\}\leftarrow\{0,1/2,1)$ ? Quel poly ou livre nous conseilles-tu , s'il te plait ?

    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).
  • GaBuZoMeu
    GaBuZoMeu
    Oui, tu as raison, je corrige.
    L'histoire des flèches d'ensembles, c'est un petit amusement pour manipuler de façon concrète une modélisation intuitionniste. Je doute que ça se trouve dans un poly, peut-être dans des textes de vulgarisation ? Chez Prouté ?
    Ouais tiens, justement, il y a ça : http://163.172.10.123:8080/topos_shadoks.pdf
  • umrk
    umrk
    @GaBuZoMeu : fantastique, mille mercis ! les topos pour les nuls ! ça c'est de mon niveau ....
  • Foys
    Foys
    Modifié (June 2022)
    Bonjour @Martial
    (2) => (3).
    Soit $x\in \mathcal P(\{\emptyset\})$. Alors $x \subseteq \{\emptyset\}$.
    (i)Premièrement, tout élément de $x$ est égal à $\emptyset$, en effet, soit $y\in x$. Alors $y\in \{\emptyset\}$ et donc $y=\emptyset$.
    (ii)Puisque $\mathcal P(\{\emptyset \})$ est supposé décidable, $x=\{\emptyset\}$ ou $x\neq \{\emptyset\}$. Dans le premier cas on a $x \in 2$. Dans le second, $x$ est vide (car pour tout $y$, $y\in x$ entraîne $y=\emptyset$ par (i) et donc $\{\emptyset \} \subseteq x$ donc $\{\emptyset\} =x$ par extensionnalité puisque $x\subseteq \{\emptyset\}$, contredisant l'hypothèse). bref $x=\emptyset$.
    Cette disjonction de cs montre que $x$ est dans $2=\{\emptyset, \{\emptyset\}\}$, berf  $\mathcal P(\{\emptyset\}) \subseteq 2$.  L'autre inclusion est immédiate.

    (5) => (6). Soit $E$ une partie de $2$. On suppose que l'appartenance de $\emptyset$ à n'importe quel ensemble et décidable.
    Alors $\emptyset \in E$ ou bien $\emptyset \notin E$. Dans le premier cas, $\emptyset = \min E$. Dans le second, $E$ est vide (l'argument est le même qu'au (2) => (3)). Donc dans les deux cas, $E$ satisfait "si $E$ est non vide, $E$ possède un plus petit élément".

    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$.
  • Martial
    Martial
    Merci @Foys. Le point $(2) \Rightarrow (3)$ est beaucoup plus clair dans ta rédaction que ce que j'avais écrit initialement.
  • Martial
    Martial
    Encore merci à tous pour vos aides nombreuses.
    Je viens de publier ce que j'ai réussi à écrire sur IZF jusqu'à présent : 
    C'est à partir de la page 300.
    Il y a encore sans doute quelques coquilles ou raisonnements approximatifs...
  • Martial
    Martial
    @Thierry : si tu lis la page 56 du livre "Intuistionistic Set Theory", tu verras qu'il y est dit que la trichotomie sur les ordinaux entraîne le tiers exclu, donc elle est fausse en général, conformément à l'impression que j'avais l'autre jour.
    L'explication est straightforward et laissée au soin du lecteur.
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 2

2 Invités