FOM: Effective Bounds in Core Mathematics

[Fred Richman]

Harvey Friedman wrote:
 
> Under my suggestion, a constructivist would be defined as "someone who
> studies constructivity in mathematics, or constructive proofs". This is
> analogous to a proof theorist as "someone who studies formal proofs" or a
> topologist as "someone who studies topological spaces".

Is this a simple terminological dispute? I wasn't thinking of that at
all. I would be inclined to say that a constructivist is a
mathematician who systematically proves theorems without appeal to the
law of excluded middle. I might note that although I have never heard
of "proof theorism" or "topologism", people do seem to talk about
"constructivism", referring to a view of mathematics.
 
> I still don't see why it is attractive, or even reasonable, to take the
> point of view that I put in between *'s above. As I said before, it is
> counterproductive and needlessly provocative. Furthermore, it almost
> guarantees that most logicians and mathematicians will not study
> constructivity.

I don't see why the term "proof" must of necessity be reserved for
classical proof. In a thoroughgoing constructive development of
mathematics, the proofs would all be constructive. Theorems whose
proofs require the law of excluded middle would be so flagged in much
the same way as we sometimes flag theorems that use the axiom of
choice, the continuum hypothesis, or the Riemann hypothesis. The
constructivist program is to develop mathematics in exactly that way.
In such a context, the starred point of view is practically mandatory.

As for the last remark, constructivists are not particularly
interested in studying constructivity. They are interested in doing
mathematics in a constructive manner.

> Taking a counterproductive and needlessly provocative stance like * needs a
> justification such as this. Otherwise, it is just counterproductive and
> needlessly provocative.

May I point out that using the phrase "counterproductive and
needlessly provocative" so often is counterproductive and needlessly
provocative?

--Fred