Is Solèr’s theorem true in constructive mathematics? Solèr’s theorem says that for every star division ring $R$ and every $R$-module $H$ with an orthomodular Hermitian form $\langle (-),(-) \rangle:H \times H \to R$ such that there exists an infinite orthonormal sequence $e:\mathbb{N} \to H$, $R$ is either the real numbers $\mathbb{R}$, the complex numbers $\mathbb{C}$, or the quaternions $\mathbb{H}$, and $H$ is a Hilbert space over $R$. Assuming that the star division rings used are Heyting division rings (or else Solèr’s theorem is most likely false), is Solèr’s theorem true in constructive mathematics?
 A: Suppose you have a classical classification theorem saying

Each structure (of a certain kind) is either an $A$ or a $B$.

Then you cannot exhibit constructively a $C$ which is neither $A$ nor $B$ because every constructive proof is also classical, and so that would contradict the classical classification.
What happens instead is that the classical meaning of “$p$ or $q$” corresponds to the constructive “not ($\neg p$ and $\neg q$)“ so the constructive reading of the classical classification theorem is

Apart from $A$ and $B$, there is no other structure (of a certain kind).

To give you an idea on how to play tricks with excluded middle in constructive mathematics, consider any proposition $p$ and define
$$K_p = \{ z \in \mathbb{C} \mid p \Rightarrow z \in \mathbb{R} \}.$$
It is easy to check, regardless of what $p$ is, that $K_p$ is a subfield of $\mathbb{C}$.
Moreover, if $p$ holds then $K_p = \mathbb{R}$, and if $\neg p$ holds then $K_p = \mathbb{C}$. But stating that $K_p$ is either $\mathbb{R}$ or $\mathbb{C}$ implies $\neg \neg p \lor \neg p$, which lets us decide $\neg p$, which is not generally possible in constructive mathematics. It is still the case that $K_p$ cannot be different from both $\mathbb{R}$ and $\mathbb{C}$, because that amounts to $\neg (\neg p \land \neg\neg p)$, which is constructively true (obviously).
Consequently, if Solèr’s theorem were true constructively (in the version that says that every structure is either this or that), we could decide $\neg p$: just ask the theorem to classify $K_p$ for you.
The usual solution to the conundrum is to strengthen the assumptions to something that does not matter classically. For example, you might want to assume that the vector space $E$ featuring in the definition of a Hermitian form has a given basis, and that the basis has size which is either a natural number or is countably infinite (this cannot be shown to hold for $K_p$ above seen as a real vector space). But that is only the first step, there will be further complications, and one would have to dig into the details of the classification theorem. Unfortunately, I do not know whether anyone has done so.
