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 20, 2013

Have You Left Off Beating Your Wife?

Posted by David Corfield

Continuing the series of what type theory can do for philosophy, let us take a look at the infamous question of the title. To forestall criticism, let me say straight away that I’m not proposing in these posts that dependent type theory is the last word in the analysis of these puzzles. I’m merely exploring some issues for my own sake. If I manage to elicit comments such as Neel’s and Mike’s response on self-reference, I shall be very content.


Have you left off beating your wife yet?

Where Bertrand Russell would take a belief as more complex than its surface structure might suggest, still he took it to concern a proposition, the kind of thing which is either true or false. As discussed before

The present king of France is bald

is really a composite:

Posted at 9:59 AM UTC | Permalink | Followups (10)

February 10, 2013


Posted by John Baez

People of a certain ilk wonder why we need groupoids. Why aren’t groups enough?

There are many answers to this question. The answers provided by Alan Weinstein and Ronald Brown should be convincing to any open-minded topologist or geometer. But what if you’re a group theorist… say, someone who studies finite groups? What do groupoids have to offer you?

I just noticed a nice answer to this question. The Mathieu group M 12M_{12} is somewhat easier to understand if you think of it as part of a groupoid. John Conway calls this groupoid M 13M_{13}.

Don’t confuse this with the Hercules Cluster, which is called M13:

The font makes a big difference! The globular cluster M13 is a Messier object. The groupoid M 13M_{13} is a less messy object.

Posted at 12:02 AM UTC | Permalink | Followups (40)

February 6, 2013

The Title of This Post is False

Posted by David Corfield

Continuing our enquiry into what homotopy type theory can do for the formalisation of natural language, if we could make good sense of the phenomena of self-reference, that should pique the interest of those discontent with predicate logic. We won’t be explicitly involving the homotopy aspect of the type theory here, and yet who knows whether it might assert itself, as it did last time on the subject of ‘the’.

So, let’s take a look at the classic liar paradox:

This proposition is false.

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

February 4, 2013

Presentations and Representations in Foundations

Posted by Mike Shulman

I’ve had several requests to write more introductory posts on type theory like the last one. Today I’m going to give it a go by adapting my notes from a talk I just gave here at IAS. So rather than trying to continue directly from the last post, today we’ll take a different tack. Namely, suppose we were designing a new foundational system from scratch. This system will probably be about some kind of “basic objects”, and it’ll probably also include some ways to construct such objects (often using other given objects as data). The question is, how do we describe or characterize these constructions?

Posted at 4:36 AM UTC | Permalink | Followups (33)