¿Cuánto cuesta dividir por $2$ ?

Question

Teorema 1 [ZFC, lógica clásica]: Si $A,B$ son conjuntos tales que $\textbf{2}\times A\cong \textbf{2}\times B$ entonces $A\cong B$ .

Eso es porque el axioma de elección permite la definición de cardinalidad $|A|$ de cualquier conjunto $A$ y para $|A|\geq\aleph_0$ tenemos $|\textbf{2}\times A|=|A|$ .

Teorema 2 : El teorema 1 sigue siendo válido en ZF con lógica clásica.

Esto es menos trivial y se explica en la sección 5 de División por tres - Sin embargo, aunque la construcción no implica ninguna elección, sí hace implican la ley del medio excluido.

Pregunta: ¿Existen intuicionista teorías de conjuntos en las que se puede demostrar $$\textbf{2}\times A\cong \textbf{2}\times B\quad\Rightarrow\quad A\cong B\quad\text{?}$$

Por ejemplo, ¿es cierta esta afirmación en los topoi elementales o puede demostrarse en alguna teoría de tipos intuicionista?

En su comentario a continuación Kyle indicó que la declaración es indemostrable en algún tipo teoría - ¿alguien sabe el argumento o una referencia para eso?

Editar Véase también la pregunta relacionada En $A\times A\cong B\times B$ implica $A\cong B$ ? sobre "raíces cuadradas

Answer 1

Recientemente se ha publicado un artículo en arXiv sobre esta cuestión: Swan, Sobre la división por dos en las matemáticas constructivas .

Resulta que hay ejemplos de topos en los que no se puede dividir por dos.

Answer 2

(Lo que sigue no es realmente una respuesta, o sólo una muy parcial, pero sin duda es pertinente y demasiado larga para un comentario).

Existe un teorema de Richard Friedberg (" La unicidad de la división finita para las clases de equivalencia recursivas ", Matemáticas. Z. 75 (1961), 3-7) que dice lo siguiente (todo ello en lógica clásica):

Para $A$ y $B$ subconjuntos de $\mathbb{N}$ define $A \sim B$ cuando existe una función parcialmente computable $f:\mathbb{N}\rightharpoonup\mathbb{N}$ que es uno a uno en su dominio y definido al menos en todo $A$ tal que $f(A) = B$ . (También se dice que $A$ y $B$ son computablemente equivalente o equivalente recursivo y, de hecho, se trata de una relación de equivalencia, que no debe confundirse con "computacionalmente/recursivamente isomórfica", ver aquí .) Entonces [el teorema de Friedberg afirma]: si $n$ es un número entero positivo, entonces $(n\times A) \sim (n \times B)$ implica $A\sim B$ (aquí, $n\times A$ es el conjunto de números naturales que codifican pares $(i,k)$ donde $0\leq i<n$ y $k\in A$ para alguna codificación estándar de pares de números naturales por números naturales).

Para que esta afirmación se acerque más a la pregunta planteada aquí, los subconjuntos de $\mathbb{N}$ pueden considerarse objetos, de hecho subobjetos de $\mathcal{N}$ en el topos eficaz (un topos elemental con n.n.o. $\mathcal{N}$ tal que todas las funciones $\mathcal{N}\to\mathcal{N}$ son computables), de hecho, estos subobjetos son exactamente los clasificados por los mapas $\mathcal{N} \to \Omega_{\neg\neg}$ donde $\Omega_{\neg\neg} = \nabla 2$ es el subobjeto de los valores de verdad $p\in\Omega$ tal que $\neg\neg p = p$ Además, decir que dos de estos objetos son isomórficos, o internamente isomórficos, en el topos efectivo, equivale a decir que $A$ y $B$ son computablemente isomorfas como se ha indicado anteriormente. Así que el resultado de Friedberg puede reinterpretarse diciendo que si $A$ y $B$ son tales objetos del topos efectivo y si $n\times A$ y $n\times B$ son isomorfas, entonces $A$ y $B$ son.

No estoy seguro de hasta qué punto esto se puede interiorizar (por ejemplo, ¿valida el topos efectivo "si $A$ y $B$ son $\neg\neg$ -conjuntos estables de números naturales y $n\times A$ es isomorfo a $n\times B$ entonces $A$ es isomorfo a $B$ " de forma explícita $n$ ? y que tal para $n$ cuantificado dentro del topos?) o generalizado (¿realmente necesitamos $\neg\neg$ -). Pero puede que merezca la pena estudiarlo, y proporciona al menos una especie de respuesta positiva a la pregunta original.