"Intuistionistic Set Theory" IZF
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
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
J'affirme péremptoirement que toute affirmation péremptoire est fausse
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 !)
Cordialement, Pierre.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
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).
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$.
- Supposons $x=0$. Alors $x=0\wedge\neg( x=0)$, donc $\bot$, donc $x=1$.
- 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é.
Par exemple je cite : GaBuZoMeu a dit : 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...