[FOM] Wiki: type theoretic fnds

[Erik Palmgren]

Regarding the 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.?

I think Aczel's type theoretic model (in MLTT) of CZF constructive set 
theory may be a good example. Here a direct constructive model of a 
complicated system is given. No recursion theory is necessary.
It is possible to understand the computational content of the
model by reflecting on the computation rules of the MLTT involved.
It has only type constructions Pi (dependent product), Sigma (dependent 
sum), + (disjoint sum), N (natural numbers), Empty type, W (type of 
wellfounded trees), and a type universe closed under these 
constructions. Measuring success by length of a self contained
explanation, I think this may be hard to beat for a standard 
realizability interpretation.

Erik Palmgren

> Date: Wed, 30 Mar 2016 16:20:07 -0400
> From: Harvey Friedman <hmflogic at gmail.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: [FOM] Wiki: type theoretic fnds
> Message-ID:
> 	<CACWi-GWrUSgGtosomTramHsXRUE6C5pfcYZ7Vtd4J2KLJhj=eQ at mail.gmail.com>
> Content-Type: text/plain; charset=UTF-8
>
> 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
>
>
> ------------------------------
>
> Message: 4
> Date: Wed, 30 Mar 2016 19:24:55 -0400
> From: martdowd at aol.com
> To: fom at cs.nyu.edu
> Subject: [FOM] Reflective well-founded relations
> Message-ID: <153c9d814fb-6c6-63fb at webprd-a82.mail.aol.com>
> Content-Type: text/plain; charset="utf-8"
>
> "Reflective well-founded relations" has just been submitted, and is
> temporarily available at my web site.
>
> If $\kappa$ is an inaccessible cardinal and $\phi$ defines a WF
> (well-founded relation) $R$ in $V_\kappa$, say that $\phi$ relects
> at $\lambda$ if it defines a WF at $\lambda$.  Say that $R$ is reflective
> if there is a stationary set of $\lambda$ at which $\phi$ reflects.
>
> By generalizing the results of "Sigma-1-1 Well-Founded Relations and Set
> Chains", new axioms for set theory are given which make use of such WF's.
>
> It is also shown that as $S$ gets smaller the heights of the WFs' increase,
> whence if $V=L$ the chain lengths do.
>
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: </pipermail/fom/attachments/20160330/b8857d89/attachment-0001.html>
>
> ------------------------------
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
> End of FOM Digest, Vol 159, Issue 30
> ************************************
>