Formal Semantics in Modern Type Theories

7Advanced Topics

In this chapter, we discuss some advanced topics concerning MTT-semantics. These include work on propositional forms of judgmental interpretations (formal treatment of section 3.2.3), dependent event types (DETs; neo-Davidsonian event semantics with refined event types) and dependent categorial grammars (DCGs; Lambek-style categorical grammars with dependent types). The topics are discussed in the following three sections, which are independent of each other and, as such, can be read independently.

7.1. Propositional forms of judgmental interpretations: formal treatment

As explained in section 3.2.3, in MTT-semantics there are judgmental or ill-typed interpretations and, in order to interpret composite sentences, we may need to turn a judgmental interpretation into a proposition. These can be illustrated by examples whose interpretations involve the following, and the examples are taken from section 3.2.3 (pp. 62–64):

• – derivable judgments: examples include (3.62);
• – non-derivable judgments under negation: examples include (3.66) and (3.67);
• – ill-typed applications under negation: examples include (3.79) and (3.82).

There are propositional forms corresponding to the above judgmental interpretations. Here, we will study them in a more formal and precise way. This section should be read together with the informal introduction to propositional forms in section 3.2.3 and is based on various previous studies (Xue et al. 2018, 2020; Chatzikyriakidis and

Luo ...