Andrew Swan: Constructive mathematicians can't even divide by 2

Abstract: It's easy to see in ZFC that if $X \times 2$ is in bijection with $Y \times 2$, then $X$ is in bijection with $Y$. It is harder to show this in ZF without choice, but still possible, as originally shown by Bernstein. If we really work constructively, i.e. without the law of excluded middle, then it is not possible. By examining a proof of "division by 2" by Sierpiński we can show that any constructive proof would need to also be equivariant under a certain group action. With a bit more work we can give an example of a topos where it is not possible to divide by 2.

The seminar now has a homepage with the planned talks for the entire semester: https://mathematical-conversations.splet.arnes.si/