Many tests that semanticists use in their research rely on reasoning tests. For example, if we know that all space aliens love chocolate, and we learn that Mary is a space alien, then we also know that Mary loves chocolate. Apart from providing fundamental information about space aliens, this argument reveals certain properties of the determiner “all”.

Putting the argument above into a grammar implementation with access to reasoning systems immediately encounters serious difficulties. One that will concern us in this talk has to do with the fact that well-developed logical reasoners hardly go beyond first-order predicate logic, whereas semanticists often employ much more expressive higher-order logics. This means that modern off-the-shelf reasoners capture the behavior of quantifiers like “all” and the statements about the culinary preferences of space aliens in general and of Mary in particular, but a treatment of intensional predicates such as the verb expressing your _knowledge_ about space aliens and Mary and our resulting _knowledge_ about Mary’s dietary inclination are beyond current standard tools.

In this talk I will review an old idea by Leon Henkin (1950), Henkin Semantics for higher-order logics, and show how his insights can be used to apply first-order theorem provers and model builders in higher-order reasoning based on Montague Grammar. An experiment in which a grammar of English together with a reasoning system is tasked with solving typical reasoning problems of formal semanticists demonstrates both the power and the limits of such an architecture.