butter of current linguistic semantic analysis. One of the most
influential modern semantic formalisms---Montague's PTQ
fragment---included a simply-typed version of the Predicate Calculus
-with lambda abstraction.
+with lambda abstraction.
Montague called the semantic part of his PTQ fragment *Intensional
-Logic*. Montague's IL had three base types: `e`, for individuals,
-`t`, for truth values, and `s` for evaluation indicies (world-time
-pairs). The set of types was defined recursively:
-
- e, t, s are base types
+Logic*. Without getting too fussy about details, we'll present the
+popular Ty2 version of the PTQ types, roughly as proposed by Gallin
+(1975). [See Zimmermann, Ede. 1989. Intensional logic and two-sorted
+type theory. *Journal of Symbolic Logic* ***54.1***: 65--77 for a
+precise characterization of the correspondence between IL and
+two-sorted Ty2.]
+
+We'll need three base types: `e`, for individuals, `t`, for truth
+values, and `s` for evaluation indicies (world-time pairs). The set
+of types is defined recursively:
+
+ the base types e, t, and s are types
if a and b are types, <a,b> is a type
- if a is a type, <s,a> is a type
-So `<e,<e,t>>` and `<s,<<s,e>,t>>` are types, but `<e,s>` is not a
-type. As we have mentioned, this paper is the source for the
-convention in linguistics that a type of the form `<a, b>` corresponds
-to a functional type that we will write here as `a -> b`.
+So `<e,<e,t>>` and `<s,<<s,e>,t>>` are types. As we have mentioned,
+this paper is the source for the convention in linguistics that a type
+of the form `<a, b>` corresponds to a functional type that we will
+write here as `a -> b`. So the type `<a,b>` is the type of a function
+that maps objects of type `a` onto objects of type `b`.
Montague gave rules for the types of various logical formulas. Of
particular interest here, he gave the following typing rules for
functional application and for lambda abstracts:
* If *α* is an expression of type *<a, b>*, and *β* is an
-expression of type b, then *α(β)* has type *b*. * If
-*α* is an expression of type *a*, and *u* is a variable of type
-*b*, then *λuα* has type <code><b, a></code>.
+expression of type b, then *α(β)* has type *b*.
-When we talk about monads, we will investigate Montague's treatment of
-intensionality in some detail. In the meantime, Montague's PTQ
-fragment is responsible for making the simply-typed lambda calculus
-the baseline semantic analysis for linguistics.
+* If α* is an expression of type *a*, and *u* is a variable of
+*type b*, then *λuα* has type <code><b, a></code>.
+When we talk about monads, we will consider Montague's treatment of
+intensionality in some detail. In the meantime, Montague's PTQ is
+responsible for making the simply-typed lambda calculus the baseline
+semantic analysis for linguistics.