Formal Semantics in Modern Type Theories

2Modern Type Theories

A modern type theory (MTT) is a computational formal system that involves several fundamental mechanisms that are new to logical systems and have been proven to be very useful in various applications. For instance, the notion of judgments, which are statements in a type theory to make assertions, involves contextual mechanisms that can be employed effectively to describe situations (or incomplete possible worlds) in linguistic semantics.

An MTT has a rich type structure, much richer than the arrow types A → B as found in the Montagovian setting. Besides logical propositions (i.e. types of proofs of propositions according to the Curry-Howard principle of propositions-as-types (Curry and Feys 1958; Howard 1980)), it contains many other types that can be used for various representational purposes in constructing formal semantics. In linguistic semantic studies, people have talked about many-sorted logical systems or multisorted set-theoretical domains. As Link puts it nicely:

Language is able to refer to a wide array of objects of different sorts, which differ from each other in their characteristic structural properties. The universe of linguistic and philosophical discourse is thus most naturally taken as a multi-sorted domain containing all those objects. (Link 1998, Preface).

MTTs are not just many-sorted systems and these “sorts”, or types as they are called, are structured in powerful and rich ways. Their types include those that can be used to interpret ...