| Monotonicity reasoning is a pervasive phenomenon in natural language semantics. This thesis presents a version of the simply typed lambda calculus, which is naturally interpreted on hierarchies of preorders rather than sets, in order to model this style of reasoning. Rather than using the usual arrow types denoting functions of sets, we instead use two arrow types to represent arbitrary and monotone functions on preorders. To also allow for antitone functions, we include a primitive operation on types to represent opposite preorders. We present several important results for the calculus, including strong normalization, a Church-Rosser Theorem, a Lyndon-type theorem, and the soundness and completeness of the calculus for a general class of models. |
