Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

May 22, 2013

Philosophy Talks in Oxford

Posted by Simon Willerton

Guest post by Bruce Bartlett

On Monday, David Corfield and Kobi Kremnitzer gave philosophy talks in a snazzy new building at Oxford:


The talks shared homotopy type theory as a common theme. The name “Per Martin-Löf” was mentioned a lot, which was good for me since I had always thought Martin and Löf were two separate people:

pic of martin-löf

Notes are available above, but I will try to give some brief impressions.

Kobi Kremnitzer, What is geometry?

1. Introduction

He started by answering the question “Why am I giving this talk?”, and explained that he followed the pragmatic approach to philosophy of mathematics. I think then he said his approach was somehow similar to that of Wittgenstein and Carnap (but he could have been saying the exact opposite :-)), and that for him, there is no Metaphysics in the joint carving. I’m afraid this totally went over my head, but I did imagine some Oxford dons pleasantly carving a roast chicken, which started to make me hungry!


He stressed that for him mathematics is not in the business of theorem proving only, but mathematicians create new systems, new languages, and that in the correct language a problem becomes trivial… the approach of Grothendieck.

2. Categorical language Since it was a philosophy talk, he motivated categories by starting with Kripke semantics, going via posets, and then he went from posets to categories by literally “raising the bar”!


3. Crashcourse in algebraic geometry Algebraic geometry is the study of solutions to polynomial equations, like a parabola:

X={yx 2=0}. X = \{y-x^2 = 0\}.

I haven’t specified what “y” and “x” actually are, and that’s the point. We can interpret them in any ring. Hence the Grothendieck view is to think of an affine variety XX defined by a bunch of polynomial equations f 1,,f nf_1, \ldots, f_n as being a presheaf on the (opposite) category of rings,

X:RingsSet, X : Rings \rightarrow Set,

defined by

X(R)={(a 1,,a n)R n:f i(a 1,,a n)=0foralliI}. X(R) = \{ (a_1, \ldots, a_n) \in R^n : f_i(a_1, \ldots, a_n) =0 \,\, for \,\, all \,\, i \in I\}.

This leads us to define the category of algebraic spaces as being nothing but the category of presheaves on Ring opRing^{op}.

This category of algebraic spaces has lots of nice properties. Inside it live subcategories of objects having nice properties, such as schemes and sheaves. But Kobi stressed that it is very handy to understand them as living in this general universe of algebraic spaces.

4. What is algebra? There was a crucial idea lurking above – that a ring is a gismo RR which allows you to take any polynomial f[x 1,,x n]f \in \mathbb{Z}[x_1, \ldots, x_n] and evaluate it on elements of RR.

So – to go from algebraic to differential geometry, we could replace the concept of a “ring” with the concept of a “C C^\infty-ring” – this is a gismo RR which allows you to take any smooth function fC ( n,)f \in C^\infty (\mathbb{R}^n, \mathbb{R}) and evaluate it on elements of RR!

For instance, the space of smooth functions on a manifold is a C C^\infty-ring… but so is [ϵ]/ϵ 2\mathbb{C}[\epsilon]/ \epsilon^2 ! So by this slight change of view, we have accomplished Leibniz’s dream – calculus and infinitesimals in the same universe.

5. Final comments He spoke a bit about: derived geometry, set-theoretic foundations, noncommutative geometry, synthetic differential geometry, elementary theory of the category of sets – have a look at the last few pages of his notes.

He stressed that ordinary set-theoretic foundations pulverizes spaces into “atomic dust” where the elements have no “cohesion” with each other… we have to put this back in by hand using topology. As a foundation, homotopy type theory will have this cohesiveness natively built in, and that is attractive to a geometer.

David Corfield, What might philosophy make of homotopy type theory?

David began by defining three “camps” in the philosophy of mathematics:

  • Antiformalism (eg. Heidegger, Wittgenstein)
  • Proformalism (eg. Russell, Carnap, Quine)
  • Historical / dialectical philosophy (eg. Cassirer, Collingwood, Lautman, Polanyi, Lakatos, Shapere, MacIntyre, Friedman)

This last camp has the longest list of names, so you guessed it, David placed himself there! He quoted from Domski and Dixon, which I couldn’t understand, but I could understand this quote from his book:

Straight away, from simple inductive considerations, it should strike us as implausible that mathematicians dealing with number, function and space have produced nothing of philosophical significance in the past seventy years in view of their record over the previous three centuries. Implausible, that is, unless by some extraordinary event in the history of philosophy a way had been found to filter, so to speak, the findings of mathematicians working in core areas, so that even the transformations brought about by the development of category theory, which surfaced explicitly in 1940s algebraic topology, or the rise of non-commutative geometry over the past seventy years, are not deemed to merit philosophical attention.

He had rather sobering news for philosophers keen on getting involved with homotopy type theory:

If one is not on-board already, that’s leaving it rather late to assist with Homotopy Type Theory.

He mentioned the n-category exposition on homotopy type theory by Mike Shulman (starting here) quite a lot, and also Urs Schreiber’s explanation of how homotopy type theory natively produces the “right answer” in a differential topology problem in string theory (flux quantization condition).

He also explained how homotopy type theory gets around certain problems, such as Have you left off beating your wife? and The present king of France is bald.

He also spoke about polarity, inference, modal logic and lots of other stuff - but my understanding was severely cramped.

Finally he ended on a positive note, there is plenty of places for philosophers to get involved:

  • For philosophers of the historical / dialectical persuasion, homotopy type theory is just the kind of development that needs to be written up. There is plenty to learn from the development – the role of logician-philosopher Martin-Löf, constructive type theory, category theory, homotopic mathematics, influence of physics, computer science.

  • For proformalist philosophers, there are also plenty of opportunities. Look closely at intensionality, modality, polarity, the dependent type theory-language relation, and philosophy of physics.

He ended by linking to the upcoming book by Mike Shulman and co., and the nLab.

Posted at May 22, 2013 5:26 PM UTC

TrackBack URL for this Entry:

15 Comments & 0 Trackbacks

Re: Philosophy Talks in Oxford

Thanks for putting this together, Bruce. I enjoyed Kobi’s effort to bring modern geometry to the attention of philosophy.

While in Oxford I heard of the new Centre – QMAC. Think I’ll try to get along to their symposium

Particular attention will be devoted to questions concerning the theory and mathematical application of local topological quantum field theory, and an investigation of how modern mathematical perspectives on quantum theory could be advanced through an understanding of the geometry of type theory.

Sounds like what we learn about in these parts.

Posted by: David Corfield on May 22, 2013 8:52 PM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

Yes indeed, I think the opening symposium of the QMAC centre at Oxford will be advertised more formally soon.

Posted by: Bruce Bartlett on May 23, 2013 1:01 AM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

By the way, what is… Whewellian consilience?

Posted by: Bruce Bartlett on May 24, 2013 8:00 AM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

William Whewell (1794-1866) used ‘consilience’ as a test a scientific theory needed to pass, where hypotheses had to

“explain and determine cases of a kind different from those which were contemplated in the formation” of those hypotheses (1858b, 88) (SEP).

Different lines of evidence should converge to the same laws.

Perhaps I’m using consilience a little loosely to mean when lines of conceptual investigation come together to generate something greater than the parts. This has the flavour also of Whewell’s coherence.

Posted by: David Corfield on May 24, 2013 8:52 AM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

Hi Bruce. Nice post — thanks!

A couple of errors, I think: there are two item 3s. More profoundly, a scheme, algebraic space etc. is not a presheaf on RingRing but a presheaf on Ring opRing^{op}. That is, it’s a functor RingSetRing \to Set (satisfying whatever conditions). After all, if you have a solution to y=x 2y = x^2 in some ring RR, and a homomorphism RSR \to S, then you get a solution to y=x 2y = x^2 in SS.

Posted by: Tom Leinster on May 23, 2013 12:58 AM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

Yeps, thanks - will fix it.

Posted by: Bruce Bartlett on May 23, 2013 1:15 AM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

It’s really nice that philosophers are engaging with homotopy type theory! (Although it’s somewhat, um, disconcerting to see my blog posts quoted at length in David’s slides… (-: ) Since the conference at Irvine a few weeks ago, I’ve been realizing more that mathematicians working on foundations have an obligation to reach out to philosophers, especially when radical changes like this come along. I hope that the book will be helpful to philosophers as well as mathematicians. (Although the prospect of its being quoted far and wide also fills me with trepidation, especially given the long arguments and compromises we had over details of wording…)

I guess I should add Per Martin-Löf to the list of “distinguished mathematicians who may be mistaken for two people by the unwary student”. For some reason I don’t think I ever had that problem with his name, but I do remember being deceived at first by Cesare Burali-Forti, Tullio Levi-Civita, and Gösta Mittag-Leffler. Maybe we should make an nLab category for them.

I hope that philosophers (and mathematicians!) aren’t overly discouraged by David’s comment that “if one is not on-board already, that’s leaving it rather late to assist with Homotopy Type Theory.” A lot has happened already, true, but it’s really still quite early days mathematically for HoTT. There are lots of mathematical aspects still unexplored, and I suspect many that it hasn’t even yet occurred to us to think about exploring. Not being a philosopher myself, I can’t say anything definite about the philosophical side, but I suspect that there’s plenty to contribute on that side too.

As one possible example, I’d be interested to see a philosopher sympathetic to HoTT take on Martin-Löf’s meaning explanation of type theory. Last fall we spent (part of me wants to say “wasted”) a lot of time trying to understand “the meaning of the meaning explanation”, and I for one never really quite “got it”, although I did make enough progress to write an nLab page. I suspect that since Martin-Löf is, as David says in his slides, a “logician-philosopher”, another philosopher might “get” what he’s doing more easily. What is the “meaning explanation” of homotopy type theory?

Posted by: Mike Shulman on May 23, 2013 10:31 PM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

I certainly didn’t mean to put off any philosopher from joining in the HoTT fun with my “too late to assist” remark. Anyway, I left ‘interpret’ and ‘apply’ as live options.

My thought was that if you were hoping to contribute as the kind of pioneering philosopher-logician of the past (Leibniz, Frege, Peirce,…), you’d better be aware that you need to steep yourself in a vast background first of category theory, type theory, homotopy theory, etc., and not just the formalisms, but also the ways of thinking in these formalisms. I’m continually reminded around here, and the nLab, just how much you guys have as your background knowledge. Unfortunately, most philosophers are not exposed at all to this background in their training.

I think you located one very plausible place for philosophers to contribute. Also, though maybe related, where did the motivation for the intensional aspect of intensional type theory come from?

Posted by: David Corfield on May 24, 2013 9:04 AM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

Ah, I see what you mean. Yes, it’s true that there is a lot of background involved. On the other hand, one of the exciting things about homotopy type theory is that you don’t really need to already have all that background in classical mathematics in order to do the analogous things synthetically in type theory. It’s true that a lot of what we do in HoTT is an adaptation of something that was known classically, but sticking too closely to the classical mathematics can also hold us back from finding the ‘natural’ way to do things in HoTT. In fact, so far some of the best homotopy type theorists are graduate students who’ve been exposed to this stuff very early on, and I suspect one reason is that they don’t have as much to unlearn.

The book (and papers, blog posts, etc.) are necessarily addressed at least partly to mathematicians coming from a classical background, because they’re people we want to draw in. But I hope that the book will also be readable as a pure exposition of HoTT as a theory in its own right, without needing any prior exposure to the classical concepts. In particular, we’ve also been hoping that it will be readable by some computer scientists, who come in with very different backgrounds. I’d be very interested to know whether it’s readable to philosophers as well, and if not, how we can make it more so in future revisions. (One thing that occurs to me immediately is that we might be assuming more category theory in a few places than the average philosopher knows, since our target audiences among both mathematicians and computer scientists generally have some experience with it.)

Posted by: Mike Shulman on May 24, 2013 7:49 PM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

Martin-Löf - one or two?

Well, type-theoretical logican PER Martin-Löf has a brother ANDERS, who was also a mathematical Professor (in Matheamtical Statistics) at Stockholm.

Also logician Martin-Löf in myexperience was sometimes confused with MARTIN LÖB, of Löb’s Theorem fame, and professor of Logic at Leeds and later at Amsterdam.

Posted by: Göran Sundholm on May 29, 2013 3:07 PM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

One Martin-Löf was on my PhD committe. Think it was Anders, although not obvious since neither photo on Wikipedia is from the right time (1986).

Posted by: Thomas Larsson on May 31, 2013 3:11 PM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

And wikipedia is evidently slanted towards academic fame. A third Martin-Löf born in the early 1940s (a brother?), Sverker, is one of Sweden’s best known industrialists. Since he apparently is not on english wikipedia, here is a link to the Swedish one.

Posted by: Thomas Larsson on May 31, 2013 3:23 PM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

You may be interested in Martin-Lof’s lectures on invariance under isomorphism and definability. The videos are available from the link.

Posted by: Bas Spitters on May 24, 2013 8:24 AM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

Thanks for sharing, Bruce.

I’d be very interested in understanding how one passes from

  • schemes as ringed spaces locally isomorphic to a spectrum, to
  • schemes as particular presheaves on Ring op\mathrm{Ring}^{\mathrm{op}},

and conversely.

Is there, e.g., a formal account of such constructions? Can we replace rings with some other category and get a notion of spectrum that makes things work?

Posted by: Tom Hirschowitz on June 24, 2013 11:17 AM | Permalink | Reply to this

Re: Philosophy Talks in Oxford

The key is the notion of Zariski covers. One needs some topology that tells you what maps of rings correspond to inclusions of subspaces when you pass to the spectrum. See the nLab page on ‘geometries’ (although it seems to be down for me at the moment).

Posted by: David Roberts on June 24, 2013 3:14 PM | Permalink | Reply to this

Post a New Comment