## January 30, 2013

### 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.

Posted at January 30, 2013 11:45 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2594

### 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 true proposition.

(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 judgmentally equal, 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?)

Posted by: Mike Shulman on January 30, 2013 1:36 PM | Permalink | Reply to this

### Re: The King of France

Great, thanks! There really is a difference between watching and doing type theory.

What you had in parentheses in the third paragraph was right. Now I see I don’t need those circumlocutions.

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?)

Yes, you’d think linguists would have studied these structures. I wonder if type theoretic framing would be suggestive.

Posted by: David Corfield on January 30, 2013 1:51 PM | Permalink | Reply to this

### Re: The King of France

Mike just beat me to answering that …

Regarding type theory and natural language: you may want to look at the Grammatical Framework by Aarne Ranta.

Posted by: Bas Spitters on January 30, 2013 2:06 PM | Permalink | Reply to this

### Re: The King of France

I don’t suppose you could summarize it for us?

Posted by: Mike Shulman on January 30, 2013 2:51 PM | Permalink | Reply to this

### Re: The King of France

Dear Bas, Dear all,

Thanks for the interesting discussion and for inviting me to it! My main work on this problem is in the book “Type-Theoretical Grammar” (OUP 1994), Chapter 4, and GF can be seen (to some extent) a grammar formalism implementing these ideas so that they are usable in computer programs such as translation and parsing.

The main idea is indeed similar to what was is stated in David Corfield’s comment on January 31, under the name of “generalized the”. My inspiration for it came from Game-Theoretical Semantics, in particular the book “Anaphora and Definite Descriptions” by Hintikka and Kulas (Reidel 1985). The contribution of type theory was that it provided a rigorous formalization of the idea, with games interpreted as types and winning strategies as proof objects.

So let me give a brief summary: the article “the” can indeed be seen as a noun-phrase forming operator, which can be typed as follows:

the : (A : Set) -> Elem A -> A

Semantically, it is defined as an identity function

the A a = a

Syntactically, it is linearized (“sugared” in the 1994 book) in a way that forgets the object a,

the A _ –> “the” A

where of course in other languages the form of the article may depend on the gender of A, as made precise in GF.

There is not requirement of uniqueness here, nor even existence in a global sense. The interpretation normally comes from the context, which is defined in type theory as a sequence of proof variables of increasingly depending types. Thus for instance “the window is broken” can be used in any context where a window is given, even though there might exist other windows. Existence can be relative to a very narrow context, for instance,

if this room had a window, I would open the window

which type theoretically is a universal quantification

(Pi z : (Sigma x : window)(has(this_room,x))open(I,p(z))

The “King of France” example is related to this, and involves, as Ulrik Buchholtz points out, a presupposition, which means a proof object suppressed in linearization. Ordinaty mathematics has plenty of examples, where my favourite example is

derivative : (f : R -> R) -> (x : R) -> differentiable(f,x) -> R

linearized

derivative f x _ –> “the derivative of” f “at” x

in English. Also mathematical symbolism suppresses the proof:

derivative f x _ –> f “’(” x “)”

As we know, awareness of the suppressed proofs in cases like this is an essential part of the proper usage of mathematical language.

Now the analogy to the King of France is clear,

king : (x : country) -> kingdom(x) -> man

king x _ –> the king of x

And notice that the proof can be provided by the local context as well:

If France was a kingdom, the king of France would live in Versailles.

Posted by: Aarne Ranta on February 1, 2013 8:51 AM | Permalink | Reply to this

### Re: The King of France

Thank you very much for this. I see our library has your book. I’ll enjoy reading that over the weekend. Has anyone taken on further this application of type theory to natural language?

Posted by: David Corfield on February 1, 2013 12:24 PM | Permalink | Reply to this

### Re: The King of France

Very nice!! Thanks for the summary. That does seem to be a good way to describe the usage of “the” in natural language.

Posted by: Mike Shulman on February 1, 2013 10:28 PM | Permalink | Reply to this

### Re: The King of France

king : (x : country) -> kingdom(x) -> man

This tries to capture the existence and uniqueness of a king for a kingdom, but ordinary life doesn’t usually work that smoothly.

We can have kingdoms with no kings, like the UK currently, for reasons of gender, or kingdoms with two kings, such as Bwari, or Midian.

Surely it’s more natural to code for a type being a singleton than to construct a complex predicate:

king : (x : country) -> country-with-single-king(x) -> man

Posted by: David Corfield on February 3, 2013 1:34 PM | Permalink | Reply to this

### Re: The King of France

So presumably we can now tell the type theoretic story for generalized the as follows:

$A: Type, f: Type^A, x: A, t: IsContr(f(x)) \vdash the(f, x, t): f(x).$

Posted by: David Corfield on January 31, 2013 8:41 AM | Permalink | Reply to this

### Re: The King of France

Looks good to me. Or more generically still,

$(A:Type),(t:IsContr(A)) \vdash (the(A,t):A)$

Posted by: Mike Shulman on February 1, 2013 3:35 AM | Permalink | Reply to this

### Re: The King of France

In case it hasn’t been mentioned here, How to Calculate Proofs: Bridging the Cultural Divide Raymond T. Boute in Feb 2013 Notices AMS might could be relevant

Posted by: jim stasheff on January 30, 2013 2:25 PM | Permalink | Reply to this

### Re: The King of France

In case it hasn’t been mentioned here, How to Calculate Proofs: Bridging the Cultural Divide Raymond T. Boute in Feb 2013 Notices AMS might could be relevant

Posted by: jim stasheff on January 30, 2013 2:26 PM | Permalink | Reply to this

### Re: The King of France

I agree that the problems with definite descriptions (and partial terms in general) seem to be best resolved in terms of presuppositions stating that they denote. And dependent type theory is very well suited to express these presuppositions using hypothetical judgments.

By the way, the problem is ubiquitous already in ordinary mathematics with partial operations such as division, root taking, limits (infinite sums and integrals), etc. (Here is an essay by Feferman on Definedness.)

When dealing with programs we of course have the question of how to deal with the fact that general recursion leads to partial functions (not all programs halt).

This presents the following issue for constructive type theory: we can easily do recursion theory in type theory, and when using general recursive terms we need evidence that they halt. However, one of the main interpretations of the logic is that the usual terms should represent recursive operations. But to connect the terms of type $\mathrm{Nat} \to \mathrm{Nat}$ to the general recursive functions would be to postulate a formalized Church’s Thesis, which is not always desirable as it rules out other interpretations.

I would also like to mention some other approaches to partiality, such as Beeson’s Logic of Partial Terms and Dana Scott’s Logic of Existence. (Sorry about the pay-walled links.)

There are also category-theoretic approaches, perhaps starting with Robinson and Rosolini’s paper on Categories of partial maps and Moggi’s thesis on The Partial Lambda-Calculus, but I think other, more knowledgeable, people here can give further references.

Posted by: Ulrik Buchholtz on January 30, 2013 6:54 PM | Permalink | Reply to this

### Re: The King of France

A comment, which may be completely misguided.

Instead of asking that ‘the’ means ‘there exists a unique’ and breaking up the sentence as (the)(king of France)(is bald), what about taking ‘the — is bald’ as a unit, and having the sentence (the — is bald)(king of France), where really you should imagine some Fregean notation indicating the second clause goes in the middle of the first. Then (king of France) doesn’t need to be a subsingleton, just that the statement itself is clearly not going to have a truth value in $\mathbf{2}$. If there are several kings of France, then there will be a subset of those who are bald. Or perhaps the truth value of the sentence could be taken to only have an element when we pass to singletons of the set of kings of France - a sort of local truth.

Posted by: David Roberts on January 31, 2013 3:35 AM | Permalink | Reply to this

### Re: The King of France

Hmm, isn’t ‘the’ just too important a word to have to tack it onto some passing predicate? Would you want (the — is the son of someone who had three sisters)(king of France)?

If I’ve got that right above, we can capture ‘generalized the’ type theoretically too.

Posted by: David Corfield on January 31, 2013 8:52 AM | Permalink | Reply to this

### Re: The King of France

‘the’ means ‘there exists a unique’

That is the most common usage of “the” - that the description gives a singleton set and thus has a unique member.

However there are many examples such as “Paris Hilton is the daughter of a rich family”, “the cat bit me on the finger”, “the painting hung on the wall of my living room”, where “the” is used without implying that the sets are singletons.

I’ve seen this issue discussed but can’t recall a good linguistic explanation of when “the” can pick out a non unique member of a set.

Posted by: RodMcGuire on January 31, 2013 6:25 PM | Permalink | Reply to this

### Re: The King of France

Perhaps we should name a “generic ‘the’”, as used in

The wolverine has a reputation for ferocity and strength out of proportion to its size, with the documented ability to kill prey many times larger than itself.

This use is like $([ ]:wolverine \to creature) \& \forall x : wolverine, ferox([x])$.

Posted by: Jesse McKeown on February 1, 2013 6:33 PM | Permalink | Reply to this

### Re: The King of France

A tangentially relevant article from The Atlantic. A court has been trying to figure out whether “the” implied uniqueness, not in today’s use, but in 1783. Fun stuff.

Posted by: John Smith on February 2, 2013 8:25 PM | Permalink | Reply to this

### Re: The King of France

Let’s not forget plural ‘the’

The kings and queens of England.

Maybe there’s an idea of a definite collection at stake.

I wonder if there’s a whiff of definiteness to

The cat bit me on the arm,

even if there are two arms.

The cat bit me on the limb

sounds wrong.

Posted by: David Corfield on January 31, 2013 8:22 PM | Permalink | Reply to this

### Re: The King of France

Yeah, I think my intuitive English parsing algorithm definitely groups “the king of France” as a noun phrase, about which we then assert baldness.

Posted by: Mike Shulman on February 1, 2013 3:34 AM | Permalink | Reply to this

### Re: The King of France

Is there any logical differnce between If France was a kingdom, the king of France would live in Versailles.

If France were a kingdom, the king of France would live in Versailles.

If France was a kingdom, the king of France would have lived in Versailles.

Posted by: jim_stasheff on February 1, 2013 1:41 PM | Permalink | Reply to this

### Re: The King of France

If I remember correctly the If .. were is the more classical form of the conditional tense, whilst ‘if … was’ is the simpler ‘modern’ version. Can someone check this?

In other words in ordinary logic they should be equivalent as it looks like it is just `grammar’, but perhaps in one of the modal temporal logics ….?

Posted by: Tim Porter on February 1, 2013 7:37 PM | Permalink | Reply to this

### Re: The King of France

That’s true, but there’s a second interpretation of ‘if … was’, namely ‘if it is true that France was a kingdom’ (as opposed to ‘if it is true that France is a kingdom’). I’m not sure how standard/classical that usage is, or of its relationship to ‘If France had been a kingdom…’

Posted by: Mark Meckes on February 1, 2013 9:19 PM | Permalink | Reply to this

### Re: The King of France

Of course, we hard-line prescriptivist grammarians still maintain that writing “if…was” for the subjunctive mood is “wrong”. (-: The general descriptivist hegemony notwithstanding, I think there’s a good argument that when one of two grammatical options is objectively more expressive or less ambiguous, it should be preferred. As Mark says, “if France was a kingdom” could also mean “if it was true (at some point in the past) that France was (then) a kingdom”, so it’s better to use “if France were a kingdom” for the subjunctive meaning of “if it is true (now, although it isn’t) that France is a kingdom”. As for “if France had been a kingdom”, I think that is a “pluperfect subjunctive”, meaning that “if it is true (now, although it isn’t) that France was a kingdom (at some point in the past)”.

Posted by: Mike Shulman on February 1, 2013 10:45 PM | Permalink | Reply to this

### Re: The King of France

As long as we’re quibbling about such things, those parentheticals of “although it isn’t” should really be something more like “although it may not be”.

Posted by: Mark Meckes on February 2, 2013 1:07 AM | Permalink | Reply to this

### Re: The King of France

As long as we’re quibbling about such things, those parentheticals of “although it isn’t” should really be something more like “although it may not be”.

Posted by: Mark Meckes on February 2, 2013 1:08 AM | Permalink | Reply to this

### Re: The King of France

use “if France were a kingdom” for the subjunctive meaning

You appear to be confusing the irrealis form “were” with the English subjunctive and may be a blithering idiot :-) according to Geoff Pullum, co-author of The Cambridge Grammar of the English Language .

Posted by: RodMcGuire on February 2, 2013 1:54 AM | Permalink | Reply to this

### Re: The King of France

O! That I were King of France… I would he should not shout so loud… “Be he Nabob, Pooh-bah, hobo, nobo-/dy oompahs on the Tuba solo/quite like Roger Bubo”…

Trying to translate the intention of “I wish Bob were here”, the best I can come up with is «je voudrais que Robert fût ici»; that is, the meaning seems to force usage of what the French calls subjunctive. This is of course distinct from claiming that it is what should be called subjunctive in English, but the distinction between “were I late” and “should I be late” seems more like a tense distinction than a mood/mode distinction.

Posted by: Jesse McKeown on February 2, 2013 3:09 AM | Permalink | Reply to this

### Re: The King of France

Whoops, my blithering link above doesn’t work. Geoff Pullum feels strongly about calling “were” subjunctive. LanguageLog seems to be down right now but here is a Google search of the times he has railed against it.

Posted by: RodMcGuire on February 2, 2013 3:55 AM | Permalink | Reply to this

### Re: The King of France

Well, being myself only an amateur grammarian, I’ll sit back and let the professionals call each other names until a consensus emerges (if ever). I make no apology for following Wikipedia’s terminology (which, among other things, considers the subjunctive to be a particular example of an irrealis mood).

Posted by: Mike Shulman on February 2, 2013 7:06 PM | Permalink | Reply to this

### Re: The King of France

Yes, I was about to remark: Geoff Pullum, so renowned for his restraint and politesse and good manners.

It’s sometimes entertaining to read Language Log, to see them dissect ill-founded prescriptivist notions so artfully and articulately and with such erudition, but sometimes they do so a little too gleefully, to the point of real malice and venom.

Posted by: Todd Trimble on February 2, 2013 8:24 PM | Permalink | Reply to this

### credit Peano not Russell

The Theory of Descriptions should be credited to Peano and not Russell.

Peano stated the rules correctly and concisely in section 22 of his Studii di Logica Matematica, 1897.

Russell muddled it all up again, in his usual conceited style.

The passage from Peano is quoted in Italian and English in my lecture In defence of Dedekind and Heine–Borel at the third workshop on Formal Topology in Padova in 2007,

This goes on to present introduction, elimination, beta and eta rules for descriptions, claiming that they are already present in Peano, and proceeds to do the same for Dedekind cuts.

Posted by: Paul Taylor on February 3, 2013 3:29 PM | Permalink | Reply to this

### credit Frege not Peano (maybe?)

Russell credits Peano rather profusely in the first paragraph of the discussion of definite descriptions in the Principles of Mathematics 1903, section 63. He says that he proposes to discuss the matter philosophically only – and “On Denoting” is a different development of the same difficulties. It is not unreasonable to call by the name of a ‘theory of descriptions’ the sort of thing Russell thought lacking in Peano and tried to supply. If it is a matter of introducing a special description operator then of course Frege’s Grundgesetze (1893) – which Peano reviewed in 1895 – as usual takes precedence (there is a discussion in the earlier paper on Sinn and Bedeutung too; a different discussion appears in Grundlagen, 1884, §74 note 1, but of course without a symbol; the purpose of the 1884 note is to insist on what you express in your introduction rule.) In Grundgesetze the operator (a backslash) is made quite salient by the fact that Frege adds a special axiom VI partially capturing his informal elucidation. If we view his ‘extensions’ as sets, which is appropriate here, the axiom is: ‘the {y | y = x} = x’, which might be put “\ {x} = x”

Posted by: Michael T on March 25, 2013 12:09 AM | Permalink | Reply to this

### Re: The King of France

People who want to know more about linguists’ thoughts on definite and other kinds of NPs might have a look at Barbara Partee’s course materials:

http://people.umass.edu/partee/Teaching.htm

Posted by: Avery Andrews on February 16, 2013 9:15 AM | Permalink | Reply to this

Post a New Comment