### The King of France

#### Posted by David Corfield

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,

**[Edit: it has kindly been pointed out to me that I ought to write “There is something which is presently King of France, nothing else is presently king of France, and that thing is bald”.]**

and this is not true.

Symbolically,

$\not \exists x(K(x) \wedge \forall y(K(y) \to y = x) \wedge B(x)),$

and

$\exists x(K(x) \wedge \forall y(K(y) \to y = x) \wedge \not 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 \vdash 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 \vdash 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) \vdash 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.

## Re: The King of France

While $x:C \vdash IsSet(K(x))=True:Prop$ is close to expressing what you want, it’s better (and simpler) to just say $x:C \vdash ks:IsSet(K(x))$. Here $IsSet(K(x))$ is a proposition, propositions are types, and to assert or prove a proposition is to exhibit an inhabitant of it.

We can always construct, for any proposition $P$, a new proposition $P=True$ which will be equivalent to $P$ (and hence, under univalence, equal to it), but this is an unnecessary circumlocution. If we did this, though, then again to assert that $P$ is in fact true we would want to exhibit an inhabitant of $P=True$, i.e. to judge $x:C\vdash ks:(IsSet(K(x))=True)$. The judgment $x:C \vdash IsSet(K(x))=True:Prop$ merely says that “$IsSet(K(x))=True$” is a proposition, rather than making any claim about whether it is a

trueproposition.(Hmm, after writing that, I am reminded that sometimes a syntax like “$x=y:A$” is used for the judgment that $x$ and $y$ are judgmentally equal at type $A$, which is more like what you may have meant. In HoTT we seem to be moving towards using a different symbol like $\equiv$ for judgmental equality, with $=$ for propositional equality (i.e. paths). But if this is what you were thinking, then it has the different problem that $IsSet(K(x))$ and $True$ are not ever going to be

judgmentallyequal, even if $IsSet(K(x))$ is a true proposition. If you are just looking for a notation for the propositional equality type which notates the ambient type $A$, then common choices are $x=_A y$ and $Id_A(x,y)$.)Regarding “the king of France”, it seems to me to be a matter of what choice we make about the meaning of “the”. Russell seems to be assuming that we can always prefix anything by “the” and that this should be interpreted as the inclusion of a side condition that the descriptor prefixed describes a unique object. I’m more inclined to your interpretation, where we consider a proof of uniqueness of that object as being a necessary precondition for the use of “the” in the first place.

If we phrase “proof of uniqueness” as “inhabited subsingleton” as you did, then I would write the judgment something like $(x:C),(kp:IsProp(K(x)),(t:K(x)) \vdash (the(x,kp,t):K(x)).$ In other words, given a country $x$, a proof that it has at most one king, and a proof that it has some king, we may introduce the phrase “the king of $x$” whose value depends on $x$ and the two given proofs. (Another option would be to replace $kp$ and $t$ by a single proof of $IsContr(K(x))$.) Of course, the proof that $x$ has some king is just to exhibit a king, and so the obvious definition is $the(x,kp,t) \coloneqq t$. This reminds me of algebraic nonalgebraicity.

In ordinary language, of course, we don’t mention the proofs $kp$ and $t$, but formally it’s useful to keep them around in the syntax. A nice way to model this sort of omission in programming and large-scale proof formalizations is with things like “typeclasses” and “canonical structures”. These are ways for us to tell the computer “there is a canonical or understood inhabitant of this type, so whenever I seem to need an inhabitant of that type but haven’t provided one, you should assume that I mean the canonical one.” Proofs of uniqueness are excellent candidates for canonical structures, and the current re-development of the homotopy type theory Coq library is making use of them for this and similar purposes. Perhaps we should view natural language in a similar light, as being interpreted in the context of numerous “canonical structures” coming from the shared cultural-linguistic context of the speaker. (Surely someone has done that already?)