[FOM] classical/constructive mathematics

A. Mani 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. 


A. Mani

A. Mani
Member, Cal. Math. Soc

More information about the FOM mailing list