[FOM] Alternative Foundations/philosophical

[joeshipman at aol.com]

There are two quite different issues: representing ZFC in the alternative foundations, and representing the alternative foundations in ZFC.


Conway's main point, in my opinion, was that a mathematician with good intuition ought to be able to proceed without providing a rigorous translation of everything he does into ZFC, because the kinds of formalisms he had in mind were (to those with maturity and experience) obviously representable in ZFC (possibly with some standard large cardinal axioms), and demanding that the representation be explicitly provided would be as unreasonable as demanding that an algorithm be translated into Turing machine code.


As I have said before, mathematicians behave as if there is a "Zermelo's thesis" analogous to the Church-Turing thesis, that every correct proof can be formalized in set theory just as every effective procedure can be represented as Turing machine code. Although mathematicians don't have automatic compilers translating between formalisms that are as good as the ones the computer scientists have, I think progress is satisfactory.


Since Conway is only contemplating mathematicians making alternative foundations for the math they want to do without being forced to formalize in ZFC, and not creating a alternative foundation for ALL of mathematics, the issue of representing ZFC in the alternative foundational schemes does not arise for him.


The claims of the proponents of Homotopy Type Theory (the currently fashionable alternative foundation) are bolder; they seem to be that (1) HTT is more natural than ZFC for research in certain areas of mathematics (2) HTT is more amenable to mechanical formal verification than ZFC (3) ZFC can be represented in HTT. 


In my view, (1) seems plausible and (2) seems doubtful, and I'd like to see the details of (3). However, the real question (taking bi-interpretability for granted) should be:


What fraction of mathematical research can be more easily formalized in HTT than in ZFC?


This is what ought to influence which "foundation" is taught to mathematics students. 

-- JS


-----Original Message-----
From: Harvey Friedman <hmflogic at gmail.com>
To: Foundations of Mathematics <fom at cs.nyu.edu>
Sent: Wed, Feb 26, 2014 8:37 pm
Subject: [FOM] Alternative Foundations/philosophical


I agree with a great deal of what Chow has just said. However, I have some problem with a full endorsement of the following from his message:
\
"I am sympathetic to John Conway's "Mathematicians' Liberation Movement" 

(which of course has also been discussed before on FOM), which basically 
says that we're mature enough now to be able to pick whatever foundations 
we find convenient, knowing that we can always, in principle, translate 
between any two if them if we really want to.

In other words, if a proponent of a new system claims certain advantages 
over the old system, I do not think the reaction should be to get all 
defensive and say, "But I can do that with the old system too!"  Instead, 
one should open-mindedly explore if the new system helps foster new ideas 
that advance the field.  The sooner we abandon childish turf wars, the 
faster mathematics (and the foundations of mathematics) will advance."
There are two aspects of the usual foundations that are generally accepted (or are they generally accepted?).
1. There is a crucial kind of absolute rigor in the presentation.
2. There is a completely transparent elementary character that is relatively universally understandable. 
3. There is a precious kind of philosophical coherence that transcends mathematics itself. 
4. It has been used in order to address the obvious great fundamental methodological issues, the most well known of which concern whether or not propositions can be proved or refuted - both generally and specifically.
A certain amount of this would also be a priori clear for an alternative foundation if that alternative foundation was in an appropriate sense interpretable in the usual foundation. However, such an interpretation is generally not nearly enough to ensure 2.
How do 1-4 fare with alternative foundations?
With regard to the "liberation Movement", if one is concerned with fully complete rigorous presentations, then has history shown that generally speaking one either doesn't have this at all, or one has it done incorrectly, replete with inconsistencies?
Isn't an example of this kind of thing, the idea of using general category theory as an alternative foundation, with the "liberated" use of things like the category of all categories? Hasn't that been recently shown to lead to convincing inconsistencies within the usual mindset of general category theory?


Also, has there been a philosophically coherent presentation of altered notions of equality? If so, the FOM would benefit greatly from seeing this discussed.

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/20140226/0efe984f/attachment-0001.html>