The n-Category Café

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

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

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

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.

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.

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.

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.

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