Gleason's theorem is not constructively provable (Q2366249)

Gleason's theorem characterizes the possible generalized probability measures \(\mu\) on the closed subspaces \(A\) of a Hilbert space \({\mathcal H}\) of dimension three or greater. They are given by the quantum mechanical pure and mixed states, that is, for any such \(\mu\), there exists a positive selfadjoint operator \(W\) of trace class such that \(\mu(A)= \text{Tr} (\text{WP}_ A)\), where \(\text{P}_ A\) is the projection operator of \({\mathcal H}\) onto \(A\). In addition to ruling out non-contextual hidden variables, the theorem is central in determining how probability can be introduced into quantum mechanics. This paper shows by reduction that even the weakest restriction of the theorem to the unit sphere of the real Hilbert space \(\mathbb{R}^ 3\) is not constructively provable in the sense of Brouwer or Bishop, i.e. by intuitionistic reasoning. The theorem is shown to reduce to the lesser halting problem. This partially answers an open problem posed by Douglas Bridges. It does not say whether any viable constructivist substitute for Gleason's theorem is possible.