Posts with this logo use 
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.
So,
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:
February 10, 2013
M13
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 is somewhat easier to understand if you think of it as part of a groupoid. John Conway calls this groupoid .
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 is a less messy object.
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.
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?