Résumé
When computing compositionally the meaning of a sentence, depicted as a logical formula, one starts from the word senses, that are partial formulae, and combines them in accordance with the parse structure. This process involves two logics. The glue logic which combines the partial formulae: this is a lambda calculus, the lambda terms being intuitionistic propositional proofs—in Montague semantics, this logic is simply typed lambda calculus over two types, entities and truth-values (or propositions). Let us call target logic the other logic; its formulae are used to represent the meaning of the sentence—the target logic usually is higher order or first order logic. Our framework makes use of second order lambda calculus (system F) as the glue logic and many-sorted higher order logic as the target logic. The motivation for having many base types is to model restrictive selection (to leave out sentences like “The table whistles.”, to accept one like “Liverpool is an important harbour and votes labour.” (location/people) and to reject “Liverpool is an important harbour and won eighteen League titles. (location/football club). Those many base types (or sorts) naturally lead to quantify over types in order to factor operations that act uniformly over types. In such a setting, it is fairly natural to use typed Hilbert operators to express (generalised) quantification. Here we enrich our type system with predefined types, e.g., finite and countable sets (encodings in F are rather dull) and coercive subtyping (which is welcome for representing ontological inclusions like “cars” are “vehicles”) and adapt Hilbert operators to this extended type system.