Constructive mathematics and quantum mechanics: Unbounded operators and the spectral theorem (Q1802394)

One of the main ideas behind constructive mathematics is its algorithmic nature: if we can prove the existence (e.g., a solution to an equation) in constructive mathematics, then we automatically have an algorithm that generates the desired solution. In view of that, every time we want to compute something, it makes sense to reformulate the problem in terms of constructive mathematics. In the paper under review, this idea is applied to quantum mechanics. The two main notions of quantum mechanics are the notion of a state that describes a system, and the notion of an observable that describe measurements. In traditional mathematical formulation of quantum mechanics, states are represented as vectors in a Hilbert space \(L^ 2\), and observables are represented by operators from \(L^ 2\) to \(L^ 2\). For the majority of physical observables (including coordinates, momentum, energy, etc.) the corresponding operator is unbounded. Measurement of an observable \(A\) in a state \(s\) is described as follows: as an answer, we can get any eigenvalue \(\lambda_ i\) of \(A\) with the probability \(| (s,\psi_ i )|^ 2\), where \(\psi_ i\) is the corresponding eigenvector. Computing these probabilities is one of the main computational problems of quantum mechanics; therefore, it seems reasonable to apply constructive mathematics to this problem. If we can find the constructive proof of the spectral theorem, then we would be able to compute \(\psi_ i\), \(\lambda_ i\), and therefore, the desired probabilities. There is already a constructive functional analysis, so all the necessary definitions (of a constructive operator, etc.) are already in place. The author shows, however, that with these definitions, the spectral theorem is \textit{not} constructive, and so, there is no algorithm to compute the desired probability. The fact that physicists are able to compute these probabilities means that probably a different version of constructive mathematics is necessary to describe this situation. Alternative constructive definitions of an unbounded operator (more suited for the use in quantum mechanics) have been proposed by \textit{O. M. Kosheleva} and the reviewer [e.g. in ``On the algorithmic problems of a measurement process'', Res. Rep. Philos. Phys., Univ. Toronto, Ontario, Canada, Dep. Philos. No. 5 (1978), and in ``What can physics give to constructive mathematics'' (in Russian), Math. Logic Math. Linguistics, Kalinin 1981, 117-128 (1981)].