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.
@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".
@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
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 ?
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é ?
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".
@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.
Réponses