Can we constructively find a third element of a set $X$ satisfying $X \cong X \times X$ given two distinct elements?
Consider a set $X$ such that $X \cong X\times X$. It's quite easy to prove in a classical set theory, e.g. ZF, that $X$ must be the empty set or a singleton set or an infinite set. In other words, if we additionally assume that there exists $a, b \in X$ and $a \neq b$, then we know that $X$ is an infinite set. In particular, we know that there exists an element $c \in X$ such that $c \neq a$ and $c \neq b$.
Problem
I believe that the (analogue of the) above statement does not hold in constructive set theories. Specifically, it doesn't hold in the internal logic of an elementary topos which is intuitionistic higher-order logic, or in something like the Calculus of (Inductive) Constructions, the type theory underlying Coq. I'm pretty confident that it doesn't hold in many other constructive set theories. Type theoretically, the claim is that $$\Pi X : \mathcal U.\Pi a, b : X. (X \cong X \times X) \land \neg (a = b) \to \Sigma c : X.\neg (c = a)\land \neg (c = b)$$ is not provably an inhabited type. I'm not claiming that it is uninhabited. Classical logic shows that it clearly can be inhabited. My claim is that it would also be consistent (albeit non-classical) to axiomatically assume that it is uninhabited.
I think the easiest way to refute the original statement would be via a countermodel, i.e. an elementary topos, that has an object that doesn't satisfy (the interpretation of) the above. Even nicer would be a (constructive) proof that the above implies the law of the excluded middle, but I don't think that's possible because I believe there are non-classical models that have inhabitants of the above type. I could be wrong though. (I'd be interested in explicit, ideally relatively simple to describe, examples of such non-classical models.) Of course, I could be wrong about the whole claim, so I would certainly also accept an inhabitant of the above type, preferably in a machine-checked system like Agda or Coq.
Additional Context
Here's the intuition for why I don't think this statement is provable constructively.
First, you can constructively prove that there are more than two distinct elements of $X$. Specifically, if $f : X \times X \to X$ is one half of the isomorphism, you can constructively prove that all of $f(a, a)$, $f(a, b)$, $f(b, a)$, and $f(b, b)$ are distinct. I have a machine checked proof of this in Agda. In fact, I have a machine checked proof that under the above assumptions $X$ is not "finite" for a strong sense of "finite", namely is isomorphic to a explicitly finite set aka "Bishop-finite". I'm pretty sure but have not proven in Agda that this is true for "finitely indexed" or "Kuratowski-finite" as well, i.e. there's a surjection from an explicitly finite set onto $X$.
Thus, the problem isn't that we can't find additional elements of $X$ constructively, but that we have no way of knowing which of those are distinct from $a$ and $b$. When you attempt to write a term for the above type, it quickly becomes clear that you have too little information, i.e. too few available operations on $X$, to actually show that, say, $f(a, a)$ is distinct from $a$ or $b$. Sure enough, if we additionally assume that $X$ has decidable equality, then we can easily provide a witness (and I have an Agda term witnessing this). This means that a counter-example along the lines I described above will need to use an object which does not have decidable equality.
I think one promising place to look for countermodels is (modified) realizability toposes such as the effective topos or the closely related modified realizability topos. Power objects, e.g. $\Omega^\mathbb N$ where $\Omega$ is the subobject classifier, may be a good place to look as they readily satisfy the desired assumptions and lack decidable equality in non-classical toposes.
0 answers
0 comment threads