Formal Semantics in Modern Type Theories

1Type Theories and Semantic Studies

The long history of the study of semantics has produced a number of theories of meaning. For example, the referential theory adopts a Platonic viewpoint and proposes that meanings are entities in the world; the internalist theory, such as that held by Chomsky, suggests that meanings are concepts in our minds, and the use theory, which is closely related to Wittgenstein’s slogan of “meaning is use”, advocates that meanings are embodied in the ways that language is used in social practice. Besides being very interesting themselves, these philosophical theories have had a profound impact on the ways in which researchers think of and approach formal semantics. For example, many semanticists have been influenced by the referential theory of meaning and believed that formal semantics should be model-theoretic (see, for instance, Portner (2005)), following Tarski’s ideas in model theory for logical systems and Montague’s ideas in set-theoretical semantics for natural language (Montague 1974). On the other hand, the use theory of meaning has convinced many others and has been substantially developed more recently, both by philosophers such as Dummett (1991) and Brandom (1994, 2000) on meaning theories in general and by logicians such as Gentzen (1935), Prawitz (1973, 1974) and Martin-Löf (1984, 1996) on proof-theoretic semantics for logical systems in particular.

This book studies formal semantics in modern type theories (MTT-semantics for short). ...