Le topos $ \mathbb{Ens}$

Dans le paradigme topos, c'est $P(1)$ qui sert d'ensemble de valeurs de vérité. Il faut des hypothèses nettement plus fortes (et en fait rendre les topos inutiles) pour avoir $P(1) = \{0;1\}$ car

$$ \{a;b\} := \{x\mid x=a\ ou \ x=b\}$$

Rappel: $1:=\{\emptyset \}$

Le topos Ens n'a rien d'un modèle de ZF (encore moins de ZFC). Les topos "singent" un paradigme ensembliste à travers le fait qu'il y a une possibilité d'associer à chaque énoncé borné du langage $\{\in ; \forall ; connecteurs\}$ une flèche de sorte que ça ne marche pas trop mal (et moyennant quelques ajouts, on peut le faire même pour les énoncés non bornés).

Mais ce n'est qu'un changement psychologique. Mathématiquement et froidement tout ceci revient + ou - à faire les mêmes choses en enlevant ceci ou cela des axiomes. Le fait que ce soit fait en catégories permet de donner "une signature" à ce retrait (sinon, n'importe qui pourrait arriver et dire "je retire ceci, cela, je garde ceci, cela" et quand on lui demanderait "pourquoi", il répondrait comme le héros de la pub orangina)

Je ne comprends pas trop pourquoi tu sembles vouloir jouer avec des topos avant d'étudier les catégories cartésiennes fermées qui contiennent déjà tout et plus que nécessaire.

Je te rappelle que:

1/ $(x\in y)$ n'est rien d'autre que $y(x)$ avec $y$ à valeurs dans un machin qui s'appelle pour les humains traditionnels $\{faux; vrai\}$

2/ $(\forall xR(x)) = ([x\mapsto R(x)] = Constante(vrai) )$

3/ $(A\ et\ = ((A,B)=(vrai,vrai))$

etc, etc

Le toposisme (ne pas confondre avec les topos) est un cadre philosophico-technique où on va plutôt traduire $(A\Rightarrow $ par $A\subset B$, $vrai$ par $1$ et $faux$ par $\emptyset$. Ca désarbitrarise qui sont $vrai$ et $faux$. Mais leur caractère arbitraire n'était de toute façon pas gênant. De plus, l'aspect catégorique apporte le handicap (volontaire) de mettre au second plan les différences entre des choses isomorphes, donc propose une autre langue pour lire qui apporte, avec ses avantages et ses inconvénients des trucs important à certaines spécialités qui privilégient cet aspect (l'algèbre plus particulièrement).

Les traductions sont évidentes une fois qu'on a compris à quel jeu on joue, mais je crois (avis subjectif) que tu fantasmes peut-être un peu tout ça, quand je croise tes divers fils. On n'a rien sans rien, ces traductions ont leur intérêt, mais ne résolvent rien toutes seules.

Un modèle de ZF c'est un couple $(E,R)$ où $R\subseteq E^2)$ et non pas une catégorie, c'est tout, rien de plus. On peut "fabriquer un topos" avec un modèle de ZF, mais c'est autre chose. Dans un topos tu n'as pas de relation d'appartenance, tu la simules d'une façon spéciale.

Certes mais c'est juste du blabla de café du commerce entre experts. De mon téléphone.

Tu n'apprendras pas les idées de fond de Cohen dans ce langage. Les inter traductions sont t bien entendu toutes possibles puisqu'on peut singer la TDE dans le cadre topos mais le fait de faire ces remarques est surtout une action promotionnelle pour "vanter" les categories. Un peu comme si pour vanter Matiyasevic tu t'amusais à traduire quelques bons livres d'informatique théorique en liste de pages remplies d'équations diophantiennes.

Donc tout dépend de ton but. Apprendre les catégories (dans ce cas vas plutôt vers ce qu'elle gére bien et associativement: l'algèbre, la géométrie algébrique) ou apprendre la logique et la partie graduée du platonisme scientifique c'est à dire les résultat de fond du genre "telle théorie est plus forte que telle autre de manière "absolue"". Dans ce cas où lié le plus vite possible qu'on peut aller de Marseille à Aubagne en passant par Paris même si c'est VRAI. Sinon tu auras pas assez de 10vies :-D. Et pour info l'équivalent de ces activités d'experts existent même en arithmétique de base: wikipédia te donne un polynome dont les valeurs positives sont exactement les nombres premiers. Mais :-D je te déconseille de la même façon et pour les mêmes raisons cette définition pour prouver qu'il y a une infinité de nombres premiers.

De rien: en gros il y a des outils pour l'infini et d'autres pour le fini. Ceux pour l'infini ONT INTERET ET SE DOIVENT DE "ne pas voir le fini" (on peut le prouver).