### Types in Natural Language

#### Posted by David Corfield

One hoped for effect of my book is that some day philosophers will look to the resources of type theory rather than the standard (untyped) first-order formalisms that are the common currency at the moment. Having been taught first-order logic in a mathematical fashion on my Masters degree many years ago, it struck me how ill-suited it was to represent ordinary language. And yet still our undergraduates are asked to translate from natural language into first-order logic, e.g. Oxford philosophers here. This amusing attempt to translate famous quotations rather proves the point.

To the extent that first-order logic works here, it tends to lean heavily on the supply of a reasonable domain. But when quantification occurs over a variety of domains, as in

Everyone has at some time seen some event that shocked them,

we are asked to imagine some vast pool of individuals to pull out variously people, times and events. Small wonder computer science has looked to control programs via the discipline of types. Just as we want a person in response to *Who?*, and a place in response to *Where?*, programs need to compute with terms of the right type.

Type theories come with different degrees of sophistication. I’m advocating *dependent type theory*. In the *Preface* to his book, *Type-theoretic Grammar* (OUP, 1994), Aarne Ranta recounts how the idea of studying natural language in constructive (dependent) type theory occurred to him in 1986:

In Stockholm, when I first discussed the project with Per Martin-Löf, he said that he had designed type theory for mathematics, and than natural language is something else. I said that similar work had been done within predicate calculus, which is just a part of type theory, to which he replied that he found it equally problematic. But his general attitude was far from discouraging: it was more that he was so serious about natural language and saw the problems of my enterprise more clearly than I, who had already assumed the point of view of logical semantics. His criticism was penetrating but patient, and he was generous in telling me about his own ideas. So we gradually developed a view that satisfied both of us, that formal grammar begins with what is well understood formally, and then tries to see how this formal structure is manifested in natural language, instead of starting with natural language in all it unlimitedness and trying to force it into some given formalism.

Ranta achieves a remarkable amount in this book, and yet I think it didn’t receive as wide recognition as it deserved, although there are a few people working in this tradition today.

It would be interesting to see how different languages lexically code for types, such as where the Japanese affix different endings to their numerals when counting people, long objects, small objects, flat objects, small animals, larger animals, mechanical objects, and so on. Anyone have similar examples from other languages?

## Re: Types in Natural Language

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.