FOM: RE: human well-being; constructivism; anti-foundation

[Matt Insall]

Matthew Frank said:
``I would argue that working on Bishop-style mathematics brings more
conceptual benefits to classical mathematics than working on other
varieties of constructive math.''

My response:
     I do not use Bishop-style mathematics, but I believe that I see a value
in it.  You did not give details, but I will explain what I think are the
values of at times using such restrictive logic systems.  (Warning:  Some
fairly subjective speculation about some things in the culture and practice
of mathematics is included below.)  To me, the formal structure of an
argument is frequently not any more important than the intuitive content of
the result and of the methods of proof and of the statements in the proof.
Thus, although (I would like to think) I am capable of reading a formal
proof, from the axioms for Zermelo-Fraenkel set theory and some formalized
definitions of topological spaces and related notions, of a theorem like the
Tychonoff theorem that products of compact spaces is compact, I would
probably prefer to read the proof written in a natural language.  (In fact,
although my native language is English, I would perhaps prefer to read the
proof in French, rather than in full-blown formalization in a first order
language for Zermelo-Fraenkel style set theory.)  My preference is not only
due to aesthetic considerations, but it is due to the fact that there is
apparently some intuitive understanding that can benefit me in finding or in
understanding other results.  Now, this appears to be the case for me in
using classical first-order (or perhaps some higher-order) logic that
includes the law of the excluded middle.  The value I see in restricting the
use of the law of the excluded middle is that, although (yea, even because)
the proofs obtained are longer, there is more explanation provided to my
intuition about why (in what I guess is referred to as a Neo-Platonic sense)
the given result is (again in a Neo-Platonic sense) true, specifically
because the proof's author must work harder to obtain a proof of the desired
result.  I understand that from a formalistic point of view, this may not be
considered to be very significant.  But if one is to be a serious formalist
about this, one can consider the application of ``intuition'' at certain
points to be a form of ``conjectural development'', to which formal methods
are to be later applied as a type of verification procedure by a formal
prover or a formal proof-checker.  In this sense, Bishop-style proofs,
whether one is a practicing Bishop-style mathematician or not, can help the
entire mathematical community to find more truth in a way that is similar to
what I think is currently modelled by non-monotonic reasoning systems.  (For
example, I have seen some uses of a theorem-prover called ``Otter'', in
which some form of resolution is used, but certain not-yet-proved results
are treated in a way similar to our use of conjectures in mathematics.  What
I perceived as a ``non-monotonicity'' was that the ``set of support'' does
not just grow over time, but sometimes becomes smaller, as some conjectures
are rejected, and some lemmas are deemed unnecessary.)  Thus, a coupling of
all the different methods and forms of proof (from different logic systems)
can be beneficial in a technical sense by providing more ``food for
thought'' to the minds that are working on the problems.  I am sure that
even some automatic theorem-provers will eventually take an even more
similar (to mathematical practice) approach, in an effort to model the
conjectural/speculative aspects of mathematical and scientific culture as
well, and in concert with, the formal proof-oriented aspects of mathematical
culture.  In fact, I am sure that several systems already do some of this.
I also am fairly certain that in addition to speeding up computations to try
to compensate for restrictions due to complexity and long proof issues, such
systems will at times work to slow down some computations by obtaining
longer proofs that provide more detailed information, and systems based upon
logics that deny the law of the excluded middle will play a significant role
in this, as will also logics that use the law of the excluded middle.




Dr. Matt Insall
http://www.umr.edu/~insall