[FOM] Wiki: type theoretic fnds

[Mario Carneiro]

One obvious property of type theory in general, that has been mentioned
several times on related threads, is that type theory has a much stronger
ability to reject statements as ill-formed, which is a *good thing*. In set
theory, you are not allowed to write "x in in y". Why? Because it does not
fit the formation rules for wffs, it is a meaningless expression. However,
"0 in 1" is perfectly valid, even though many mathematicians will tell you
this is meaningless. (If you spend too much time with ZFC, you will become
convinced that this is a normal question, since it is well-formed according
to ZFC, and the answer is "yes" if those are defined as von Neumann
ordinals.)

In type theory, this sort of thing is thrown out. If "0" and "1" are
definitions of real numbers, we allow expressions like "0 + 1" and "0 = 1",
but "0 in 1" is rejected. You say "there 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." How do you
propose to categorize and marginalize these type-theoretically invalid
statements?

As a first approximation, ZFC has sets, of course, and these often act like
types. We can define the set R of real numbers, and "0 in R" is of course
perfectly well defined and true. We can form functions, such as {<x,y> | (x
in R /\ y = x + 1)}, abbreviated (x in R |-> x+1), which the type theorist
might write (lambda x:R, x+1), and these will inhabit the set (R^R) of all
functions from R to R.

Suddenly, it seems we have a simple type theory on our hands. Indeed, it is
no more complicated to form the dependent product, also known as an indexed
cartesian product. Similarly, the dependent pair type, sum type, and other
common type formers are all available in ZFC.

But that's not all the type theorists want. They also want their rules to
"compute", which means some kind of normalization for the terms that can be
formed. In this area, there is no such guarantee by general ZFC (as far as
I know). However, it doesn't matter as long as we are simulating type
theory inside ZFC, because we will invariably want to use the well-typed
operators mentioned above (specifically lambda terms and application) in
order to construct our terms.

Coming now to HoTT, the question becomes much less clear. The reason, is
because all of the above is essentially creating a model for dependent type
theory in ZFC, where extensional and intensional equality coincide. As soon
as you add univalence, that goes out the window, and to date I have never
seen a model of HoTT in ZFC, which gives me grave doubts as to its
consistency: in fact, for me the most impressive thing about HoTT is that
it seems to be consistent despite its crazy rules. I have asked some very
smart people about why HoTT is understood to be consistent, and what models
there are, and I heard something about infinity-groupoids and simplicial
sets which I interpreted as "come back after you've taken a class or two on
category theory".

So in some ways ZFC and HoTT are incompatible, in that it is exceedingly
nontrivial to simulate all the aspects of one in the other. (For simulating
ZFC in HoTT, it seems mostly possible, although you have to make extensive
use of propositional truncation to remove all the "garbage" that HoTT adds
to all your sets.) I like to think of it more as an alien planet, where I
don't really understand what is going on, but it seems to work out well for
the residents, and so I would caution against assuming that our "home
planet" ZFC is better simply because that is what we are used to.

Mario Carneiro

On Wed, Mar 30, 2016 at 4:20 PM, 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160331/b941d8c7/attachment.html>