Formal Semantics in Modern Type Theories. Stergios Chatzikyriakidis
1.2. Foundational semantic languages
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 TY2 can 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
In MTTs, the correctness of typing judgments of the form a: A, stating that a is of type A, is decidable in the sense that we can mechanically decide whether such a judgment can be correctly made. For computer scientists, this is equivalent to saying that a computer system can automatically decide whether a is of type A. Thanks to this decidability result and because of the rich typing mechanisms in MTTs, the Curry–Howard principle of propositions-as-types (Curry and Feys 1958; Howard 1980) gives us an embedded logical mechanism for semantic interpretations – the second requirement above. In this book, we shall elaborate this in detail to illustrate how the logical mechanisms work and how the typing mechanisms facilitate semantic formalizations.
MTTs are specified by means of proof-theoretic rules (see Chapter 2) and, because of this, there are two advantageous facets that are not available in previous set-theoretic semantics: the first is that an MTT can have a use theory of meaning in that its judgments (sentences) can be understood proof-theoretically by means of their inferential uses. Such a proof-theoretic understanding of a foundational semantic language was not available before: we cannot understand set theory in such a way. Therefore, this offers us a new possibility: we may claim that an MTT, as the foundational semantic language, is well understood by means of its proof-theoretic meaning theory. Second, because they are proof-theoretically specified, MTTs (and hence MTT-semantics) can be readily implemented on computers to support computer-assisted reasoning in natural language. In fact, this is supported by the current proof technology provided by the proof assistants based on MTTs, as mentioned above, and we shall describe how MTT-semantics can be implemented on computers to perform reasoning tasks in natural language.
1.3. Montague’s model-theoretic semantics
Since its development in the late 1960s and early 1970s, Montague semantics (Montague 1974) has been the dominant approach to formal semantics. There are several textbooks about Montague semantics including, for example, that by Dowty et al. (1981). As explained above, Montague has introduced an intermediate language, called Intensional Logic (IL), for his model-theoretic semantics. For instance, to interpret the sentence in (1.1), we could first give its interpretation (1.2) in IL, where the semantics of John is an entity j and the semantic interpretation talk of the verb “talk” is a predicate over entities of the world, which can be applied to j to form the interpretation (1.2):
(1.1) John talks.
(1.2) talk(j)
This then gives the set-theoretical interpretation of (1.1), i.e. the interpretation of (1.2) in set theory (according to, for example, Henkin’s model interpretation), which says that the set-theoretic interpretation of j is a member of the set that interprets the predicate talk.
In what follows, we shall first describe simple type theory6 and then how it is used in Montague semantics.
1.3.1. Simple type theory: a formal description
Montague’s IL (Montague 1973; Gallin 1975) consists of an extensional core, which is Church’s simple type theory (Church 1940) (we call it C in this book, with C standing for “Church”), and a part concerning intensionality.7 We shall focus on describing the former and then briefly comment on the part about intensionality.
Our description of Church’s