Gleason’s theorem plays an important role in the foundations of quantum mechanics. On the positive side it demonstrates how the probabilistic structure of quantum theory follows from its logical structure, that is, the geometry of Hilbert spaces. On the negative side, the theorem puts a severe constraint on possible hidden-variable interpretations of quantum mechanics.
My interest in it arose from a note by Robert Solovay ``Gleason’s Theorem for non-separable Hilbert spaces: Extended abstract '', who proved a similar result for non-separable Hilbert spaces. The point is that the proof uses forcing.
I realized the result has more connections with set theory in fact:
The Theorem of Gleason for Nonseparable Hilbert Spaces: The Gleason theorem is proved for nonseparable Hilbert spaces under the assumption of the continuum hypothesis.
A Boolean-valued approach to Gleason's theorem: Using the Boolean-valued method, the author proves Gleason-type theorems for the projection lattice of an $AW^∗$-algebra without $\mathcal{I_2}$ summands of type $I$.
Question 1. Are there any detailed proofs of Solovay's result avalable?
I am also interested to know if there are any proofs of Solovay's theorem without the use of metamathematical tools.
Question 2. Does Solovay's result has any applications similar to those of Gleason's original result?
