Bas Spitters
As an illustration of the use of proof mining we extract a constructive proof of the Riesz representation theorem out of the classical proof. This allows us to generalize the theorem to valuations on locales and to apply it in the context of non-commutative integration theory --- the foundations of quantum mechanics.
|