[FOM] The Provenance of Pure Reason (II)

[Gabriel Stolzenberg]

   As I read the quote below from Bill Tait's "The Provenance of
Pure Reason," Bill is talking from within and about what, in my
previous message, I called, "classical constructive mathematics."
On this view, constructive math consists in seeing what one can
do without the law of excluded middle.  Period.  There are no
distinctively constructive concepts of 'existence' or 'function.'

    "In Tait [1983], I argued that constructive mathematics
     cannot be founded on a conception alien to classical
     mathematics...but that rather its basic concepts belong
     to classical mathematics.

     The argument given there, which I still endorse, is that
     these concepts are defined by the rules of proof governing
     them...and that the constructive rules of proof are a subset
     of the classical."

   1.  Bill's argument that the basic concepts of constructive math
"belong to" classical math seems to work equally well with the law
of excluded middle replaced by a version of Church's thesis that
implies the negation of the law of excluded middle.  Does this mean
that the basic concepts of constructive math belong both to classical
math and to this other system that is inconsistent with it?

   2.  It seems to follow from what Bill says that, when we consider
constructive math on its own, not as a part of something else, the
concept of existence is governed and defined by its own rules of proof.
But when we consider the imbedding of constructive math in classical
math (by extending the list of rules), doesn't the law of excluded
middle participate in governing the concept of existence?  And, if it
does, don't we have a different concept?

   3.  I assume that "a conception alien to classical mathematics"
refers to talk of "a procedure for constructing something" rather
than to the idea of an existence proof that doesn't use the law of
excluded middle.  If so, is it Bill's view that, if what I accept
as constructive rules of proof seem to clash with my intuitions
about procedures for constructing things---which is what I think
of my mathematics as modeling, I should ignore my intuitions and
stick with the formal rules?  Why?  Wny not consider changing the
rules?

   4. Just as constructive math can be represented as the part of
classical math devoted to seeing what can be done without the law
of excluded middle, classical math can be represented as that part
of constructive math devoted to seeing what follows from it.  Thus,
just as the formalism of classical math is adequate for writing
constructive proofs, the formalism of constructive math is adequate
for writing classical ones.  (Note. I am saying nothing here about
concepts, only formalisms.)

   Gabriel Stolzenberg