Es bien sabido que las topos de Grothendieck y las topos de realizabilidad (por diferentes razones) son modelos de la teoría de conjuntos intuicionista de Zermelo-Fraenkel. Por lo tanto, tanto Andrej como Todd demostraron en sus respuestas (de manera esencialmente diferente) que Cantor-Bernstein-Schroeder no puede ser demostrado en IZF.
Por supuesto, esto no significa que la propiedad de Cantor-Bernstein-Schroeder sea incompatible con la matemática constructiva; sólo muestra que IZF es demasiado débil para demostrar la CBS. Por lo tanto, una pregunta complementaria podría ser: ¿cuáles son las implicaciones de IZF+CBS; hace IZF+CBS que la lógica colapse al caso booleano?
Si no me equivoco, la respuesta es no, y el contraejemplo se construye a continuación. Sin embargo, comenzaré con una observación negativa.
Dejemos que Ω sea un álgebra de Heyting con uniones contables. Un elemento v∈Ω es complementable si existe un elemento w∈Ω tal que v∨w=1 y v∧w=0 .
Decimos que Ω es un álgebra booleana si cada uno de sus elementos es una unión finita de elementos complementables (equivalentemente, si cada elemento es complementable).
Decimos que Ω es un álgebra pro-booleana si cada uno de sus elementos es una unión contable de elementos complementables.
La afirmación es que todo topos elemental con colímite contable que satisface la propiedad de Cantor-Bernstein-Schroeder es pro-boleana (es decir, su clasificador de subobjetos es un álgebra pro-boleana).
Dejemos que v:V→1 sea un valor de "verdad" (un monomorfismo en objeto terminal). Construiremos dos objetos X=∐N1 y Y=V⊔X . Hay monomorfismos evidentes ιX:X→Y dado por la inyección del coproducto, y v⊔id:Y→X . Por tanto, por Cantor-Bernstein-Schroeder existe un isomorfismo b:Y→X . Como los coproductos en un topos son extensos, podemos dividir cada componente ι0:V→Y , ιk:1→Y del coproducto Y a lo largo de b a través de las inyecciones de los coproductos ιl:1→X obtención de elementos αk,l tal que Y≈∐k∐lαk,l≈∐l∐kαk,l y b=∐lbl con cada bl:∐lαl,k→1 siendo un isomorfismo (utilizando de nuevo la extensividad de los coproductos y el hecho de que el pullback de un iso es iso). Como las uniones en un topos son efectivas (y los coproductos son disjuntos) 1≈∐lαl,k=⋃lαl,k y así cada αl,k se complementa con ⋃x≠lαx,k . Dado que cada valor subterminal puede situarse exactamente de una manera en el objeto terminal, V=⋃lαl,0 es una unión disjunta contable de elementos complementables.
(No podemos obtener más de esta construcción; por ejemplo en la categoría de gavillas sobre números racionales con la topología habitual, ∐N1≈V⊔∐N1 para el valor de verdad (no complementable) V correspondiente a la bola abierta (−1,1) Por desgracia, hay otros objetos de esta categoría que pueden servir de contraejemplo para CBS. Permítanme también señalar que el procedimiento estándar de construir un isomorfismo a partir de dos monomorfismos no funcionaría en este caso. Sin embargo, por el argumento anterior está claro que tal isomorfismo puede construirse para cualquier topos pro-booleano. La solución es no desplazar uniformemente todo el V (o su pseudocomplemento), pero para mover cada una de las (contablemente muchas) partes complementables de V por separado).
[Lo siento mucho, ahora veo que hay un error en el siguiente argumento; intentaré arreglarlo (a condición de que sea posible --- no estoy seguro ahora). Debería haber comprobado todos los detalles relevantes antes de publicar esto como respuesta].
Para obtener un resultado positivo, considere el conjunto: D={0,1,12,13,14,…} con topología heredada de R y construir la categoría Sh(D) de gavillas sobre D . Cada conjunto abierto en D puede construirse a partir de monotones {1n} y un conjunto de la forma [0,1k] .
Dejemos que F,G:Dop→Set sean cualesquiera gavillas y supongamos que existen monomorfismos m:F→G y n:G→F . Un monomorfismo entre láminas es una inyección en cada uno de sus componentes, por lo que por el teorema de CBS para conjuntos F(U)≈G(U) para todo conjunto abierto U . Sea ϕU:F(U)≈G(U) sea una colección de tales isomorfismos. Construiremos un isomorfismo α:F→G entre gavillas de forma inductiva:
-
λ[0,1]=ϕ[0,1]
-
para todo lo que no sea vacío F({1k}) elegir un elemento 11k∈F({1k}) ; si F({1k}) está vacío, entonces λ[0,1k+1]=ϕ[0,1k+1] Si no es así λ[0,1k+1]=G([0,1k+1]⊂[0,1k])∘h1k , donde h1k:F([0,1k+1])→F([0,1k]) es el único morfismo hacia el producto F([0,1k])=F([0,1k+1])×F({1k}) inducido por F([0,1k+1])!→111k→F({1k}) y la identidad en F([0,1k+1])
-
de manera similar, para cada no vacío F([0,1k+1]) elegir un elemento 1[0,1k+1]∈F([0,1k+1]) ; si F([0,1k+1]) está vacío, entonces λ{1k}=ϕ{1k} Si no es así λ{1k}=G({1k}⊂[0,1k])∘h[0,1k+1]
-
si U es una unión disjunta de la forma [0,1k]⊔⋃i{1ni} , donde [0,1k] es el mayor intervalo contenido en U entonces λU=λ[0,1k]×∏iλ{1ni} donde los productos están determinados por las estructuras de las gavillas.
En el segundo y tercer paso hemos elegido los componentes de λ para ser compatible al alza, y en el cuarto paso la condición de naturalidad se desprende de la propiedad universal de los productos. Así, F≈G .
[EDIT: Permítanme argumentar que ϕU puede elegirse de forma que cada λU es realmente un isomorfismo. Supongamos que todos los F({1k}) son no vacíos. Definir colimF([0,1k]) para ser el colímite del diagrama: F([0,1])→F([0,12])→⋯→F([0,1k])→⋯ Lo tenemos: (colimkF([0,1k]))×(∏iF({1i}))≈F([0,1])×colim_k∏_i>kF({1i})≈F([0,1]) y de forma similar para G . Dado que en una categoría localmente presentable los monomorfismos son estables bajo colímites dirigidos, tanto: colimF([0,1k])colim(m[0,1k])→colimG([0,1k]) y: colimF([0,1k])colim(n[0,1k])←colimG([0,1k]) son monomorfismos, por lo que por CBS para conjuntos colimF([0,1k])ϕ0≈colimG([0,1k]) . Por lo tanto, ϕ[0,1] se puede suponer que es de la forma ϕ0×∏ϕ{1k} . Asimismo, cada ϕ[0,1k] . ]
(Por cierto, creo que en realidad no estamos tan lejos de la inversa del teorema anterior, pero eso es para otra historia...)