### 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:

- Kobi Kremnitzer, What is geometry?, 2-4pm.
- David Corfield, What might philosophy make of homotopy type theory?, 4.30-6.30pm.

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:

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 = \{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 $X$ defined by a bunch of polynomial equations $f_1, \ldots, f_n$ as being a *presheaf* on the (opposite) category of rings,

$X : Rings \rightarrow Set,$

defined by

$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^{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 $R$ which allows you to take any polynomial $f \in \mathbb{Z}[x_1, \ldots, x_n]$ and *evaluate* it on elements of $R$.

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

For instance, the space of smooth functions on a manifold is a $C^\infty$-ring… but so is $\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.

## 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

Sounds like what we learn about in these parts.