The n-Category Café

It is not central to predicate logic that there is only one sort. But pedagogically it simplifies things and it has unfortunately become rather universal. It would be better to compare type theory to multi-sorted predicate logic.

I suppose you have already considered Chomsky’s Colorless green ideas sleep furiously to explain that a “category error” is a type error, rather than a “semantic error” as usually claimed, and thus ultimately a syntactical error (in a non-context-free grammar)?

I believe Meinong’s jungle deserves some exploration.

I mentioned Japanese counting suffixes. I didn’t realise there could be so many, as here.

While dependent type theory is an improvement over first-order logic, unfortunately both dependent type theory and first-order logic assume that natural languages are static, where in fact, natural languages are dynamic by nature.

There are many languages which have counters, not just Japanese. One of my favorite examples are the Mayan languages Tzotzil and Tseltal. They’re a favorite because when learning about them my professor told us a joke (in Tzotzil iirc) that starts off “there are three guys walking down the street”— only instead of using the counter for two-legged things, as one should for humans, they instead use the counter for four-legged things. Because of that grammatical ‘error’, the listener is forced to conclude that the three guys must be falling down drunk. Nowhere else in the joke is it indicated that the guys are wasted, but the humor of the joke comes from that implicit understanding; and hence the joke can’t really be translated into languages like English. From a type-theoretic standpoint, one could interpret this as being a sort of implicit coercion to get the types to match up; and from the HoTT standpoint (or any other dependent type theory without UIP) we can see this as an example of the fact that paths may have nontrivial content and so transporting along them is not a no-op.

Linguistically speaking, counter systems can (in many respects) be viewed as an extreme variant of the grammatical gender in IndoEuropean languages. For example, one of the primary uses of gender systems is to have some form of ‘agreement’ that helps clarify things like which noun an adjective modifies. Arguably Japanese counters can be said to serve the same clarifying function. That is, consider a sentence like “I have three cats”. In English we would parse that as having a syntactic structure where “three” is some sort of adjective/modifier that attaches to “cats”, and then the phrase “three cats” is some sort of argument to the verb “have”. However, in Japanese the “three” is not a modifier on “cats”, instead it behaves syntactically more like an adverb/modifier attaching directly to the verb.† Without counters this syntax would very easily lead to confusion, but with counters it’s pretty straightforward (unless someone’s going out of their way trying to be confusing).

Another example of lexically coded type information is grammatical case markers (this is a stock example in the Montagovian tradition). These aren’t types for categorizing objects in the domain of discourse, as you have in the counters example above and in many-sorted logics; instead they’re types for categorizing syntactic/combinatorial potential, that is for coding how/where the pieces of a sentence fit together. Using Japanese again, we can think of verbs as having some number of slots for arguments, and each slot requires a certain type of argument (e.g., subject, direct object, indirect object); the case particles then serve as the mechanism for converting generic nouns into the appropriate syntactic type. This is important because Japanese does not have fixed word order, so we cannot rely on the position of a phrase to determine which slot it goes into (whereas English does use positional arguments, hence doesn’t ‘need’ grammatical case).‡

†: Japanese does have constructs that behave like English, but they’re not the default/simple/standard syntax.

‡: My dissertation formalizes the free-order aspect of this example, since case marking alone doesn’t free one from the sequentiality of categorical grammars. We ultimately end up with something very like operads, however some details are different since we do not have full commutativity but only a limited form of commutativity.