[FOM] classical/constructive mathematics

[A. Mani]

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. 

Best

A. Mani


-- 
A. Mani
Member, Cal. Math. Soc