Γ ├ 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 made by Carnap (1947) that the intension of an expression be modeled by a function on possible states of affairs whose value, at a particular state, is the extension of the expression in that state. Nearly all constructions in English have some intensional instances (see, for example, a discussion on this in Partee (1988), among others). This has led Montague to give a special treatment of intensionality in his IL. It can be treated by adding a special base type s to simple type theory C, which allows one to consider types like s → A.11
For instance, we may interpret the intension of a sentence as a function from possible worlds to truth values, of type s → t. This approach to intensionality has been extensively studied, although it is not regarded as completely satisfactory in some aspects: for example, it suffers from the so-called problem of logical omniscience in that logically equivalent sentences are regarded as having the same meaning, which may be incorrect in an intensional context. In this book, we shall largely ignore the intensionality issue, with some exceptions,12 not because it is not important (it obviously
