A Comparison of Type Theory with Set Theory

In Deniz Sarikaya, Deborah Kant & Stefania Centrone (eds.), Reflections on the Foundations of Mathematics. Springer Verlag. pp. 271-292 (2019)
  Copy   BIBTEX

Abstract

This paper discusses some of the ways in which Martin-Löf type theory differs from set theory. The discussion concentrates on conceptual, rather than technical, differences. It revolves around four topics: sets versus types; syntax; functions; and identity. The difference between sets and types is spelt out as the difference between unified pluralities and kinds, or sorts. A detailed comparison is then offered of the syntax of the two languages. Emphasis is placed on the distinction between proposition and judgement, drawn by type theory, but not by set theory. Unlike set theory, type theory treats the notion of function as primitive. It is shown that certain inconveniences pertaining to function application that afflicts the set- theoretical account of functions are thus avoided. Finally, the distinction, drawn in type theory, between judgemental and propositional identity is discussed. It is argued that the criterion of identity for a domain cannot be formulated in terms of propositional identity. It follows that the axiom of extensionality cannot be taken as a statement of the criterion of identity for sets.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Eta-rules in Martin-löf type theory.Ansten Klev - 2019 - Bulletin of Symbolic Logic 25 (3):333-359.
Property theory and the revision theory of definitions.Francesco Orilia - 2000 - Journal of Symbolic Logic 65 (1):212-246.
Constructive notions of set: Part I. Sets in Martin–Löf type theory.Laura Crosilla - 2005 - Annali Del Dipartimento di Filosofia 11:347-387.
The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
Remarks on the Type Theory in the Semantics of Propositional Attitudes.Oleg A. Domanov - 2018 - Epistemology and Philosophy of Science 55 (4):62-67.
Property Theory of Musical Works.Philip Letts - 2018 - Journal of Aesthetics and Art Criticism 76 (1):57-69.
The Art Type Theory of Art.Robert S. Fudge - 2015 - Philosophical Papers 44 (3):321-343.
Realizing Mahlo set theory in type theory.Michael Rathjen - 2003 - Archive for Mathematical Logic 42 (1):89-101.

Analytics

Added to PP
2019-11-12

Downloads
3 (#1,519,925)

6 months
3 (#445,838)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Ansten Klev
Czech Academy of Sciences

References found in this work

No references found.

Add more references