Abstract
The classical theory of types in question is essentially the theory of Martin-Löf [1] but with the law of double negation elimination. I am ultimately interested in the theory of types as a framework for the foundations of mathematics and, for this purpose, we need to consider extensions of the theory obtained by adding ‘well-ordered types,’ for example the type N of the finite ordinals; but the unextended theory will suffice to illustrate the treatment of extensional equality.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Martin-Löf, Per. “An intuitionistic theory of types: predicative part.” In H. E. Rose and J. Shepherdson (ed.), Logic Colloquium ‘73, Amsterdam: North-Holland, 1975, 73–118.
Martin-Löf, Per. “Analytic and synthetic judgements in type theory.” In P. Parrini (ed.), Kant and Contemporary Epistemology, Dordrecht: Kluwer Academic Publishers, 1994, 87–99.
Tait, W. W. “The law of excluded middle and the axiom of choice.” In A. George (ed.) Mathematics and Mind, Oxford: Oxford University Press, 1994, 45–70.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Tait, W.W. (1995). Extensional Equality in the Classical Theory of Types. In: Depauli-Schimanovich, W., Köhler, E., Stadler, F. (eds) The Foundational Debate. Vienna Circle Institute Yearbook [1995], vol 3. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-3327-4_17
Download citation
DOI: https://doi.org/10.1007/978-94-017-3327-4_17
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-4617-8
Online ISBN: 978-94-017-3327-4
eBook Packages: Springer Book Archive