What does it take to divide by $2$?

Theorem 1 [ZFC, classical logic]: If $A,B$ are sets such that $\textbf{2}\times A\cong \textbf{2}\times B$, then $A\cong B$.

That’s because the axiom of choice allows for the definition of cardinality $|A|$ of any set $A$, and for $|A|\geq\aleph_0$ we have $|\textbf{2}\times A|=|A|$.

Theorem 2: Theorem 1 still holds in ZF with classical logic.

This is less trivial and explained in Section 5 of Division by Three – however, though the construction does not involve any choices, it does involve the law of excluded middle.

Question: Are there intuitionistic set theories in which one can prove $$\textbf{2}\times A\cong \textbf{2}\times B\quad\Rightarrow\quad A\cong B\quad\text{?}$$

For example, is this statement true in elementary topoi or can it be proved in some intuitionistic type theory?

In his comment below Kyle indicated that the statement is unprovable in some type theory – does somebody know the argument or a reference for that?

Edit See also the related question Does $A\times A\cong B\times B$ imply $A\cong B$? about ‘square roots’


There was a paper recently posted to arXiv about this question: Swan, On Dividing by Two in Constructive Mathematics.

It turns out that there are examples of toposes where you can’t divide by two.

Source : Link , Question Author : Hanno , Answer Author : aws

Leave a Comment