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.

February 26, 2020

Type Theory and Propositions

Posted by David Corfield

One of the things that philosophers will take a lot of getting used to, if HoTT is to be taken up as a new logic for philosophy, is the idea of propositions as a kind of types. We are very used to treating propositions with propositional logic, and then sets very differently, with first-order logic and some set axioms. This results in different issues arising for the latter, as when a philosopher worries about the ontological commitments of a simple piece of applied set theory or even applied arithmetic. It appears that speaking of two apples on my desk, I’m referring to some abstract entity 22. Then I’m to worry what kind of entity this number is, and how I can know about it. Applying logic by itself to the world is generally taken not to incur any such ontological debt.

Now, we are beginning to hear in analytic philosophy the idea that propositions are types, for instance, in the work of Hanks and Soames that propositions are types of predicative acts, as when we predicate wisdom of Socrates in ‘Socrates is wise’.

From the HoTT perspective, we will often have

x:AB(x):Prop, x: A \vdash B(x): Prop,

where from a:Aa: A we can then form B(a):PropB(a): Prop. And we can think of this type as predicating BB of aa. But propositions may arise by other routes, such as Id A(a,b)Id_A(a, b) for a set AA and two of its elements, e.g., is it the case that the tallest person in the room and the youngest person in the room coincide. Another form of proposition is generated as A\|A\| for a type AA. The latter is known as the bracket type where any elements of AA are identified. The proposition A\|A\| will be true when AA is inhabited. So if, say, AA is the type of occurrences of Kim drinking coffee yesterday, A\|A\| corresponds to the proposition whether Kim drank coffee yesterday.

Posted at 2:30 PM UTC | Permalink | Followups (121)

February 20, 2020

What’s the Most Exciting New Mathematics?

Posted by John Baez

I’m considering writing a column on the most exciting new developments in math (for some magazine). This makes me want to ask:

What do you think are the most exciting new developments in math?

It would help a lot if you explain why you think they’re exciting. And I especially want to hear answers from outside category theory–since I roughly know what’s going on there. But there are probably new things there, too, that I haven’t heard about yet. So don’t hold back: let me know what you think!

Posted at 6:24 PM UTC | Permalink | Followups (31)

February 17, 2020

2-Dimensional Categories

Posted by John Baez

There’s a comprehensive introduction to 2-categories and bicategories now, free on the arXiv:

Abstract. This book is an introduction to 2-categories and bicategories, assuming only the most elementary aspects of category theory. A review of basic category theory is followed by a systematic discussion of 2-/bicategories, pasting diagrams, lax functors, 2-/bilimits, the Duskin nerve, 2-nerve, adjunctions and monads in bicategories, 2-monads, biequivalences, the Bicategorical Yoneda Lemma, and the Coherence Theorem for bicategories. Grothendieck fibrations and the Grothendieck construction are discussed next, followed by tricategories, monoidal bicategories, the Gray tensor product, and double categories. Completely detailed proofs of several fundamental but hard-to-find results are presented for the first time. With exercises and plenty of motivation and explanation, this book is useful for both beginners and experts.

Posted at 3:44 PM UTC | Permalink | Followups (7)

February 15, 2020

Robert Hermann, 1931–2020

Posted by John Baez

Robert Hermann, one of the great expositors of mathematical physics, died on Monday February 10th, 2020. I found this out today from Robert Kotiuga, who spent part of Saturday with him, his daughter Gabrielle, and his ex-wife Lana.

Posted at 6:08 PM UTC | Permalink | Followups (7)

February 14, 2020

Magidor on Category Mistakes and Context

Posted by David Corfield

The previous discussion on category mistakes got me reading Ofra Magidor’s SEP article on the subject. Magidor was the right choice to produce this article as the author in 2013 of an OUP book Category Mistakes. She is the Waynflete Professor of Metaphysical Philosophy at the University of Oxford (website), a chair once held by one of my favourite British philosophers, R. G. Collingwood.

Now Collingwood came up before in a post of mine as someone who thought that the representation of propositions in Russell’s logic was totally misguided. Rather than freestanding statements, for Collingwood, propositions only make sense in the context of a series of questions and answers. In part, it was thinking through his insights in terms of type theory that got me started on the idea of proposing the latter as a new logic for philosophy of language and metaphysics.

Posted at 10:14 AM UTC | Permalink | Followups (39)

February 11, 2020

Types in Natural Language

Posted by David Corfield

One hoped for effect of my book is that some day philosophers will look to the resources of type theory rather than the standard (untyped) first-order formalisms that are the common currency at the moment. Having been taught first-order logic in a mathematical fashion on my Masters degree many years ago, it struck me how ill-suited it was to represent ordinary language. And yet still our undergraduates are asked to translate from natural language into first-order logic, e.g. Oxford philosophers here. This amusing attempt to translate famous quotations rather proves the point.

To the extent that first-order logic works here, it tends to lean heavily on the supply of a reasonable domain. But when quantification occurs over a variety of domains, as in

Everyone has at some time seen some event that shocked them,

we are asked to imagine some vast pool of individuals to pull out variously people, times and events. Small wonder computer science has looked to control programs via the discipline of types. Just as we want a person in response to Who?, and a place in response to Where?, programs need to compute with terms of the right type.

Type theories come with different degrees of sophistication. I’m advocating dependent type theory. In the Preface to his book, Type-theoretic Grammar (OUP, 1994), Aarne Ranta recounts how the idea of studying natural language in constructive (dependent) type theory occurred to him in 1986:

In Stockholm, when I first discussed the project with Per Martin-Löf, he said that he had designed type theory for mathematics, and than natural language is something else. I said that similar work had been done within predicate calculus, which is just a part of type theory, to which he replied that he found it equally problematic. But his general attitude was far from discouraging: it was more that he was so serious about natural language and saw the problems of my enterprise more clearly than I, who had already assumed the point of view of logical semantics. His criticism was penetrating but patient, and he was generous in telling me about his own ideas. So we gradually developed a view that satisfied both of us, that formal grammar begins with what is well understood formally, and then tries to see how this formal structure is manifested in natural language, instead of starting with natural language in all it unlimitedness and trying to force it into some given formalism.

Posted at 10:44 AM UTC | Permalink | Followups (20)

February 6, 2020

Modal Homotopy Type Theory - The Book

Posted by David Corfield

My book Modal Homotopy Type Theory appears today with Oxford University Press.

As the subtitle – ‘The prospect of a new logic for philosophy’ – suggests, I’m looking to persuade readers that the kinds of things philosophers look to do with the predicate calculus, set theory and modal logic are better achieved by modal homotopy (dependent) type theory.

Since dependent type theories are thoroughly interrelated with category theory, in a sense then, all these years later, I’m still trying to get philosophers interested in the latter. But this book marks a shift in strategy in making the case not only for the philosophy of mathematics, but also for metaphysics and the philosophy of language.

The book explains in order: Why types? Why dependent types? Why homotopy types? Why modal types? I’ll discuss some such issues in forthcoming posts.

Posted at 10:33 AM UTC | Permalink | Followups (11)

EGA1: The Language of Schemes

Posted by John Baez

Tim Hosgood, Ryan Keleti and others have finished an English translation of this classic:

and the LaTeX files are now open-source on GitHub. They are working on the rest of EGA, and they could use help!

Posted at 1:28 AM UTC | Permalink | Post a Comment