Nonstandard analysis and constructivism? (Q1119637)

The author admits that certain aspects of this paper are speculation. This speculation is not relative to the author's proved results, however. The speculation refers to whether or not constructivists will, some day, accept certain aspects of nonstandard analysis as constructive in character. This comes from the obvious relation between the first-order properties associated with the finite and the \({}^*finite\). In order to aid in such a determination, the author has investigated certain nonstandard proofs of the constructive versions of the Intermediate and Extreme Value Theorems. In order to remove certain ``glaring nonconstructive elements,'' he inductively defines certain standard sequences that when extended to \({}^*finite\) sequences allows him to eliminate the standard part operator from a nonstandard proof of the constructive version of the Intermediate Value Theorem. The basic tool the author utilizes in order to give a constructive type of proof for the Extreme Value Theorem is a result he establishes for a compact metric space. He shows that a space X is compact iff there is a standard sequence \(x_ 1,...,x_ n\) in X such that for every infinite \(N\in^*{\mathbb{N}}\) and every \(x\in^*X\) there is an \(n\leq N\) such that \(x_ n\approx x\), where \(\approx\) is the author's extension of the infinitely close concept. The author calls such a standard sequence a finite approximation of X. However, following the author's own admission, since he uses the standard part operator, this proof would not be considered as approximating a constructive proof. Nevertheless, the author presents, as his final result, what he states is a completely ``constructive'' proof of the Extreme Value Theorem employing a finite approximating sequence. The actual structure of the proof itself is constructive in character. However, the use of a result that is obtained by a nonconstructive process tends to refute its completely constructive character. Thus as the author states, ``These ideas are still highly speculative, but nonetheless suggestive.'' From the view of nonstandard analysis, the author does give some interesting refinement to the customary methods.