Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

October 21, 2015

When Not To Use ‘The’

Posted by David Corfield

I’ve revised A Note on ‘The’ and ‘The Structure of’ in Homotopy Type Theory, which we discussed a few months ago – The Structure of A.

As Mike said back then, trying to define ‘structure of ’ in HoTT is a form of ‘noodling around’, and I rather think that working up a definition of ‘the’ is more important. The claim in the note is that we should only form a term ‘The AA’ for a type AA, if we have established the contractibility of AA. I claim that this makes sense of types which are singleton sets, as well as the application of ‘the’ in cases where category theorists see universal properties, such as ‘the product of…’.

Going down the hh-levels, contractible propositions are true ones. I think it’s not too much of a stretch to see the ‘the’ of ‘the fact that PP’ as an indication of the same principle.

But what of higher hh-levels? Is it the case that we don’t, or shouldn’t, use ‘the’ with types which are non-contractible groupoids? One case that came to mind is with algebraic closures of fields. Although people do say ‘the algebraic closure of a field FF’ since any two such are isomorphic, as André Henriques writes here, a warning is often felt necessary about the use of ‘the’ in that these isomorphisms are not canonical. Do people here also get a little nervous with ‘the universal cover of a space’? Perhaps intuitively one provides a little extra structure (map in or map out, say) which makes the isotropy trivial.

I was also wondering if we see traces of this phenomena in natural language, but I think the examples I’m coming up with (the way to hang a symmetrical painting, the left of a pair of identical socks) are better thought of as concerning the formation of terms in equivariant contexts (as at nLab: infinity-action), and the subject of a lengthy discussion a while ago on coloured balls.

Posted at October 21, 2015 11:16 AM UTC

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

32 Comments & 0 Trackbacks

Re: When Not To Use ‘The’

David, suppose I’m in a room of people and notice a person in the corner, holding a glass and I recognise him to be a famous architect. I say to the person I’m speaking to, “The man over there drinking a glass of water is a famous architect”, and we continue chatting, perhaps about the buildings he designed, etc. However, he is not drinking water. He is drinking gin. So, he doesn’t satisfy the description “the man over there drinking a glass of water”. However, my speech act certainly refers to him.

(This kind of example was given by Keith Donnellan, 1966, “Reference and Definite Descriptions”, Philosophical Review.)

Also, by “proposition”, do you mean “sentence” (i.e., a syntactic string)? Or do you mean the semantic content of a sentence (i.e., what synonymous sentences express)?

Posted by: Jeffrey Ketland on October 21, 2015 2:01 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

The issue that a speaker might not have complete or correct information about the world seems to me completely orthogonal to the meaning of “the”. In your example, to the speaker’s knowledge the type of men over there drinking a glass of water was in fact contractible.

Posted by: Mike Shulman on October 21, 2015 5:12 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

I’ve sometimes thought that there should be a way to measure a kind of distance of types, so that as we modify the types in an expression we can say something about its continuing to refer.

I guess it would go via the nearest mutual supertype. So in your case we have “The man over there drinking a glass of colourless liquid”.

Were you to say “The woman over there with the white wine”, we have to resort to the supertype “The person over there drinking a pale liquid”. If no-one else in that area is holding anything, I might still take you to have referred.

By the time you reach “The bear somewhere about with a pistol” it’s probably a stage too far, as “animal somewhere about holding an object” is too distant.

Brandom writes about how we use inverted commas to accept reference through a supertype while not acknowledging the specific type: “That ‘woman’ is in fact my son!”.

I think Jerrold L. Aronson, Rom Harré, and Eileen Cornell were onto something with their type analysis in Realism Rescued. There’s certainly a lengthy complaint about ordinary first-order logic not providing tools to see continuity in science over time.

Posted by: David Corfield on October 21, 2015 5:52 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

The kind of example Donnellan mentions aims to show that the descriptive phrase “the F” may fail to refer, though the speaker still refers successfully when asserting “the F is a famous architect”. I guess the speaker’s intended meaning does involve something that is a small perturbation of the meaning of syntactic phrase used. Here water and gin are visually very similar, and easily mixed up, both examples of a transparent liquid one might drink. So, there’s some “G”, similar to the original “F”, where the speaker’s underlying intention can be expressed by “the G is a famous architect”. It’s very difficult to explain similarity in more basic terms though, because things can be similar and dissimilar in so many different ways. Mere inclusion isn’t going to be enough to get from phrase “the F” actually used to the phrase “the G” the speaker genuinely intends. Mike’s right though, that this point about reference failure is sort of orthogonal to the main point you’re discussing here about the meaning of “the F” phrases, which is non-uniqueness (“the product of A and B”, or “the algebraic closure of F”, “the ordered pair of a and b”, etc.), rather than failure of existence.

Posted by: Jeffrey Ketland on October 21, 2015 7:16 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

A useful insight into one way to think of propositions in HoTT is through the notion of propositional extensionality, which is a version of univalence.

Posted by: David Corfield on October 21, 2015 6:01 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

Yes, but by “proposition” do you mean a syntactic object (string of symbols, like a formula or a sentence) or the content of a syntactic object?

Posted by: Jeffrey Ketland on October 21, 2015 6:23 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

This is something that the HoTT community can’t agree on either…

Posted by: Mike Shulman on October 22, 2015 12:08 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

Do I have it right that one difference in the community concerns whether or not to mark differently a type and the type as an element of the type TypeType?

At propositional extensionality you see we talk of the ‘name’ of a proposition, designated ‘PP’, to contrast it with the proposition as type PP.

This is the way of ‘Tarski universes’, right? Although at Type of types we have the designation of the difference as El(P)El(P) for the type and PP for the element of TypeType.

I guess someone looking in from outside might be shocked that such a basic issue hasn’t been settled, and could wonder how it is possible to proceed. Didn’t we have a discussion somewhere about different grades of sameness, from precise syntactic equality through to a looser equivalence?

Posted by: David Corfield on October 22, 2015 9:14 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

It’s frequently important to distinguish between syntactic strings and their propositional content. In semantic theory, a proposition is defined to be the semantic content of a sentence, so that synonymous sentences have the same content (express the same proposition). Propositions themselves aren’t syntactic entities. No one really has a good theory of propositions, although there are hundreds of articles and many books on the topic. It was the source of a famous correspondence between Frege and Russell around 1902.

If LL is a formalized language with alphabet AA, then A *A^{\ast} is the set of finite sequences from AA (these are the strings or words from AA). A certain inductively subset of these are the terms of LL and a certain inductively defined subset are the formulas of LL, and the sentences of LL are those formulas with no free variables.

Let LL be the formalized language of arithmetic with signature {0̲,s,+,×}\{\underline{0},s,+,\times\}. It contains a constant 0̲\underline{0} and function symbol ss. The sequence of terms 0̲,s0̲,ss0̲,sss0̲,\underline{0}, s\underline{0}, ss\underline{0}, sss\underline{0}, \dots are called canonical numerals. In general, n̲\underline{n} is the nnth canonical numeral. Under the intended interpretation \mathbb{N}, we have (n̲) =n(\underline{n})^{\mathbb{N}} = n, so n̲\underline{n} denotes (refers to) nn.

Where A *A^{\ast} is the set of strings from LL, we can code these strings as numbers, using a godel coding function f:A *f : A^{\ast} \to \mathbb{N}. So, if EE is a string from LL, then it has a godel code f(E)f(E). If n=f(E)n = f(E), then it is denoted by the numeral n̲\underline{n}, and this is written: E\lceil E \rceil. This closed term behaves like a quotation name of the string EE.

For the version of Tarski’s T-scheme you’ve written down at the n-lab post, note that it is inconsistent with very weak principles of arithmetic. The instances are called T-sentences, and have the form T(ϕ)ϕT(\lceil \phi \rceil) \leftrightarrow \phi, where ϕ\phi is a sentence of LL. Suppose QQ is the very weak theory known as Robinson arithmetic. For any formula Ψ(x)\Psi(x), there is a sentence GG such that QQ proves GΨ(G)G \leftrightarrow \Psi(\lceil G \rceil). In particular, if one has a truth predicate T(.)T(.) lying around, there is a sentence λ\lambda such that QQ proves λ¬T(λ)\lambda \leftrightarrow \neg \T(\lceil \lambda \rceil). This contradicts the T-sentence T(λ)λT(\lceil \lambda \rceil) \leftrightarrow \lambda. So, one cannot consistently add the set of all T-sentences to any theory which extends (or interprets) QQ.

Posted by: Jeffrey Ketland on October 22, 2015 3:28 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

David, at the n-lab post on propositional extensionality, you write,

Hence propositional extensionality in type theory is the statement that (P=Q)(PQ)('P' = 'Q') \simeq (P \simeq Q).

Let me rewrite this as,

(ϕ=θ)(ϕθ)(\lceil \phi \rceil = \lceil \theta \rceil) \leftrightarrow (\phi \leftrightarrow \theta).

because I’m not sure of the intended formal rules for \simeq. (I suspect that, formally, \simeq behaves like a strong biconditional, such as (ϕθ)\square (\phi \leftrightarrow \theta), but let’s go with \leftrightarrow.)

This axiom will fail when ϕ\phi and θ\theta are distinct but logically equivalent formulas, because ϕθ\phi \leftrightarrow \theta is true, even though ϕ\phi is distinct from θ\theta. Even if you replace your identity symbol = by some arbitrary relation symbol, say EE, the result is inconsistent with QQ. E.g.,

E(ϕ,θ)(ϕθ)E(\lceil \phi \rceil, \lceil \theta \rceil) \leftrightarrow (\phi \leftrightarrow \theta).

For let θ\theta be \top, some arbitrary tautology. Then ϕ\phi \leftrightarrow \top is equivalent to ϕ\phi, by a truth table. So, the axiom implies,

E(ϕ,)ϕE(\lceil \phi \rceil, \lceil \top \rceil) \leftrightarrow \phi.

Define the formula T(x)T(x) to mean E(x,)E(x,\lceil \top \rceil). So, the axiom implies,

T(ϕ)ϕT(\lceil \phi \rceil) \leftrightarrow \phi.

But this is the T-scheme, and it is inconsistent with Robinson arithmetic QQ, as I mentioned before, because one can define a “liar” sentence λ\lambda such that

Qλ¬T(λ)Q \vdash \lambda \leftrightarrow \neg T(\lceil \lambda \rceil)

Posted by: Jeffrey Ketland on October 22, 2015 10:59 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

It is surely rather implausible that a simple consequence of the Univalence Axiom would be inconsistent with anything one would naturally want to assume when using HoTT.

There are much better qualified people to sort through these things. We had a discussion once about type theory formation rules blocking self-reference, and more general things were said there about how different type theories handle self-reference.

Posted by: David Corfield on October 23, 2015 12:18 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

David, yes, there will be some restriction; and so the point here is that your formulation probably isn’t a consequence of Univalence! But the logical point remains: suppose LL is the first-order language of arithmetic as before, EE is a binary predicate symbol, and L EL_{E} the language obtained by adding EE to LL. Define the scheme Equiv\mathbf{Equiv} to be,

E(ϕ,θ)(ϕθ)E(\lceil \phi \rceil, \lceil \theta \rceil) \leftrightarrow (\phi \leftrightarrow \theta)

Then the theory Q+EquivQ + \mathbf{Equiv} is inconsistent, using the diagonal lemma.

In type theory, certain kinds of self-reference are blocked deliberately. I’m not sure what is supposed to happen in the case you have mentioned. But you can’t have the unrestricted T-scheme without somehow placing restrictions somewhere else. I’m unsure what these restrictions are.

Posted by: Jeffrey Ketland on October 23, 2015 5:12 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

[Y]our formulation probably isn’t a consequence of Univalence!

Indeed, it is not. Codes for formulas in UF will be terms of the type NatNat of natural numbers. Identity between natural numbers is then an identity type formed inside NatNat. Univalence applies to identities of types understood as terms of a universe of types UU. In other words, your schema cannot be an instance of the axiom of univalence.

In short: univalence is an axiom about identity of types, not identity in types. This prevents you from transporting a proof of the logical equivalence of types to a proof of the identity of their codes.

Posted by: Dimitris on October 23, 2015 8:48 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

Thanks, Dimitris. That said, one might expect a proof p 1p_1 witnessing the logical truth of ϕθ\phi \leftrightarrow \theta should somehow convert to a proof p 2p_2 that the statement expressing the equivalence E(ϕ,θ)E(\lceil \phi \rceil, \lceil \theta \rceil) itself holds. But if the formula ϕ\phi and θ\theta are permitted to contain the predicate EE, then the diagonal lemma still leads to a contradiction. So, it looks like the typing restriction would be that ϕ\phi and θ\theta are not permitted to contain the “global” logical equivalence predicate EE. (This is a sheer guess on my part.)

(Work on axiomatic truth theories tries to avoid such type-restrictions, as people are dissatisfied with Tarski’s typed truth theory, and want to study self-applicative untyped theories, like that of Kripke-Feferman, Friedman-Sheard or Cantini.)

Posted by: Jeffrey Ketland on October 23, 2015 10:12 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

I think there’s some miscommunication: when David says “codes” or “names” for types he doesn’t mean something syntactic. The word “code” or “name” is just a manner of speaking to distinguish elements of a Tarski universe from the types that they represent. So it’s perfectly consistent (and, indeed, is a consequence of univalence formulated with Tarski universes) for two codes to be equal precisely when the types that they code for are equivalent.

Posted by: Mike Shulman on October 24, 2015 3:14 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

Yes, Jeffrey’s scheme is about codes-as-Godel-numbers and so it is not an instance of univalence. But David was not talking about codes in that way, of course.

Posted by: Dimitris on October 25, 2015 2:29 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

I wouldn’t say that. It’s true that there is variety in whether type theories use Tarski or Russell universes, but I wouldn’t consider that a point of disagreement in the community. It’s just a choice to be made when formulating a type theory formally, and I don’t think there’s a right or a wrong choice; each choice has its uses.

Jeffrey is of course right that propositional extensionality means that even the “names of propositions” that it refers to are not purely syntactic objects but already have been “semanticized” to some extent. The disagreement I was referring to has to do not so much with anything formal, but rather with to what things the word “proposition” should apply: types (truncated or not), or the syntax describing types, or something in between.

Posted by: Mike Shulman on October 23, 2015 5:12 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

There ought to be infinitely many “the”s, one for each connectivity a type can be, and I think it makes sense to reserve “the” itself for contractible types. I mean, you wouldn’t talk about “the basepoint” of a space merely because it was connected…

Posted by: Qiaochu Yuan on October 21, 2015 4:41 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

I wouldn’t, and you wouldn’t, but I think there are classically trained algebraic topologists who do roughly that.

I like the idea of multiple “the”s. Unfortunately, like the idea of multiple version of “exists” to describe Σ\Sigmas truncated at all levels, it seems that in practice we rarely use any of these levels except 1-1 and \infty.

Posted by: Mike Shulman on October 21, 2015 5:14 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

Why stop there? We could have a notion of “the” for every modality!

Posted by: Tim Campion on October 23, 2015 3:50 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

This is a nice note! One minor suggestion: I try not to use Voevodsky’s phrase “h-level” when using the traditional numbering (contractible = -2, proposition = -1, set = 0, etc.), since Voevodsky uses it with his reindexed numbering (contractible = 0, proposition = 1, set = 2, etc.). I prefer the traditional numbering (mainly because it’s so traditional), but I think it reduces confusion to use different words when using different numbering: a 0-type is of h-level 2, a 1-type is of h-level 3, etc.

Posted by: Mike Shulman on October 22, 2015 12:19 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

I knew the offset counting but I’m not sure I had it straight that ‘h-level’ refers to one of them.

So for the other method, one must say ‘homotopy nn-type’ or ‘nn-truncated’? Do we not need an expression so that I can ask a certain question about a type, and you’ll answer nn when it’s an nn-type,

Question: What ??? is XX?

Answer: nn.

Posted by: David Corfield on October 22, 2015 9:03 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

It would be nice to have such an expression, but I don’t think we do. The best way I can think of to ask that question would be something like “How truncated is X?”

Posted by: Mike Shulman on October 23, 2015 5:17 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

“How truncated is X?”

It makes it sound like XX was formed by truncation of another type.

Posted by: David Corfield on October 23, 2015 8:16 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

I agree, it’s not great. I’d love to hear better suggestions.

Posted by: Mike Shulman on October 24, 2015 3:10 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

“How tall is XX?”

Posted by: John Baez on November 1, 2015 6:39 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

So the height of an nn-type is nn?

Posted by: David Corfield on November 2, 2015 11:25 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

That’s the idea. Surely one needs some word like that, preferably short and simple. ‘Height’ seems reasonable to me, especially since ‘truncating’ something makes it shorter and people talk of ‘higher structures’ and ‘higher categories’.

Posted by: John Baez on November 5, 2015 3:04 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

Presumably, we can have a ‘the-in-context’ in the sense that we can have ‘contractibility in a context’

A:Typex:AB(x):TypeIsContr(B(x)):Type. \frac{A\colon Type \qquad x\colon A\vdash B(x)\colon Type}{IsContr(B(x))\colon Type}.

Then an element of this dependent type IsContr(B(x))IsContr(B(x)), picks out an element p(x):B(x)p(x): B(x) along with an XX-dependent proof of contractibility to p(x)p(x).

If AA and each B(a)B(a) is a singleton set, this would just amount to little more than a function. So we could have TheSuccessor(n)TheSuccessor(n), where Successor(n)Successor(n) is the (singleton) set of successors of nn. But we wouldn’t have TheKing(c)TheKing(c) for a country cc as some countries don’t have kings.

Would anything interesting happen for general AA, such as BG\mathbf{B}G? But I have to dash now.

Posted by: David Corfield on October 23, 2015 3:01 PM | Permalink | Reply to this

Re: When Not To Use ‘The’

Looks like maybe the principle of unique choice?

Posted by: Mike Shulman on October 24, 2015 3:20 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

Ah, thanks. So that’s Corollary 3.9.2 of the HoTT book.

Corollary 3.9.2 (The principle of unique choice).

Suppose a type family P:A𝒰P : A \to \mathcal{U} such that (i) For each xx, the type P(x)P(x) is a mere proposition, and (ii) For each xx we have ||P(x)||||P(x)||. Then we have (x:A)P(x)\product_{(x:A)} P(x).

Also Lemma 3.11.6 looks interesting:

If P:A𝒰P : A \to \mathcal{U} is a type family such that each P(a)P(a) is contractible, then (x:A)P(x)\product _{(x:A)} P(x) is contractible.

Posted by: David Corfield on October 24, 2015 11:15 AM | Permalink | Reply to this

Re: When Not To Use ‘The’

I’ve nothing substantial to add but am enjoying the discussion! So here is a link to a relevant passage: ‘When I make a word do a lot of work like that,’ said Humpty Dumpty, ‘I always pay it extra.’ The chapter ends with H.D. complaining “‘Your face is the same as everybody has — the two eyes, so —’ (marking their places in the air with his thumb) ‘nose in the middle, mouth under. It’s always the same’.” Contractibility!

Posted by: stefan on October 26, 2015 5:36 PM | Permalink | Reply to this

Post a New Comment