[FOM] classical/constructive mathematics
a_mani_sc_gs at yahoo.co.in
Fri Oct 17 11:40:21 EDT 2008
On Wednesday 15 Oct 2008 10:06:36 Harvey Friedman wrote:
> An apparently closely related fact about HA is purely formal. HA
> possesses a great number of properties that are commonly associated
> with "constructivism". The early pioneering work along these lines is,
> if I remember correctly, due to S.C. Kleene. Members of this list
> should be able to supply really good references for this work, better
> than I can. PA possesses NONE of these properties.
> RESEARCH PROBLEM: Is there such a thing as a complete list of such
> formal properties? Is there a completeness theorem along these lines?
> I.e., can we state and prove that HA obeys all such (good from the
> constructive viewpoint) properties?
HA appears reasonable, but Markov's principle (*) does not follow (Of course *
can be debated).
A stronger reason for doubts on HA being sufficient is in the nature of
negation in constructive mathematics. We want \neg A to be like A \rightarrow
\bot. But unless \bot is defined by constructive means to encompass all
kinds of contradiction, it will not be genuinely constructive. HA does not
seem to be capable on the point. ("\neg A" should NOT be "A \rightarrow
0=1" by definition). In constructive mathematics, the concept of negation
should be subject to persistent revision.
Member, Cal. Math. Soc
More information about the FOM