The King of France

The King of France:

You may have seen me pondering over the years how to convince my philosophical colleagues that they ought to invest some time learning category theory. Now, of course philosophers of mathematics should do so, and there’s an excellent case to make that philosophers of physics should do so too, but what of someone working in what are taken to be areas more at the core?

In an as yet undetermined number of posts here, I want to see how we might motivate such attention. Let me start then with a classic from the philosophy of language, involving what are known as ‘definite descriptions’. The use of logic is very common here, so with our new freedom from logic, we ought to have something to say.

In 1905 in On Denoting, Bertrand Russell wielded the power of the, then still novel, predicate calculus to resolve what he took to be a problem with non-denoting terms. On the face of it, writing as he did in the early twentieth century, both

The present King of France is bald

and

The present King of France is not bald

are false, France being a republic. But is the second proposition not the negation of the first? Would this not suggest that the Law of Excluded Middle fails?

Russell’s idea was that one is not the negation of the other, in that the second proposition is not equivalent to

It is not the case that the present King of France is bald.

For Russell, this last proposition is true, since if we unpack the first proposition, it amounts to

There is something which is the present King of France, nothing else is the present king of France, and that thing is bald,

and this is not true.

Symbolically,

¬∃x(K(x)∧∀y(K(y)→y=x)∧B(x)),

and

∃x(K(x)∧∀y(K(y)→y=x)∧¬B(x)),

are not logically equivalent.

Now, if first-order logic is a projected shadow of intensional dependent type theory, what was casting the shadow? I’m going to need some help from the experts, but here we go.

For simplicity’s sake, let’s forget the temporal element, and imagine we have the kind of geo-political entities that we know today as ‘countries’.

First of all, we ought to correct the habit of using untyped logics. Second, we need to get to work on the term ‘King of France’. Let’s declare there to be a type of countries, C, and make the judgement that f:C. Now, ‘King’ would seem to denote a mapping from C to sets of people, it being possible that a country has any number of kings, including none.

So we have the dependent type

x:C⊢K(x):Type.

Now I realise I can read Mike on this stuff, but feel somewhat tentative using it myself. To state that the kings of a country form sets, I guess I write

x:C⊢IsSet(K(x))=True:Prop.

OK, now what? ‘The king of France’ = k(f) is a term, but to which type does it belong? ‘The King of x’ denotes the single king of x, when there is precisely one such king. So, can I do this by requiring the type K(x) to be an inhabited sub-singleton?

IsProp(K(x))=True:Prop,t:K(x)⊢k(x):K(x).

Until we judge that France is a country and that King(France) is an inhabited sub-singleton, we are not allowed to introduce the term ‘The King of France’, let alone speculate as to the hairiness of his head.

It would seem that we’re siding with Peter Strawson’s thought that

When uttering ‘The king of France is wise’ “we simply fail to say anything true or false.”

Something I need to look into is previous literature on dependent type theory and definite descriptions. I see there is Jesper Carlström’s, Interpreting Descriptions in Intensional Type Theory.

DIGITAL JUICE