Constructive type theory, an appetizer

Dibattiti recenti in metafisica hanno dimostrato l'importanza per l'analisi filosofica di teorie dei tipi quali la teoria dei tipi semplici (STT). In questo capitolo presento gli aspetti salienti di una teoria dei tipi nello stile di Martin-Löf che chiamo CTT. Il mio scopo principale è convenire il senso di questa teoria sofisticata, la sua ricchezza e flessibilità e confrontarla con STT. Mi interesso soprattutto delle forme di quantificazione disponibili in CTT. Ulteriore scopo è dimostrare che un confronto tra una pluralità di approcci a teorie dei tipi è benefico per l'analisi filosofica. Possiamo, per esempio, scoprire caratteristiche di una teoria che possono essere "importate" in un'altra, arricchendo così il nostro repertorio di strumenti formali. Oppure attraverso un confronto con teorie meno note possiamo comprendere meglio le caratteristiche stesse delle teorie che conosciamo già bene. Come dimostrato in questo capitolo, CTT ha molto da offrirci su tutti questi aspetti. 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.