Gleason, Kochen–Specker, and the model existence game

The Kochen–Specker theorem shows that certain finite sets of rays admit no assignment of the values 0 and 1 compatible with orthogonality. We prove Gleason’s theorem and a strengthening of the Kochen–Specker theorem in infinitary real-valued logic. In this logic the probability of a quantum proposition is the value of a formula. The hypothesis that every probability is 0 or 1 fails in every model of a countable theory. The standard models of this theory are the separable infinite-dimensional complex Hilbert spaces with a density operator. In them, every hypothesis that the probabilities avoid a nonempty Borel or σ-projective subset of [0,1] fails as well. In place of compactness we use model-theoretic forcing, cast as a two-player topological game. The game yields finite obstructions that constrain the probabilities themselves. They identify the axioms on which each refutation rests. They exist even when every finite set of axioms has a model.