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

"Intuistionistic Set Theory" IZF

2»

Réponses

  • Merci, je vois mieux.
  • 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.
  • Modifié (24 Jun)
    @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.
  • Modifié (24 Jun)
    @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.
  • Modifié (23 Jun)
    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)
  • @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 ?

  • 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
  • @GaBuZoMeu : fantastique, mille mercis ! les topos pour les nuls ! ça c'est de mon niveau ....
  • Modifié (24 Jun)
    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".

  • Merci @Foys. Le point $(2) \Rightarrow (3)$ est beaucoup plus clair dans ta rédaction que ce que j'avais écrit initialement.
  • 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...
  • @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.
Success message!