Reinhard Muskens (Tilburg University)
Intensional models for the theory of types
In this tutorial I will explain how the simple theory of types (Church 1940) can be provided with a semantics that makes the axiom of extensionality fail, but supports classical reasoning with the usual logical operators. The interest in the resulting logic, which has a very simple Gentzen sequent formalization, comes from the fact that it allows one to evade certain logical difﬁculties such as the problem of logical omniscience. While Extensionality is a reasonable assumption in mathematics, it is somewhat of a show-stopper in applications of logic to artiﬁcial intelligence or natural language. The semantics to a large degree implements Frege’s idea that all signs that have a referent, also come with a sense.
It will be explained how this semantics generalizes that of Henkin 1950 in that if it is assumed that certain functions from senses to referents are injective we essentially obtain his general models. If it is assumed, moreover, that these functions
are also onto certain sets of relations, one gets full (or "standard") models.
It will be shown how in a fully intensional type theory it is possible to construct possible worlds as certain properties of propositions and it will also be shown how the theory can be used to translate a small fragment of natural language to logic,
in Montague’s fashion.
The tutorial will stress ideas rather than technicalities. Those who want both and those who want to prepare in advance are invited to have a look at the following paper. http://let.uvt.nl/general/people/rmuskens/pubs/intensional.pdf