[FOM] Alternative Foundations/philosophical

[Bas Spitters]

Thanks for the clear questions:

(1) The surreal numbers can be conveniently formalized in the univalent
foundations.
In fact, the new "higher inductive types" seem to capture Conway's proposed
system quite closely.
http://books.google.nl/books?id=LkDUKMv3yp0C&pg=PA342

The book contains a list of examples from homotopy theory, algebraic
topology, ... which can be proved synthetically.
I.e. homotopy type theory makes precise the following idea:
"Grothendieck came along and gave us a new dream of what homotopy types
might actually be. Very roughly, he realized that they should show up
naturally if we think of "equality" as a process--the process of proving two
things are the same--rather than a static relationship."
"It will take about a century for the effects of [homotopy type theory] to
percolate through all of math."
http://johncarlosbaez.wordpress.com/2014/02/18/finding-and-solving-problems/

(2). Type theory is the theory underlying many modern proof assistants
(Coq, agda, NuPrl, ...). Homotopy type theory fixes many of the issues that
made type theory less attractive to mathematicians. More positively, it
provides a language for weak oo-groupoids, the generalization of set theory
which Grothendieck pointed to.
Type theory is an important part of programming language design. This field
was simply non-existent when ZFC was developed.

(3) We verified Lawvere's axioms for set theory:
http://books.google.nl/books?id=LkDUKMv3yp0C&pg=PA342

As usual, this allows us a cumulative hierarchy of sets by a sets-as-trees
interpretation. We get a model of ZFC:
http://books.google.nl/books?id=LkDUKMv3yp0C&pg=PA359

I am using google books for easy reference. However, the book is also
freely (CC-BY) available from:
http://homotopytypetheory.org/book/

Finally, please note the carefully phrased:
"We believe that univalent foundations will eventually become a viable
alternative to set theory as the "implicit foundation" for the unformalized
mathematics done by most mathematicians."


On Thu, Feb 27, 2014 at 4:46 AM, <joeshipman at aol.com> wrote:

> 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 listFOM at cs.nyu.eduhttp://www.cs.nyu.edu/mailman/listinfo/fom
>
>
> _______________________________________________
> 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/20140228/9873a6dc/attachment.html>