7
$\begingroup$

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?

$\endgroup$
9
  • $\begingroup$ It might make sense to start first with Frobenius’s more familiar trichotomy of finite-dimensional real division algebras, which someone may have considered from a constructive perspective already. But maybe no one has found much to say: papers on nearby topics, eg arxiv.org/abs/2102.12775, don’t mention it. $\endgroup$
    – user44143
    Feb 28, 2022 at 13:40
  • $\begingroup$ @MattF. That paper on central simple algebras talks about central simple algebras over discrete fields, so the paper does not apply to any algebra over the real numbers, since the real numbers are not a discrete field. $\endgroup$
    – user173426
    Feb 28, 2022 at 15:13
  • $\begingroup$ Agreed — I only called it a nearby topic! $\endgroup$
    – user44143
    Feb 28, 2022 at 15:26
  • $\begingroup$ @MattF. Also, if Andrej Bauer's answer below is correct, I would also expect Frobenius's trichotomy of finite-dimensional real division algebras to fail in constructive mathematics, because, as usually stated, it would also imply excluded middle. $\endgroup$
    – user173426
    Feb 28, 2022 at 15:28
  • 1
    $\begingroup$ That is just a motivation to find a more constructive statement than the usual. Eg perhaps Frobenius’s theorem or Soler’s theorem can be proved constructively as “any $X$ can be put in a canonical form of $Y$ with an infinite series of $e_i$; if the $e_i$’s are all 0 then $X=\mathbb{R}$, if the first non-zero $e_i$ is positive then $X=\mathbb{C}$, and if the first non-zero $e_i$ is negative then $X=\mathbb{H}$.” That would be a satisfying constructive version. $\endgroup$
    – user44143
    Feb 28, 2022 at 15:41

1 Answer 1

9
$\begingroup$

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.

$\endgroup$
4
  • 2
    $\begingroup$ Instead of strengthening the hypotheses one might also weaken the conclusion. For example, if the question is about subfields of $\mathbb{C}$ containing $\mathbb{R}$, one might ask whether they're all of the form $K_p$ for some $p\in\Omega$, which classically means exactly that they're $\mathbb{R}$ or $\mathbb{C}$ but constructively gets rid of your objection: or generally speaking, try to find a family parametrized by (maybe several) elements of $\Omega$ which classically covers all classification cases and constructively covers all possibilities. I don't know if this is possible! $\endgroup$
    – Gro-Tsen
    Mar 1, 2022 at 10:37
  • 1
    $\begingroup$ Right, that's another standard move. $\endgroup$ Mar 1, 2022 at 12:29
  • 3
    $\begingroup$ I'm confused about "amounts to" in "stating that, for all $p$, $K_p$ is either $\mathbb R$ or $\mathbb C$ amounts to $p\lor\neg p$." The right-to-left implication was proved in the immediately previous sentence, and it's clear that if $K_p=\mathbb C$ then $\neg p$. But is it supposed to be clear that if $K_p=\mathbb R$ then $p$? That seems to require getting all (or at least "enough") truth values to be of the form "$z\in\mathbb R$" for some complex $z$, and I don't immediately see how to do that. $\endgroup$ Mar 1, 2022 at 14:53
  • 1
    $\begingroup$ @AndreasBlass: Yes, that is a problem, thanks for catching it. I rephrased, hopefully correctly. Still an interesting question remains: given a proposition $p$, can we define a subfield $K_p \subseteq \mathbb{C}$ such that $K_p = \mathbb{R} \iff p$? How about getting $K_p = \mathbb{C} \iff p$? $\endgroup$ Mar 1, 2022 at 19:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.