[FOM] Philosophical coherence and foundational role of set and type theory

[Sam Sanders]

Dear Harvey, dear FOM,

I am not a specialist in set or type theory, but let me make the 
following observations about the discussion regarding ZFC vs HoTT:

Important aspects of a foundation of mathematics would seem to include:

1) simplicity:  The axioms of ZFC are fairly easy to write down and have fairly easy intuitive motivations.  

By contrast, type theory (of any variety) seems to require more effort to comprehend/motivate initially.  

2)  bedrock status:  By definition, a foundation is/should be the most elementary level, the bedrock.  Now,
the axioms of ZFC are about sets (with the notion of rank/type implicit, as observed by Scott on the FOM before), 
and all of math is represented by sets.  

By contrast, the syntax and semantics of type theory is usually expressed using set theory, although there has 
been attempts to ‘internalise’ type theory.  (Google “type theory should eat itself”) 


If one believes that “philosophical coherence” includes any of the two previous aspects, then ZFC seems to win
over any type theory in terms of this notion (whatever it means btw).


HOWEVER, it must be acknowledged that HoTT tries to make real progress regarding 1) and 2):

Firstly, the univalence axiom is motivated by the idea that mathematicians in practice identify isomorphic structures.  

One can debate whether this should *always* be done, or whether it really only works well in certain sub-fields of math.    
For instance, perhaps mathematicians have a more “dynamic” approach to syntax where *sometimes* isomorphic structures
are identified, but not in other cases where this would be problematic. (Compare this to how the level of detail and rigour 
vary wildly even throughout individual proofs)   

One can debate whether the univalence axiom has general merit besides trying to reflect mathematical practice in subfields, 
and clarifying the notion of equality in MLTT.  


Secondly, the internalisation of type theory, i.e. the representation of syntax and semantics of type theory in type theory 
is a lively research area, and HoTT has led to new models and interpretations of syntax and semantics.  Nonetheless,
the internalisation of type theory is very much an open problem, and the existing partial solutions are rather technical (to the best of my non-expert knowledge)


In conclusion, Harvey would seem to be right in asking for a simple example where the univalence axiom (or the internalisation of type theory)
really offers something new vanilla ZFC cannot.  

Best,

Sam

> On 30 Mar 2016, at 22:20, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> I looked some at
> 
> https://en.wikipedia.org/wiki/Univalent_foundations
> 
> https://en.wikipedia.org/wiki/Homotopy_type_theory
> 
> As I expected, I could not find a single example of any of the following:
> 
> 1. Some issue in f.o.m. that is not being addressed by the usual f.o.m.
> 2. Some issue in f.o.m. that is being addressed by type theoretic f.o.m.
> 
> I see some new algebraic/topological type interpretations of type
> theories, and the like.
> 
> Although it wasn't clear from these articles, I could imagine that
> there is some kinds of type theories for which it is not at all
> obvious that one has any mathematical model, or even that one has any
> model at all in any reasonable sense.
> 
> So the impression one inevitably gets is that this stuff is
> 
> a. A framework for doing some new kinds of abstract categorical
> algebra/topology that is exciting to very abstractly minded
> mathematicians.
> b. A complicated solution in search of a foundational problem.
> 
> So I repeat my suspicion and therefore my challenge.
> 
> Anything that can be done with this kind of "foundations" can be done
> much more simply and much more powerfully and much more effectively by
> sugaring the usual f.o.m.
> 
> But I can't start backing this up, and others cannot really challenge
> me, until they state a crystal clear foundational issue that they
> think is not or cannot be addressed in standard f.o.m., and that is
> addressed in this exotic f.o.m.
> 
> One thing that does not seem to be in doubt, correct me if I am wrong.
> This exotic f.o.m. is much more complicated than standard f.o.m.
> 
> Perhaps we should start with a simpler question.
> 
> What foundational issue is addressed by even ML type theory - no
> univalence axiom - that cannot be more simply and better addressed by
> standard f.o.m.?
> 
> Let me close with a methodological question.
> 
> What standards should be applied by proposing to replace an existing
> system with another system that is massively more complicated?
> 
> My answer of course as you see, is to ask for careful generally
> understandable explanations as to what is to be gained. There also
> needs to be a major effort made to see if the existing much simpler
> system already can be used to address the issues, whatever they are,
> adequately, or maybe even better.
> 
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom