"Intuistionistic Set Theory" IZF

raoul.S

Merci, je vois mieux.

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

@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

@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

OK, merci @GaBuZoMeu

GaBuZoMeu

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

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

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

@GaBuZoMeu : fantastique, mille mercis ! les topos pour les nuls ! ça c'est de mon niveau ....

Foys

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".

Martial

Merci @Foys. Le point $(2) \Rightarrow (3)$ est beaucoup plus clair dans ta rédaction que ce que j'avais écrit initialement.

Martial

Encore merci à tous pour vos aides nombreuses.

Je viens de publier ce que j'ai réussi à écrire sur IZF jusqu'à présent : 

https://drive.google.com/file/d/1P7_UlJmLsGzI_58wMiTsDE0fJaeURDqY/view

C'est à partir de la page 300.

Il y a encore sans doute quelques coquilles ou raisonnements approximatifs...

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.