|
Markov’s variety of the constructive mathematics is just what Bishop did plus the assumption that Church-Markov-Turing thesis holds. One does not need to assume that to recover any result of classical mathematics applicable in the real world. Also all those weird results of Markov’s approach that apparently “contradict” the classical mathematics is a consequence of Church thesis. Without that one cannot prove them. So Bishop’s approach is always compatible with classical mathematics. As for Hahn—Banach I can only site the book “Techniques of Constructive Analysis” by Douglas S. Bridges: For example, our proof of the Hahn-Banach theorem (Theorem 5.3.3) is, as it stands, a valid algorithmic proof of the classical Hahn Banach theorem. Moreover and this is one advantage of a constructive proof in general our proof embodies an algorithm for the construction of the functional whose existence is stated in the theorem. This algorithm can be extracted from the proof, and, as an undeserved bonus, the proof itself demonstrates that the algorithm is correct or, in computer science parlance, "meets its specifications".
… The Hahn-Banach theorem enables us to extend a normed linear functional, with an arbitrarily small increase in norm, from a subspace of a normed space to the entire space. This fundamental result has numerous applications throughout functional analysis. In the constructive context we deal only with the extension of linear functionals on subspaces of a separable normed space. The standard classical proofs extending the theorem to nonseparable normed spaces depend on Zorn's lemma and are therefore nonconstructive.
…
The classical Hahn-Banach theorem says that we can extend a bounded linear functional v from Y to a functional u on the whole space X with exact preservation of norm. In general, as Exercise 5 shows, we cannot do this constructively. But, as we shall see, if we impose extra conditions on the norm of X, then we can make the extension norm-preserving. |