[FOM] Alternative Foundations/philosophical

[Dominic Mulligan]

Harvey Friedman quoting various experts wrote:

> "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."

A rather contentious claim. The likes of Isabelle, HOL4, HOL-Light and
other systems in the HOL family have amply demonstrated that there is
absolutely no need to move to "sophisticated type theories" to be able to
successfully formalise great swathes of mathematics and computer science.
The type system of a typical HOL system is pedestrian even by 1970s
programming language theory standards. In fact, it seems to me that one of
the main lessons to be drawn from systems like Isabelle is that keeping
your types as simple as possible is a boon from a practical point of view.

Regards,
Dominic Mulligan


On 3 March 2014 01:42, Harvey Friedman <hmflogic at gmail.com> wrote:

> 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
>
>
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140305/35c5b0b0/attachment-0001.html>