Abstract
Within Per Martin-Löf’s Constructive Type Theory (CTT for short) the logical constants are interpreted through the Curry-Howard correspondence between propositions and sets. A proposition is interpreted as a set whose elements represent the proofs of the proposition. It is also possible to view a set as a problem description in a way similar to Kolmogorov’s explanation of the intuitionistic propositional calculus.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
- 3.
For a thorough discussion see Granström (2011, pp. 54–76).
- 4.
Martin-Löf used the sign “\(\in \)” in order to indicate that something, say a, is of some type, say B. He even suggests to understand it as a the copula ‘is’. Nordström et al. (1990) also uses this notation while other authors such as Ranta (1994) use the colon. Granström (2011) distinguishes the colon from the epsilon, where the first applies to non-canonical elements and the latter to canonical ones. We will use the colon.
- 5.
Cf. Granström (2011, pp. 111–112).
- 6.
Cf. Ranta (1991, Sect. 3).
References
Granström, J. 2011. Treatise on Intuitionistic Type Theory. Dordrecht: Springer.
Martin-Löf, P. 1984. Intuitionistic Type Theory. Naples: Bibliopolis. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980.
Nordström, B., K. Petersson, and J.M. Smith. 1990. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford: Oxford University Press.
Ranta, A. 1991. Constructing possible worlds. Theoria 57(1–2): 77–99.
Ranta, A. 1994. Type-Theoretical Grammar. Oxford: Clarendon Press.
Sundholm, G. 1997. Implicit epistemic aspects of constructive logic. Journal of Logic, Language and Information 6(2): 191–212.
Sundholm, G. 2001. A plea for logical atavism. In The Logica Yearbook 2000, ed. O. Majer, 151–162. Prague: Filosofia.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2015 The Author(s)
About this chapter
Cite this chapter
Clerbout, N., Rahman, S. (2015). Brief Reminder of Constructive Type Theory. In: Linking Game-Theoretical Approaches with Constructive Type Theory. SpringerBriefs in Philosophy. Springer, Cham. https://doi.org/10.1007/978-3-319-19063-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-19063-1_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19062-4
Online ISBN: 978-3-319-19063-1
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)