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

[Astor, Eric P.]

Dear FOM:

I also am not a specialist in set or type theory - nor, I suppose, properly in f.o.m. itself. For what it's worth, I don't exactly have a horse in this race - I appreciate both the set-theoretic and type-theoretic perspectives on mathematics, coming as I do from a mixed background. However, I think I have two things to add, and one question.

Question: Harvey and other posters have mentioned on multiple occasions that they will gladly be held to the same standards as they wish to hold the type-theoretic position, in requesting clarity of terms and justification for major changes. My request: would someone care to propose a simple definition of "philosophical coherence" that is obviously satisfied by ZFC, but not so obviously satisfied by HoTT and other type theories? This would seem a useful point for debate, at minimum, and at best a good point on which to build discussion - for instance, it would allow proponents of type theory to explain how type theory is already coherent in this sense, or allow those skeptical of its value to show a clear benefit of the status quo.

I admit, I have no such definition to offer, so for this rest of this e-mail, I will continue in my own personal intuitive sense of the term.

Thing 1: In one sense, I agree that set theory and ZFC currently have clearer philosophical coherence - but only when considered at their core, absent the complexities of mathematics built on top of it. Insofar as ZFC provides foundations on which we build complex structures, I think that self-evident coherence quickly falls away - as we immediately drop consideration of the underlying set (at which level ZFC has such clarity) when discussing such structures, describing them purely by their behaviors. The identification of these structures built from sets with the "intuitive" or "Platonic" structures we have in mind (e.g., the identification of 0 as BEING the empty set) seems to lack the self-evident coherence that ZFC itself possesses - at least, not without accepting something that bears a remarkable resemblance to the univalence axiom!

Type theory appears to make a different trade-off - the structures we work with on a daily basis are now built and treated in an obviously coherent way, as our foundational language describes objects by their BEHAVIOR. Of course, by truly considering only the "externally visible" aspects of a structure, we begin to see why the univalence axiom might be coherent (or even required) in this context; objects that behave identically with regards to all external interfaces are, for all meaningful purposes, identified. (This in precisely the same sense in which standard set theory holds that sets that have the same elements are equal, discarding as external any "label" or interpretation we might place on said sets and elements.) This viewpoint renders the interaction of structures (including sets as a special, nearly-trivial case) self-evidently coherent - at the cost of a more complex, and possibly less clear, core.

One might of course argue that we could turn to set theory for the core, and use type theory as/to model our LANGUAGE... that is, we could deliberately adopt a layered f.o.m., where the language (and rules) of mathematics are strictly separated from its demonstration of logical coherence. As I understand it,  there have been multiple attempts in that direction - with the recent example of David McAllester's morphoid type theory, which seems essentially to implement mathematical practice as a language on top of ZFC. Whether this can be accomplished by mere "sugared syntax" is of course a debate over at which point sugared syntax becomes a new language - which includes asking whether restricting our sense of well-formed formulas, or admitting new rules of deduction, will in fact make our language more useful.

Thing 2: I heartily second Sam's point that it is not currently clear what will be a proper internalization of type theory - let alone THE internalization we should consider standard. On this, I agree with several posters: a good first piece of evidence for a useful internalization of type theory would be a clarification of the "applied philosophical core" of type theory, probably most clearly indicated by a SIMPLE example (that is, without much structure) where a candidate internalized type theory (very possibly HoTT) gives insight that standard foundations do not.

However, I would also like the same demonstration for ZFC - but on the level of mathematical structures. Can someone give a simple example of an insight acquired from ZFC, not as easily offered by HoTT, that is self-evidently valuable from a more structural viewpoint?

I think that, if we can answer either of these questions (and, ideally, both), we would be making significant progress in f.o.m.

Best,
- Eric Astor

-----Original Message-----
From: fom-bounces at cs.nyu.edu [mailto:fom-bounces at cs.nyu.edu] On Behalf Of Sam Sanders
Sent: Thursday, March 31, 2016 08:27
To: Foundations of Mathematics <fom at cs.nyu.edu>; Harvey Friedman <hmflogic at gmail.com>
Subject: [FOM] Philosophical coherence and foundational role of set and type theory

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


_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom