Magidor on Category Mistakes and Context

February 14, 2020

Magidor on Category Mistakes and Context

Posted by David Corfield

$MathML-enabled post (click for more details).$

The previous discussion on category mistakes got me reading Ofra Magidor’s SEP article on the subject. Magidor was the right choice to produce this article as the author in 2013 of an OUP book Category Mistakes. She is the Waynflete Professor of Metaphysical Philosophy at the University of Oxford (website), a chair once held by one of my favourite British philosophers, R. G. Collingwood.

Now Collingwood came up before in a post of mine as someone who thought that the representation of propositions in Russell’s logic was totally misguided. Rather than freestanding statements, for Collingwood, propositions only make sense in the context of a series of questions and answers. In part, it was thinking through his insights in terms of type theory that got me started on the idea of proposing the latter as a new logic for philosophy of language and metaphysics.

$MathML-enabled post (click for more details).$

Returning to Magidor’s SEP article mentioned above, we read

Another potential problem for the syntactic approach has to do with the context sensitivity of category mistakes. Consider the following examples:

(11) The thing I am thinking about is green.

(12) That is green.

(13) The number two has the property I’ve just mentioned.

Whether or not these sentences exhibit the kind of infelicity associated with category mistakes depends on context: (11) and (12) are perfectly felicitous in a context where it is clear that the thing I am thinking about/referring to is a pen, but not so in a context where it is the number two. Similarly, (13) is felicitous in a context where it is clear that the property I’ve just mentioned the property of being prime, but not so if it was the property of being green. This is a problem for the syntactic approach, because whether a sentence is syntactically well-formed or not is a context-invariant property: it cannot vary according to context in this manner.

From the type-theoretic perspective, this sounds very strange. There we have the term ‘context’ used in a technical sense to express the conditions that are required in order to form the type that is the proposition, as represented by the sentence. I don’t know the origins of the term in the type-theoretic tradition, but it surely arises from something close to the informal sense of the situation in which judgements are expressed.

Let’s consider proposition (13). Natural language uses sugared turns of phrase for what is represented in type theory, often leaving out parameters. It seems to me reasonable to take

The $A$ , $a$ , has the property $P$

as shorthand for the still sugared

The $A$ , $a$ , has the property( $A$ ), $P$ .

In a situation in which we have $a:A$ and $P: Property(A)$ , we can form the proposition ‘The $A$ , $a$ , has the property $P$ ’, as a longhand version of $P(a)$ . We may then judge this proposition to be true.

When I say ‘The $B$ I just mentioned’, for a type $B$ , this means that we have a recent judgement $b:B$ , whence

‘The $B$ I just mentioned’ $:\equiv b: B$ .

In the current case, I must have recently mentioned some property. So is there a type of properties? Well, a reasonable first step is to say that in the context $X: Type$ , we have

$Property(X) :\equiv [X, Prop] :Type$ ,

where Prop is the type of propositions. (Think subobject classifier, or just the two-element set if you like.)

Let us imagine then that we have judged $A: Type, P: [A, Prop], a: A$ . Then

$a$ has the property (of $A$ ) I just mentioned (that is, $P$ )

is well-formed. Indeed, we can see that $P(a)$ is a proposition, and now the claim is being made that $P(a)$ is true.

Is there a more general type of properties? I suppose one might form the type $\sum_{X: Type} Property(X)$ , of pairs $(A, P)$ such that $P$ is a property of $A$ . One might even call this dependent sum, $Property$ .

Then if I’ve been speaking about a property $(B, Q)$ ,

‘The property I just mentioned’ $:\equiv (B, Q)$ : Property.

But then I can’t form the proposition ‘ $a$ has $(B, Q)$ ’ if I’ve been introduced to $a$ , as $a:A$ , since it does not arise from the rule:

$X: Type, x: X, (X, P): Property \vdash$ ‘ $x$ has $(X, P)$ ’ $\equiv P(x): Prop$ .

I find explaining such things in type theory an odd affair. It feels like you’re making a huge fuss about very little, here that we really have no right to be saying ‘The number two has the property I’ve just mentioned’, when the property I’ve just mentioned is ‘being green’. And yet if we need to spell these things out, then we had better do so.

I suppose one might question whether these considerations were all ‘syntactical’, but I don’t see why we shouldn’t see them as such. For type theorists, sentence formation is utterly context-dependent.

Posted at February 14, 2020 10:14 AM UTC

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

39 Comments & 0 Trackbacks

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

One could have as context a list of numbers written with different coloured pens (with no repetition). Then, one could refer to “the number 2” as being one of the items on that list, and the proposition whether it was green or not would then be well-formed. But if the context was $\mathbb{N}$ , as you have implicitly above, then it doesn’t make sense, as you say.

Posted by: David Roberts on February 14, 2020 9:12 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

For people with grapheme-color synesthesia, the digit 2 can already be blue/green/etc. regardless of its physical color. In other words, “the number two is green” is not automatically a category mistake.

It’s clear to me that we should consider a type of contexts, built from the type of properties, in order to discuss situations like this in which you’d want to agree with someone on most category errors but only disagree on whether numbers can have colors.

Posted by: unekdoud on February 15, 2020 6:14 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

One would certainly need to distinguish a type of numbers from a type of instances of numerals.

Posted by: David Corfield on February 15, 2020 8:12 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

One argument that the issue of the well-formedness of (13) is syntactical would reinterpret things category-theoretically.

The case is, in more general terms, as though I have arrows $f: A \to B$ and $g: A \to C$ , and I wonder whether it’s well-formed to say

The composite of $f$ and another arrow that I’ve just mentioned is equal to $g$ .

Posted by: David Corfield on February 15, 2020 3:15 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Later on in the article we are closer to home:

A second question which separates different versions of the presuppositional account is what kind of presuppositions are involved in the case of category mistakes. A natural hypothesis (endorsed by Asher (2011)) is that these are type presuppositions. For example, we might suggest that ‘is green’ triggers the presupposition that its subject is a concrete object; that ‘is prime’ triggers the presupposition that its subject is a number; and that ‘is pregnant’ triggers the presupposition that its subject is a female.

Presuppositions are something I treat in my book (p. 59) and appear in the (type-theoretic) context that needs to be in place for a type to be formed. Ranta had also reached this conclusion.

Now, apparently, the following causes a problem for Asher:

(36) Mathematician: you know, not only numbers, but also polynomials are prime or composite. This polynomial, for example, is prime.

Of course this is a reasonable thing to say. We can all imagine trying to expand the mind of a teenager by informing them of the extension of the concept of prime elements to kinds of collection, known as ‘rings’. We might also tell them about the idea of prime knots.

Staying with rings, a mathematician isn’t going to speak of something being prime without having specified the ring, since, e.g., $2$ is prime in $\mathbb{Z}$ but not in $\mathbb{Z}[i]$ . So there is a tacit parameter when speaking of prime elements:

$R: Ring, r:R \vdash prime_R(r): Prop.$

Returning to the article

These discourses [such as (36) - DC] seem entirely felicitous even though the final sentence in each discourse violates the proposed type presupposition. In response a proponent of the type-presuppositional hypothesis might suggest reverting to a different type-based hypothesis. For example, in response to (36) they might suggest that the presupposition generated is that the subject-term is a mathematical object. However, this new proposal might be too liberal and because it fails to account for why ‘2.145 is prime’ is a category mistake and it might also be too restrictive because it fails to account for other versions of the argument, where an expert suggests that a non-mathematical object can be prime as well.

That would be misguided to suggest that the presupposed type is any mathematical object. Primeness is relative to a ring. In fact, ‘2.145 is prime’ need not be a category mistake in that sense. Qua real number, the sentence is well-formed. It’s just false – fields, while they are rings, do not have any primes.

Outside of mathematics, I guess we say things like ‘prime real estate’, but that’s a homonym. We really shouldn’t expect each lexical item to have a single type reading.

Posted by: David Corfield on February 16, 2020 3:32 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Further on we read:

Next, consider a different debate at the intersection of philosophy of language and metaphysics, one concerning the phenomenon of copredication. Imagine a context where three copies of War and Peace are on the shelf. Each of the following seems to have a true reading:

(46) (Exactly) three books are on the shelf.

(47) (Exactly) one book is on the shelf.

A natural way to account for these diverging readings is to posit two respective readings of ‘book’: one on which it is used to pick out physical books (of which we have three), and one on which it is used to pick out “informational” books (of which we have one). However, on further reflection this still leaves a puzzle concerning (47): if ‘book’ in this sentence picks out an informational book (arguably a kind of abstract entity), how can this kind of object have the physical property of being on the shelf? These kind of apparently ‘mixed’ reading are referred to in the literature as instances of copredication.

Some solutions to this puzzle involve constructing non-standard semantic and syntactic structures for copredicational sentences (e.g., Asher 2011; Gotham 2017), but Liebesman and Magidor (2017) argue that sentences such as (47) should be taken at face-value: the sentence is about informational books, but on their view, informational books can have physical properties such as being on shelves.

I discuss copredication on p. 34 of my book. I should say here that we are dealing with two different types: Book on shelf up to physical tome; Book on shelf up to information source. The first is a set of three elements, hence (46). The second is a groupoid with three objects and a reversible arrow between each pair. The groupoid cardinality of the latter is 1, hence (47).

In the case of (46), I could ask someone to specify one of the three books by saying where precisely on the shelf it is located. In the case of (47), I can’t ask where precisely on the shelf the one book is located.

Posted by: David Corfield on February 17, 2020 12:00 PM | Permalink | Reply to this

David

$MathML-enabled post (click for more details).$

Three consecutive Waynflete Professors of Metaphysical Philosophy appear in my book - Collingwood, Ryle and Strawson.

To hear now from the third:

“That it should be possible to identify particulars of a given type seems a necessary condition of the inclusion of that type in our ontology.” (P. F. Strawson, Individuals, 1959, p. 16)

Posted by: David Corfield on February 19, 2020 7:05 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

In this type theory you’re using to analyze language, is there a difference between well-formedness and meaningfulness? Can the truth of one proposition affect the meaningfulness of another expression?

Posted by: Matt Oliveri on March 3, 2020 4:59 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

In the type theory itself one doesn’t speak of meaningfulness. Martin-Löf devised a meaning explanation as a justification of the rules of the type theory. However, I don’t see this as bearing on the project to understand natural language in type-theoretic terms.

In natural language as understood in type theory I’m suggesting that apparently well-formed but inappropriate sentences (E.g., ‘This is prime’ pointing at a rabbit) are really not well-formed since there are hidden parameters which don’t match.

A case we worked out here, and which appears in the book, concerns terms of the form ‘the $A$ ’ which should only be introduced if the type $A$ has been shown to be contractible. That in turn requires an element of $A$ of the right form. Then ‘the $A$ ’ carries with it hidden parameters. To use a famous example, we shouldn’t speak of ‘the present King of France’ without having established that there is a unique such person.

Can the truth of one proposition affect the meaningfulness of another expression?

Certainly, if by this you mean can a proposition as type depend on an element establishing the truth of another. I spend some time on this in Chap. 2 in the context of a discussion of type dependency. The meaningfulness of ‘Jill came tumbling after him’ depends on the truth of ‘Jack fell down’. The meaningfulness of ‘He has stopped smoking’ depends on the truth of ‘He was in the habit of smoking’. The meaningfulness of ‘She knows P’ depends on the truth of P.

Posted by: David Corfield on March 4, 2020 7:31 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Hmm, OK. Maybe I’d better clarify, and motivate the question.

Some versions of type theory have an equality reflection rule, which has the consequence that well-typedness depends on truth. So if $M$ is an $a$ by $b$ matrix, and $N$ is a $b'$ by $a$ matrix, “ $N$ is the transpose of $M$ .” is not well typed, but “If $b = b'$ then $N$ is the transpose of $M$ .” is.

So for a king-related version, I guess “If there’s a unique present King of France, he’s bald.” should be meaningful?

Many type theorists identify two problems with equality reflection:

Because the proof that well-typedness depends on is hidden, you generally cannot determine well-typedness just from what was said.
Because a hypothetical proof that well-typedness depends on could actually be impossible, well-typedness becomes vacuous under inconsistent assumptions.

Posted by: Matt Oliveri on March 4, 2020 9:24 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

You’d have to specify how you’ve defined ‘transpose’. Ignoring choice of ring, if it’s given in the context of two natural numbers, $n$ and $m$ , as a function from the type $Mat(n, m)$ to the type $Mat(m, n)$ , then yes there will be combinations of words that don’t amount to a proposition-type, such as $A$ is the transpose of $B$ for the wrong kind of sized matrices.

But you might define a type of matrices to include those of all sizes, and then define an endofunction ‘transpose’ on this type. Then any ‘A is the transpose of B’ is a proposition-type.

As for, “If there’s a unique present King of France, he’s bald.”, with suitable definitions in place, we might reach

$(x,p): isContr(King\;of\;France) \vdash Bald(q(x)): Type,$

where $q(x)$ projects to whatever type of thing ‘Bald’ is a predicate for, (Person or Animal, say), and $p$ is a proof of uniqueness of $x$ .

Then someone might claim that this dependent type is inhabited by uttering those words.

Posted by: David Corfield on March 4, 2020 10:22 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

if it’s given in the context of two natural numbers, $n$ and $m$ , as a function from the type $Mat(n,m)$ to the type $Mat(m,n)$

Yes, this is what I’m referring to.

But you might define a type of matrices to include those of all sizes, and then define an endofunction ‘transpose’ on this type.

Not this.

So here’s the question again: In a context with $a,b,b':nat$ and $M:Mat(a,b),N:Mat(b',a)$ , is “If $b = b'$ then $N$ is the transpose of $M$ .” a proposition?

$(x,p): isContr(King\;of\;France) \vdash Bald(q(x)): Type$

Hmm. That’s not what I had in mind. Maybe we’d better focus on the equality example.

Posted by: Matt Oliveri on March 4, 2020 10:50 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

First you need to say what kind of equality. If it’s ‘judgmental equality’, $b \equiv b': Nat$ , then $Mat(b', a)$ and $Mat(b, a)$ are equal types. $b \equiv b'$ is not a proposition, and so we can’t say ‘If $b \equiv b'$ , then…’.

In the case of propositional equality, we have a type $(b=_{Nat} b')$ . Then from an element, $p$ , in this identity type, I can derive an equivalence, $f$ , depending on $b$ , $b'$ and $p$ , between $Mat(b', a)$ and $Mat(b, a)$ . Then I can compare $transpose(M)$ and $f(N)$ as elements of $Mat(b, a)$ .

So there will be a type (proposition)

$\prod_{p: b' =_{Nat} b}transpose(M) =_{Mat(b,a)} f(b',b,p)(N).$

Since $Nat$ is a set, $b' =_{Nat} b$ is a proposition, so it has at most one element. There are probably things to say about why we can get away with speaking more informally.

Posted by: David Corfield on March 4, 2020 12:21 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

So it sounds like you don’t have equality reflection. With equality reflection, you effectively can say ‘If $b \equiv b'$ , then…’.

There are probably things to say about why we can get away with speaking more informally.

This is an important observation! Yes, it seems this is something reasonable from informal (natural) language that you don’t support. I think equality reflection should be part of the explanation for this example.

Posted by: Matt Oliveri on March 4, 2020 2:01 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

I think now I’m not sure what you mean by $b \equiv b'$ . For HoTT, as definitional/judgmental equality, this is something not standing in need of a proof. It’s the kind of judgement that arises from a stipulation. I can say in the metalanguage things like ‘If I judge $b \equiv b'$ , then I may judge $A(b) \equiv A(b')$ ’, which presumably gets abbreviated to ‘If $b \equiv b'$ , then $A(b) \equiv A(b')$ ’.

If by equality reflection, you mean what they have in the HoTT book, p. 105, then we certainly don’t want it in general.

Exercise 2.14. Suppose we add to type theory the equality reflection rule which says that if there is an element $p:x=y$ , then in fact $x \equiv y$ . Prove that for any $p:x=x$ we have $p \equiv refl_x$ . (This implies that every type is a set…)

The calculus aims to deal with the subtleties of homotopic equivalence, and this rule would give us only an extensional type theory.

If you are dealing with a set, such as $Nat$ , some things are simpler, e.g., it satisfies:

Axiom K: for all $x:X$ and $p:(x=_A x)$ we have $p=refl_x$ .

Posted by: David Corfield on March 4, 2020 3:28 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Yes, I’m aware of all that. Still, it seems plausible that you could get away with equality reflection restricted to certain types. Supposing it applied to $Nat$ , $b \equiv b'$ (judgmental equality of nats) would generally require proof. Then the internal hypothetical ‘If $b =_{Nat} b'$ , then…’ is effectively assuming judgmental equality, which affects the typing judgment.

Posted by: Matt Oliveri on March 4, 2020 3:55 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

I’m pretty sure it’s consistent with univalence, semantically, to postulate equality reflection for Nat. It should hold in Voevodsky’s original simplicial model, in fact.

But there are other reasonable-sounding things you can’t do, e.g. you can’t consistently postulate equality reflection for all contractible types, since equality reflection in (contractible) based path-spaces $\sum_{x:X} (a=x)$ implies equality reflection for all types.

Posted by: Mike Shulman on March 4, 2020 11:33 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Yeah.

I remembered that computational cubical type theory had a universe of “discrete” types where exact equality and paths coincide. Instead of having all the two-level apparatus, it seems like you could just have the universe of discrete types and instead give them equality reflection directly. Their discrete universe was closed under $\Pi$ , $\Sigma$ , “lower” inductive types, and equality, if I remember correctly.

So this makes equality reflection for quite a few h-sets consistent with HoTT. No quotients, though.

Posted by: Matt Oliveri on March 5, 2020 7:06 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Importantly, however, we don’t yet know how to interpret such a thing in all the models of interest. So if anyone wants to use it, I would advocate using it with suspicion.

Posted by: Mike Shulman on March 5, 2020 12:27 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Or perhaps better, the claim would amount to one that the type

$\prod_{(x,p): isContr(King\;of\;France)} Bald(q(x))$

is inhabited.

Posted by: David Corfield on March 4, 2020 10:38 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

That’s closer, I suppose. But my main problem was that I was expecting a definite description operator. I wanted to know what its typing rule was.

But it looks like you’re treating definite description as sugar, and not adding it to the formalism. I cannot offhand think of a situation (in dependent type theory) where this is highly inconvenient, but I know not having equality reflection can be highly inconvenient, and I thought description would be similar since it has a presupposition. (In predicate logic, not having definite description is highly inconvenient.)

Posted by: Matt Oliveri on March 4, 2020 11:03 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

We have an introduction rule for definite decriptions (see also nLab: generalized the

$A:Type,(a,p):IsContr(A) \vdash the(A,a,p)\equiv a:A.$

So definite description can occur in a hypothetical.

Posted by: David Corfield on March 4, 2020 11:43 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

No sorry; I don’t buy it. That’s not a definite description operator. It’s just a function that returns one of its arguments. Formally, the whole point of a definite description operator is to refer to objects that otherwise would not be denoted by any term.

It’s less clear cut whether such an operator is the right model of the “the” of natural language. But a nice thing about the real description operator is that you don’t need to pass in a proof that the object uniquely exists; it merely needs to be true that the object uniquely exists. That is what I meant about well-typedness depending on truth. What you have is a term depending on a proof. (And as you can see, it doesn’t really depend on the uniqueness part. This seems like a sign of a bad explanation.)

Posted by: Matt Oliveri on March 4, 2020 1:44 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

the whole point of a definite description operator…

I’m not sure why I should believe there to be such a single thing. How about you give us an example of what you like to use a definite description operator for, and then people can judge whether they share that need, whether they have an alternative path to meet that need, or whatever.

Let me point out one advantage to my version which is that it can deal with category theorists’ application of ‘the’ to universal constructions. Will yours?

Posted by: David Corfield on March 4, 2020 2:38 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

The description operator I have in mind is similar to yours, but it doesn’t depend on the proof; only the existence of the proof:

$A:Type,\underline{\;}:IsContr(A) \vdash the(A)\,:\,A$

I’m not positive this is sound for HoTT, but I’m not aware of any problem with it, other than that it messes up canonicity.

How about you give us an example of what you like to use a definite description operator for,

I don’t like definite description operators. But it still seems like a bad idea to refer to something as a description operator when it isn’t one.

and then people can judge whether they share that need, whether they have an alternative path to meet that need, or whatever.

It is fine to say that HoTT’s approach to modeling definite description avoids the use of a definite description operator.

Posted by: Matt Oliveri on March 4, 2020 3:36 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Unless I missed something in this conversation, you (Matt) were the one who started talking about definite description operators. I think David’s approach of regarding it as sugar seems like the most sensible and simplest way to parse natural language into dependent type theory.

Posted by: Mike Shulman on March 4, 2020 11:35 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Yes. I had in mind ways that well-typedness can depend on truth, so I thought of it.

But David did say here that he had definite description. That’s what I objected to.

Posted by: Matt Oliveri on March 5, 2020 7:14 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

But he didn’t say “definite description operator”, and you yourself said that definite description can be modeled without a definite description operator. He gave a construction that represents definite description, which I suppose one might certainly call an “operator” in an intuitive sense, but David didn’t even do that, at least not in this conversation. It sounds like you want to insist that the phrase “definite description operator” refers to something with a particular kind of syntactic behavior; that may or may not be justified, but you shouldn’t criticize people for misusing a term that they didn’t even use.

Posted by: Mike Shulman on March 5, 2020 12:33 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Given the context (;)), it still looks to me like he was claiming his “ $the$ ” to be a description operator: although he did not say “operator”, I just had. But maybe he did not mean that.

David, I apologize if I’ve made a fuss over nothing.

Posted by: Matt Oliveri on March 5, 2020 1:00 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

As Mike says, I didn’t mean to suggest that this ‘the introduction’ rule presents something that one or other community refers to as a “definite description operator” according to some specified standard of syntactic behaviour.

Posted by: David Corfield on March 5, 2020 1:44 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

OK. But now I’m curious. Haven’t you guys heard of Russell’s definite description operator “iota”? It’s briefly mentioned on Wikipedia. It’s similar to Hilbert’s epsilon, but requires uniqueness. I figured that that sets the standard for definite description operators.

Posted by: Matt Oliveri on March 5, 2020 2:12 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

The Fregean analysis in the section above on that page is eminently sensible, and come close to ours.

Instead of

‘the’ denotes a function which takes a property $f$ and yields the unique object $z$ that has property $f$ , if there is such a $z$ , and is undefined otherwise,

we say

‘the’ denotes a function which takes a type $A$ that is contractible and yields the ‘center of contraction’.

The ‘center of contraction’ is the element used to establish the type’s contractibility (HoTT book, Def 3.11.1).

Posted by: David Corfield on March 7, 2020 3:34 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Yes, I prefer the Fregean perspective. But really I like how, with type theory, you can be Fregean at the type level and Russellian at the judgment level. Use of a type presupposes that it’s valid. But if you look at derivability of judgments, out pops a Russellian approach: derivability of $a\;:\;A$ often implies derivability of $A\;type$ .

The Fregean perspective doesn’t seem to require that undefinedness is dealt with using types. If I understand correctly, we have both taken the position that well-typed expressions are defined, and so the partiality of definite description is handled by restricting its domain. I happen to be reading about an old proof assistant that instead had a definedness predicate that interacts with the definite description operator: IMPS.

Here is an intermediate ‘the’ specification to consider, for fun:

‘the’ denotes a function which takes a type $A$ and yields its ‘center of contraction’, if $A$ is contractible, and is undefined otherwise.

I’ve deliberately made this more superficially similar to the article’s version. The implicit use of excluded middle is not good, but otherwise is seems kind of like a description of my ‘the’.

Posted by: Matt Oliveri on March 7, 2020 7:47 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

No wait, IMPS doesn’t have undefinedness for formulas, even if they involve undefined expressions. So its approach doesn’t seem Fregean.

Posted by: Matt Oliveri on March 9, 2020 10:33 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Is the iota operator defined (but underspecified) even for non-unique properties? It seems that it must be, if you want to remain in first-order logic. If that’s the case, then the dependent type theory approach seems better. It’s kludgy (and nontrivial to model constructively) to have a term that’s always defined, but whose value can only be known under some conditions.

Posted by: Mike Shulman on March 9, 2020 9:40 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

Well, iota is either higher-order, or a binding form, so it looks like it’s technically already an extension to first-order logic. I agree that it’s kludgy for iota to be defined but underspecified on formulas that aren’t uniquely satisfied. By the way, this is what you get when treating iota as a use case of epsilon e.g. in Isabelle/HOL.

According to the Wikipedia article, that’s apparently not what Russell did, but their description of what he did seems ambiguous. My best guess is that atomic formulas involving an intuitively-undefined iota are false, and connectives work as usual. So “It’s not the case that the present King of France is bald.” comes out true. (This also seems kludgy to me.)

Posted by: Matt Oliveri on March 10, 2020 8:52 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

By “remain in first-order logic” I meant “remain in the judgmental structure of first-order logic”, rather than (for instance) moving to a dependent type theory. I believe some sort of type dependency would be necessary to force the well-formedness of iota to be conditional on provability of a unique-existence property.

Posted by: Mike Shulman on March 11, 2020 1:25 AM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

I guess that’s technically correct, but it misses the point of approaches with a definedness predicate, which is that well-formed terms are not necessarily meaningful.

Iota can be well-formed as soon as its predicate is, and still not be defined till the predicate is uniquely satisfied.

Posted by: Matt Oliveri on March 11, 2020 5:14 PM | Permalink | Reply to this

Re: Magidor on Category Mistakes and Context

$MathML-enabled post (click for more details).$

PS: I’m thinking that an expression is meaningful if and only if it’s well-typed. But maybe you’re not. Also, in the presence of equality reflection, I consider well-typedness to be a different judgment than well-formedness.

Posted by: Matt Oliveri on March 4, 2020 9:32 AM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

February 14, 2020