Stergios Chatzikyriakidis - Formal Semantics in Modern Type Theories

Furthermore, the fact that MTTs are proof systems with proof-theoretic semantics has another significant and practical consequence in natural language reasoning based on MTT-semantics. In particular, this makes it possible for MTTs to be implemented in proof assistants such as Agda (Agda 2008), Coq (Coq 2010) and Lego/Plastic (Luo and Pollack 1992; Callaghan and Luo 2001) – computer-assisted reasoning systems that computer scientists have developed and successfully used for the formalization of mathematics and verification of computer programs. Therefore, MTT-semantics can be directly implemented in proof assistants that implement MTTs: for example, the MTT-semantics in type theory UTT has been implemented in Coq (Chatzikyriakidis and Luo 2014; Luo 2011b) and Plastic (Xue and Luo 2012) and used for natural language reasoning (Chatzikyriakidis and Luo 2016) (see Chapter 6for more details).

That MTTs are proof-theoretically presented has led to a widely held view that formal semantics based on MTTs is only proof-theoretic and, in particular, it is not model-theoretic. 34 This is mistaken – MTT-semantics is also model-theoretic. First of all, it is necessary for us to make clear that, by MTT-semantics being model-theoretic, we do not mean that an MTT can be given a set-theoretical semantics (e.g. in some categorical framework); instead, we mean that an MTT itself can be employed as a meaning-carrying language to give model-theoretic semantics to natural language. That is, in MTT-semantics, an MTT plays the role of meaning-carrying language – in the traditional model-theoretic semantics, this is the role played by set theory. In other words, we argue that MTTs can well serve as a foundational semantic language to give meanings in themselves in a model-theoretic semantics.

We shall develop the theme that MTT-semantics is model-theoretic in two fronts: the first is to note that, like sets in Montague semantics, types in MTTs are employed to represent collections of objects (for example, semantic interpretations of common nouns), and the rich type structure in MTTs provides powerful means of representation for formal semantics. In other words, intuitively, types in MTTs are rich enough to play the role of representing collections, just as sets in Montague semantics.

As mentioned above, MTTs have a rich type structure and, as to be demonstrated in Chapters 3, 4and 5, in MTT-semantics these types play an important role in representing different kinds of collections such as those given by CNs modified by various kinds of adjectives. Such representations by means of types are not available for simple type theory, which has only base types and arrow types. Types in MTTs are powerful and can provide various different representations in semantic constructions. This is the first facet to explicate that MTT-semantics is model-theoretic.

The second facet is that the contextual structures in MTTs, which are not available in traditional logical systems, provide very useful means in semantic constructions and, in particular, they offer effective support for model-theoretic descriptions of incomplete possible worlds. We shall describe the notion of signatures (Luo 2014) (see section 2.1) that allow MTTs to be more suitable to support model-theoretic descriptions.

The notion of signature in type theory, as far as we know, first appeared in Edinburgh Logical Framework (Harper et al . 1993), where signatures with membership entries are used to describe a logical system. 35 We shall introduce signatures that do not just have the usual membership entries of the form x : A but also contain two new forms of entries, subtyping entries and manifest entries (see section 2.4), which strengthen the power of signatures in representing (incomplete) possible worlds, even in cases where, for example, situations are infinite or involve more sophisticated phenomena. As shown in Lungu and Luo (2018) and section 2.5, extending MTTs with signatures, which may contain entries of the above new forms as well as the membership entries, preserves their nice meta-theoretic properties such as strong normalization (and hence logical consistency).

It is worth pointing out that foundational semantic languages that are both model-theoretic and proof-theoretic were not available before the development of MTT-semantics or, at least, people have not recognized that there is such a possibility (in particular, set theory is not such a language since it is not proof-theoretic). MTT-semantics is both model-theoretic and proof-theoretic and sheds a new light on the division between model-theoretic semantics and proof-theoretic semantics and allows us to study formal semantics from a new perspective.

1 1Attribution for the development of simple type theory should also go to the Polish logician Chwistek (see, for example, Linsky 2009).

2 2The term “modern type theory” is adopted to distinguish MTTs, as used in MTT-semantics, from Church’s simple type theory, as used in Montague semantics, and it appeared for the first time in Luo (2009c).

3 3In this respect, interested readers are referred to Logic-enriched Type Theories (LTTs), proposed by Aczel and Gambino in their study of type-theoretic interpretations of constructive set theory (Aczel and Gambino 2000; Gambino and Aczel 2006), and to the work by the second author and Adams on a type-theoretical framework of LTTs to support formal reasoning with different logical foundations, including classical inference as well as intuitionistic inference (Luo 2007; Adams and Luo 2010). Also related is the recent work on homotopy type theory where Martin-Löf’s type theory is employed in such a way that the logic can be either intuitionistic or classical (HoTT 2013).

4 4Although the logic in IL can be used to describe a lot of linguistic features, there are many others still found very difficult, if not impossible, to be characterized in IL (or simple type theory); in the literature, these phenomena are rather studied in set theory directly – see such “direct interpretations” in, for example, Winter (2016). This is one of the reasons that, for Montague semantics, set theory itself is considered the foundational semantic language, rather than the intermediate language IL.

5 5A remark may be necessary here: we are only emphasizing the similarities between type theory and set theory here. However, they are very different – for example, it is their difference that enables us to say that MTT-semantics is also proof-theoretic and can be successfully implemented on computers for natural language reasoning. For some readers, the difference will only be apparent later on, say, after reading Chapter 2to become more familiar with MTTs.

6 6Our description of simple type theory is formal and, in section 7.2, will be extended with dependent event types, one of the applications of dependent types in Davidsonian event semantics.

7 7IL as described in Montague (1973) also contains a modal operator used to describe tense. As noted in Montague (1973), it can be considered as a special predicate symbol to be interpreted as intended. We omit it here.

8 8For those who are unfamiliar with natural deduction rules, it may be worth remarking that the rules below define a natural deduction system whose sentences are called judgments. A judgment J is correct (formally called derivable) if there is a derivation of J, that is, a finite sequence of judgments J1, ..., Jn with Jn = J such that, for all 1 ≤ i ≤ n, Ji is the conclusion of an instance of some inference rule whose premises are in {Jk | k < i }.

9 9Here, the names of the base types e and t follow the Montagovian tradition. In Church (1940), e and t are named ι and o, respectively.

10 10As in λ-calculus, β-conversion holds: we have that (λx:A.b[x])(a) is convertible to b[a], notation (λx:A.b[x])(a) ≈ b[a], where b[a] is obtained from b[x] by substituting a for all free occurrences of x. In other words, these two expressions (λx:A.b[x])(a) and b[a] are computationally the same – the former computes to the latter, and the relation ≈ of β-conversion is the reflexive, symmetric and transitive closure of this basic computational relation.