### Urs Schreiber in The Reasoner

#### Posted by David Corfield

In December 2008, I interviewed Tom Leinster for Kent’s in-house journal – The Reasoner. The latest version, September 2012, sees me do the same to Urs.

I’m posting this here so that any regulars, or anyone who comes here via *The Reasoner*, can discuss whatever strikes them in what Urs says.

The abrupt transition in *The Reasoner* from interview to succeeding article had people last time imagining Tom had decided to talk about ‘The Paradox of Omniscience’. Likewise, you need to guard against thinking Urs goes on to talk of ‘Personal taste ascriptions and the Sententiality assumption’.

Something I’d like to develop is the idea that transformations in the past in the relationships between logic, mathematics and physics were brought about by, and led to, a rethinking of the concepts of language, observation, world, knowledge, God (once upon a time), etc. Think Newton and the Leibniz-Clarke correspondence, or the transformations of, say, 1880-1930.

Regarding the latter, to quote a small passage from an article I’m reading at the moment, Logic, Mathematical Science, and Twentieth Century Philosophy: Mark Wilson and the Analytic Tradition, Michael Friedman characterises the thinking of early analytic philosophers as follows:

Just as Cantor, Weierstrass, Dedekind, and Peano had finally uncovered the “true” logical forms of the concepts of infinity and continuity, Frege and his followers could now embark on an analogous project of uncovering the “true” logical forms of all the concepts found in the mathematical-physical sciences–including, especially, the radically new science of space, time, motion, and matter emerging in the context of Einstein’s general theory of relativity. The crucial point, as I have emphasized, is that what we call modern set theory was not conceived as simply the most general purely mathematical theory comprising all possible purely mathematical structures; it was rather conceived as part of the most general framework for logic itself, and it was this, above all, that made it an appropriate general platform, in turn, for all properly

philosophicalconceptual analysis.

Should there not be an ongoing comparable, explicitly philosophical conversation taking place right now? I hope this interview can spark off such a thing.

A couple of possible starting points:

1) Is there anything in Per Martin-Löf’s philosophical background, perhaps his reading of Husserl and Frege, that gives rise to his type theory being taken up homotopy theoretically, in particular his constructive approach to identity judgements?

2) We can follow a line of thought which notes that physicists have been interested in certain kinds of theory, so that we ought in turn to be interested by a framework that’s able to capture important aspects of those theories. Cohesive homotopy type theory is such a framework. But is there not a way to run things in the other direction? Any interesting universe involves a dynamics. Dynamics must be encoded via a notion of the cohesion of adjacent elements of space. Cohesion is best encoded by the concept of a cohesive $\infty$-topos. Most suitably structured examples of cohesive $\infty$-toposes relate to smooth forms of cohesion. We could then be led to think that some parts of the form of current physics can be explained. What, though, if radically different kinds of cohesion were found?

## Re: Urs Schreiber in The Reasoner

Thanks, David.

You write:

The way I have heard the story it’s rather the opposite, and in a quite interesting way:

apparently Martin-Löf had first made public a version of his type theory that had an extra axiom forcing identity types to have unique terms. Apparently within days, if I remember correctly, a colleague of his pointed out that including this axiom ruins one of the most precious properties of type theory: it makes “type checking undecidable”. Accordingly that axiom was dropped, and there was an uncertainly left ever since as to what to make of the resulting intensional type theory, which was so very beautiful, but in which one could’t prove that there is a unique way in which two terms are equal.

It was not before the beginning of our millenium that suddenly people realized that this apparent bug was a major feature.

Notimposing this extra axiom makes the theory be homotopy type theory.This is where much of this feeling of excitement comes from: if one just follows the spirit of the purest formal logic available, then the result is automatically and naturally homotopy theoretic. One has to go against the grain to force it not to be. In a way it is maybe more fortunate than unfortunate that Martin-Löf did

notanticipate this. It makes all the more forceful the lesson to be learnd here.A propos: unfortunately the interview went to “print” shortly before Mike and myself wrote that little piece:Quantum gauge field theory in Cohesive homotopy type theoryfor QPL 2012. This explains in a bit more detail various of the issues that we are alluding to in the interview.

Yes, indeed. There are a few interesting issues to be explored. I have now two new students starting, or about to start, working on geometric quantizaton in cohesive homotopy type theory. Maybe there is a student out there fancying a thesis that aims to further explore the space of models of cohesion? Would be quite worthwhile. I have some ideas, but don’t have the time to work them all out myself.