Formal Semantics in Modern Type Theories. Stergios Chatzikyriakidis
that derive judgments – sentences in the type theory. For instance, a judgment may be of the form Γ ├ a: A, which means that a is of type A under the assumptions described in context Γ. We shall first explain what contexts and judgments are in C, and then describe its rules.8 (All of C’s inference rules are listed in Appendix A1.1.)
Contexts and Judgments. A context is a sequence of entries either of the form x: A or of the form P true. Informally, the former assumes that the variable x be of type A and the latter that the proposition P be true. Only valid contexts are legal and context validity is governed by the following rules:
where
Judgments are sentences of C, whose correctness is governed by the inference rules below. In C, there are four forms of judgments:
– Γ valid, which means that Γ is a valid context (the rules of deriving context validity are given above);
– Γ ├ A type, which means that A is a type under context Γ;
– Γ ├ a : A, which means that a is an object of type A under context Γ;
– Γ ├ P true, which means that P is a true formula under context Γ.
Inference rules. Besides the context validity rules given above, C has the following rules:
– Rules for base types: e and t are the types of entities and logical formulae, respectively.9
– Assumption rules: one can prove what have been assumed in valid contexts.
– Rules for function types: The formation rule (of function types), introduction rule (of λ-abstraction) and elimination rule (for applications) are as follows, where the terms in the forms of λ-abstractions and applications are related to each other computationally by the relation of β-conversion.10
– Rules for logical formulae formed by implication and universal quantification: their formation, introduction and elimination rules.
where, in the last rule, P (a) is obtained by substituting a for x in P (x).
– Conversion rule for truth of formulas (see footnote 10 for the conversion relation ≈):
Logical operators. The other usual logical operators can be defined by means of ⇒ and ∀. For example, the operators for conjunction and existential quantification can be defined as follows. Other operators such as disjunction and negation can be defined similarly (see Appendix A1.2).
(1.3) P ∧ Q = ∀X : t. (P ⇒ Q ⇒ X) ⇒ X
(1.4) ∃x : A.P (x) = ∀X : t. (∀x : A.(P (x) ⇒ X)) ⇒ X
Table 1.1. Examples in Montague semantics
| Example | Montague semantics | |
| CN | man, human | man, human : e → t |
| IV | talk | talk : e → t |
| ADJ | handsome | handsome : (e → t) → (e → t) |
| ADVVP | quickly | quickly : (e → t) → (e → t) |
| Modified CN | handsome man | handsome(man) : e → t |
| Quantifier | some | some : (e → t) → (e → t) → t |
| S | A man talks | ∃x : e. man(x) & talk(x) : t |
1.3.2. Montague semantics: examples and intensionality
Simple examples in Montague semantics can be found in Table 1.1, briefly showing how to interpret some of the basic linguistic categories in the Montagovian setting, including common nouns (CN), verbs (IV), adjectives (ADJ), verb-modifying adverbs (ADVVP), modified CNs, quantifiers and sentences (S). In the following section, we can find Table 1.3 with examples for these categories interpreted in MTT-semantics. For example, in Montague semantics, verb phrases are interpreted as predicates of type e → t and sentences as formulas of type t, as (1.5) and (1.6) illustrate (see, the lines for IV and S in Table 1.1):
(1.5) talk : e → t
(1.6) ∃x : e.man(x) ∧ talk(x)
A remark we should make is that, in type theories, typing judgments and logical formulas are different. In particular, a typing judgment is not a logical formula: (1.5) is a typing judgment stating that talk is of type e → t, while (1.6) is a logical formula of type t. With such examples, the difference seems to be apparent and there is no need to be emphasized. However, this becomes more important in the setting of modern type theories where much richer typing mechanisms are employed (see, for example, Chapter 2).
A notational convention is adopted in this book: we shall use a different font to represent semantics of a natural language phrase. For instance, for the natural language words “man” and “talk”, we shall use man and talk for their semantics (as in Table 1.1).
A linguistic feature that has been studied carefully in the Montagovian framework is intensionality, following the proposal