|
It all depends on what you mean by �brand new result�. If you take the classical viewpoint that every statement is either true or false and hence that once proved, a result is no longer new, then much of what we are doing will look like rewriting classical results. However, if you interpret a constructive theorem and its proof properly, then it is quite clear that, even if the statement of the theorem looks like something that is well known classically, both the properly�interpreted theorem and its proof are brand new.
Consider yet again the Picard theorems discussed above. The full constructive interpretation of PTp is this:
There is an algorithm which, applied to a holomorphic function � on D(0,1) and to two complex values omitted from the domain of �, computes the order ν of the pole that � has at 0.
I know of no proof of this statement other than the constructive one in [12] the theorem, as presented in my statement, is brand new. Moreover, that proof, while drawing on a classical proof of the classical Picard theorem for inspiration, is also new.
Similarly, we have the constructive interpretation of PTs:
There is an algorithm which, applied to a holomorphic function � on D(0,1) , the data showing that � has an essential singularity at 0 (that is, the sequence of Laurent coefficients of � which contains infinitely many negatively indexed terms), and two distinct complex numbers ζ and ζ′, computes a complex number z and shows that either � (z) = ζ or � (z) = ζ′.
Once again, this is a brand new theorem, nowhere found (to my knowledge) in the classical literature; and once again, its proof is also new.
There are aspects of constructive mathematics that are clearly new, in that the classical mathematician would see nothing to prove where the constructive mathematicians does. For example, many theorems of constructive analysis require a certain subset S of a metric space X to be located, in the sense that the distance
ρ(x,S) := inf { ρ(x,s) : ∈ S }
exists (is computable). Proving that S is located may be a nontrivial matter. This is related to the failure of the classical least�upper�bound principle. For the constructive existence of the least upper bound of a nonempty subset S of R that is bounded above we need the additional condition (it is both necessary and sufficient) that S be order located: that is, for all real α, β with α < β, either β is an upper bound of S or else there exists s ∈ S with s > α. (Note that the �or� here is decidable: in constructive mathematics, to prove the disjunction p ∨ q, we must either produce a proof of p or else produce a proof of q.)
|
