[FOM] Alternative Foundations/philosophical

[Harvey Friedman]

Chow wrote:

"Now we're getting into questions that I think are more interesting.

I think there are two different (albeit related) ways to measure whether
some piece of mathematics can be "easily formalized."  The first is how
much time and effort is required to produce the relevant bit of code in a
computerized proof assistant.  The second is how much time and effort is
required to convince oneself that the formalization can be carried out in
principle.  The two measures are correlated but not identical.  I admit
that I have never actually bitten the bullet and learned the details of
any specific proof assistant, but my general impression is that the
assistants that are based on type theory (not homotopy type theory) are
easier to work with than Mizar, the best-known set-theoretical assistant.
Is this impression correct?  If we assume this is true for the sake of
argument, then it's still not clear to me that these are the right
foundations to teach to students, unless we envisage them spending a lot
of time with a proof assistant in the future.  Conceptual simplicity seems
like it might be a more important criterion than engineering efficiency,
from a pedagogical point of view.  Now maybe type theory (or homotopy type
theory) wins on both fronts, but there are still separate questions here."

Here are some things that I have been told by various proclaimed
experts from various relevant fields.

"Practical general purpose programming languages need types, because
type checking is needed to develop software that can be debugged. We
need everywhere defined operations, which drives the need for type
checking. Partially defined operations are not a good idea - at least
an entire programming infrastructure has already been set up avoiding
partially defined operations. The same is true for formalization of
mathematics."

"The set theoretic foundations for mathematics is substantially
simpler than the alternatives based on types. However, attempts to use
the usual set theoretic foundations for mathematics make it impossible
- in the practical sense - to actually formalize abstract mathematics.
Hence the move to sophisticated type theories is necessary."

"Certain areas of abstract mathematics have now become sufficiently
far from rigorous in their current presentation that an urgent
critical need has arisen for formal verification. Without this effort,
certain areas of abstract mathematics will become impossible to
properly develop."

The usual foundations for mathematics is extremely powerful and
flexible, and supports all kinds of devices that seem to be second
nature only to those who have immersed themselves in it. Typical
elementary instances of this are the proper use of undefined terms and
abbreviations. It also has a profound kind of completely natural
philosophical coherence.

The proclaimed experts also claim that "alternative foundations for
mathematics is extremely powerful and flexible, and supports all kinds
of devices that seem to be second nature only to those who have
immersed themselves in it."

However, some issues still remain.

1. It appears that there is a substantial difference in complexity and
philosophical coherence. Some proclaimed experts will even agree with
this assessment, at least to some degree. These proclaimed experts
may, however, argue that it is not important, or not too important -
at least relative to what is gained.

2. In conversations about these matters, I have always asked for the
SIMPLEST IMPORTANT situation where the usual set theoretic foundations
is impossible to work with in a practical sense. I say that the burden
would then be on me to show how the usual foundations can be readily
adapted to do at least as good a job as alternatives. In each case, I
never got a sufficiently clear account of such a SIMPLE IMPORTANT
situation so that I could dig my teeth into how it could be properly
handled in the usual foundations.

I am not dug into uncritically accepting the way things are normally
done - and that includes the usual set theoretic foundations. On the
contrary, I see deep systematic flaws in almost every area of
intellectual activity that I am acquainted with - in terms of both
education and practice. This ranges from mathematics, statistics,
physics, law, politics, philosophy, music, chess, etcetera. But when
something really good comes along, like set theoretic foundations and
Bach, I can be supportive and enthusiastic.

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140302/f7f86967/attachment-0001.html>