Stergios Chatzikyriakidis - Formal Semantics in Modern Type Theories

In this chapter, we shall start with a brief account of the historical development of type theory for the study of the foundations of mathematics – the simple type theory for classical mathematics and dependent (modern) type theories for constructive mathematics. Simple type theory was employed by Montague and his followers as an intermediate language for the study of model-theoretic semantics of natural language, where set theory is taken as the foundational language. In MTT-semantics, on the other hand, modern type theories (MTTs) are themselves foundational languages. The new logical concepts and rich typing mechanisms in MTTs make them adequate to serve as foundational languages for formal semantics. We shall introduce MTT-semantics briefly, which will be developed further in the book, and summarize its advantages.

Type theories are computational logical systems that were originally developed for the foundations of mathematics. At the beginning of the 20th Century, Russell (1903) developed the theory of types to solve a foundational problem of mathematics exposed as a number of well-known paradoxical contradictions in Cantor’s naive set theory that are related to self-reference. Some researchers, including Russell himself, attributed such paradoxes to “vicious circles” in formations of logical formulae (“impredicativity”, in a technical jargon), which is what Russell’s Ramified Theory of Types (Whitehead and Russell 1925) was designed to circumvent.

However, Ramsey (1926) pointed out that it was the logical paradoxes such as Russell’s paradox, not the semantic paradoxes such as Liar’s paradox, that can (and should) be avoided in formulations of logical calculi and that Russell had mixed up these two kinds of paradoxes, leading to complications and problems in his ramified theory of types. As Ramsey argued, although impredicativity in formula formations is circular, it is not vicious. Based on this, Ramsey suggested 1 that the ramified theory of types can be “simplified” into Simple Type Theory, which was later formally formulated by Church (1940) using the λ-notation and used by Montague (1973) in his Intensional Logic (IL) to study the formal semantics of natural language.

The early developments of type theory, including those by Russell and Ramsey as mentioned above, were driven by the search for foundational languages for classical mathematics. In the 1970s, various logicians, notably Feferman, Friedman, Martin-Löf and Myhill, among others, studied foundational languages for constructive rather than classical mathematics. Besides other systems, Martin-Löf’s type theory (Martin-Löf 1975, 1984) stood out with several new ground-breaking concepts that were not present in traditional logical systems. It adopts the notions of context, judgment and definitional equality, and introduces powerful typing mechanisms such as dependent types, inductive types and type universes. It also makes use of the principle of propositions as types, also called the Curry–Howard correspondence (Curry and Feys 1958; Howard 1980), to incorporate an embedded logic in the type system. These features have not only made Martin-Löf’s type theory a very interesting candidate for the foundation of constructive mathematics but, more importantly, opened up new avenues to study dependent type theories as attractive foundational languages for various other applications such as computer-assisted reasoning and linguistic semantics.

In particular, the study of Martin-Löf’s type theory, together with that of Church’s simple type theory, has led to the development of a family of (intensional) type theories that we call MTTs, 2 including Martin-Löf’s predicative type theory (Martin-Löf 1975; Nordström et al . 1990) and the impredicative type theories such as the Calculus of Constructions (Coquand and Huet 1988) and the Unifying Theory of dependent Types (UTT) (Luo 1994). In computer science, MTTs have been implemented in proof assistants, computer systems for formal proof development, such as Agda (2008), Coq (2010) and Lego/Plastic (Luo and Pollack 1992; Callaghan and Luo 2001), and used in applications to formalization of mathematics and verification of programs.

It is worth remarking that, although formalizing constructive mathematics motivated the early development of dependent type theory, it is not true that MTTs can only be employed constructively. Put in another way, powerful typing is not monopolized by constructive mathematics or constructive reasoning; instead, it can be used in much wider applications such as linguistic semantics: the MTT-semantics to be studied in this book is one such example. 3

In the study of formal semantics, one considers a foundational semantic language in which semantic interpretations of natural language sentences and phrases are given; in other words, it is meaning-carrying language in the sense that its sentences/phrases interpret the natural language sentences/phrases. A foundational semantic language is usually a formal mathematical language that, besides being precise and usually unambiguous, has several important salient features, including the following:

1) the language has rich and powerful mechanisms and is hence capable of giving adequate semantic descriptions for a variety of diverse linguistic features;

2) the language contains (or embeds) a useful logic to be used in semantic interpretations;

3) the language is regarded as well understood (and, hence, so are the semantic interpretations).

In Montague’s model-theoretic semantics (Montague 1973, 1974), axiomatic set theory is the foundational semantic language. First, it is clear to see that set theory is very powerful and capable of adequate semantic descriptions: this has been proved to be the case in the development of formal semantics in the Montagovian setting. Second, set theory incorporates a useful logic, which may be different from the logical system (e.g. first-order logic) based on which set theory is formulated. However, this is not very obvious, and it is one of the reasons that Montague introduced an intermediate language IL (Intensional Logic) (Montague 1973): it gives the syntax of a simple type theory in which, among other things, the syntax of usual logical operators is made explicit. Interpreting a natural language phrase in IL, we can indirectly obtain its set-theoretical interpretation from the semantics of IL in set theory (see, Henkin’s (1950) model). The intermediate language IL makes the task of semantic description easier and clearer. In fact, as Gallin (1975) shows, although IL only formulates the syntax of logical operators and gives their meanings semantically in set theory, an alternative system TY 2can be axiomatized as a variant of Church’s simple type theory (Church 1940), of which we shall give a presentation below and discuss its use in Montague semantics. 4

Whether set theory satisfies the third requirement of a foundational semantic language, that is, whether it is well understood, is subjective and less clear. Some may say that people have a rather good understanding of naive set theory. But, of course, this is not enough or even misleading – it is not the naive set theory in play here; rather, in Montague semantics, we use an axiomatic set theory as the foundational semantic language. It is fair to say that it is not easy to understand an axiomatic set theory such as ZFC (for example, for those familiar with formal set theory, think of the complicated and non-intuitive axioms in set theory!)

In MTT-semantics, modern type theories are foundational semantic languages (see, the notes on the related historical development in section 1.4.2). They have powerful mechanisms and rich type structures: this satisfies our first requirement – an MTT is a powerful language for formal semantics. In particular, like sets in set theory, types represent collections and the rich typing mechanisms in MTTs provide powerful tools to describe various linguistic features. Although types in MTTs are different from sets in set theory, they provide powerful mechanisms for formal semantics, as to be demonstrated in this book, among other things. We say that, although MTTs are specified proof-theoretically, MTT-semantics is model-theoretic – for formal semantics, the rich typing mechanisms in MTTs are powerful, just like the set-theoretical mechanisms in set theory. 5