FOM: constructive math

[Matthew Frank]

Some overdue responses to posts on constructive math May 31-June 8 by
Davis, Forster, Richman, Schuster, Simpson.  In chronological arrangement
for lack of a better one....

May 31:  Steve Simpson wanted to know about the philosophy that underlies
Bishop-style mathematics, later clarifying philosophy was to be understood
as "the broadest principles of all".  I can answer only for the philosophy
that underlies my pursuit of Bishop-style math.  The philosophy of math is
formalism; I think formalists should be interested in constructive math,
because among alternatives to the standard formalisms (ZFC and the like),
I know of none which comes with such a rich set of intuitions, or which
interfaces in such an interesting way with many areas of mathematics.  
The broader philosophy that underlies my formalism sees all statements
(about physics, about ethics, etc.) as following from certain assumptions
which are not themselves to be evaluated as true or false.  This is pretty
broad, broader than I would want to defend in this forum, and I suspect
that most people in Bishop-style math would distance themselves from it.

Also in his posting of May 31, Simpson said "Bishop has stated (rather
vehemently) that nonconstructive existence proofs constitute fraud"; if
Bishop actually used the word "fraud", I'd like to see a reference.

June 4:  Peter Schuster asked about relating intuitionist logic to
temporal and epistemic logic.  Dirk van Dalen's discussion of Beth trees
does a bit of this, at least in a suggestive way.  (Handbook of
Philosophical Logic, vol. III (Alternatives to Classical Logic), pp.
225-339 ("Intuitionistic Logic"))  (Tom Forster suggested something
similar to this in his post, also June 4.)

June 6:  I enjoyed Martin Davis's challenge about his non-constructive
proof.  Here's my response (from the perspective of someone interested in
constructive math, not from the perspective of a "committed
constructivist"):  Davis gave a classical argument showing that "there are
diophantine relations whose negations are not diophantine".  
Constructively, this argument only shows that "not all diophantine
relations have diophantine negations".  Even this analogy with the
recursively enumerable relations might have been enough to encourage the
research Davis mentioned.  One would also have wanted to know whether the
original classical claim could be proved constructively, and so one would
have looked to examples.  One good test case would have been the r.e.,
Diophantine relation "x is not a power of two" (i.e. {x: x=y(2z+3) for
some y,z}), and seeing whether its (obviously r.e.) negation "x is a power
of two" was Diophantine--just the problem that Alfred Tarski had posed to
Julia Robinson, and got her started on these issues....

June 8:  Fred Richman made an interesting comment,
> I hate to be classified as liberal (and would never use the phrase
> "epistemically-accessible"). Perhaps "aphilosophical" instead of
> "liberal". I've explained why I like constructive proofs: they
> justify the computational interpretation of the theorems. I don't
> have to have a position on the nature of mathematical reality.
> Nevertheless, if you operate in a constructive framework, your view
> of mathematical reality will no doubt be colored by that experience.

I am amused because I disagree so much with the first part (I am happy to
be classified as liberal, do talk about epistemic access, and consider
myself philosophical), and agree so much with the second.

--Matt