Abstract
Recent debates in metaphysics have highlighted the significance
of type theories, such as Simple Type Theory (STT), for our
philosophical analysis. In this chapter, I present the salient features of
a constructive type theory in the style of Martin-Löf, termed CTT. My
principal aim is to convey the flavour of this rich, flexible and sophisticated
theory and compare it with STT. I especially focus on the forms
of quantification which are available in CTT. A further aim is to argue
that a comparison between a plurality of theories is beneficial to the
philosophical analysis. We may, for example, discover helpful features
of one theory that we may want to import into another context, thus
enriching our repertoire of formal tools. Or, through comparison with
a less well-known theory, we may gain a better understanding of the
characteristics of the theories we are familiar with. As argued in this
chapter, CTT has much to offer in all of these respects.