Advertisement

A Comparison of Type Theory with Set Theory

  • Ansten KlevEmail author
Chapter
Part of the Synthese Library book series (SYLI, volume 407)

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 put 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.

Notes

Acknowledgements

I am grateful to Deborah Kant for inviting me to contribute to this volume. The critical comments of two anonymous readers on an earlier draft helped me in the preparation of the final version of the paper. While writing the paper I have been supported by grant nr. 17-18344Y from the Czech Science Foundation, GAČR.

References

  1. Aczel, P. (1978). The type theoretic interpretation of constructive set theory. In A. Macintyre, L. Pacholski, & J. Paris (Eds.), Logic colloquium 77 (pp. 55–66). Amsterdam: North-Holland.CrossRefGoogle Scholar
  2. Artemov, S., & Fitting, M. (2016). Justification logic. In E. N. Zalta (Ed.), The Stanford encyclopedia of philosophy. Metaphysics Research Lab, Stanford University. https://plato.stanford.edu/archives/win2016/entries/logic-justification/ Google Scholar
  3. Aspinall, D., & Hofmann, M. (2005). Dependent types. In B. C. Pierce (Ed.), Advanced topics in types and programming languages (pp. 45–86). Cambridge: MIT Press.Google Scholar
  4. Barnes, J. (2003). Porphyry. Introduction. Translated with an introduction and commentary. Oxford: Oxford University Press.Google Scholar
  5. Bishop, E. (1967). Foundations of constructive analysis. New York: McGraw-Hill.Google Scholar
  6. Bradley, F. H. (1893). Appearance and reality. Oxford: Clarendon Press. Cited from the Ninth Impression (1930).Google Scholar
  7. Cantor, G. (1882). Ueber unendliche, lineare Punktmannichfaltigkeiten. Nummer 3. Mathematische Annalen, 20, 113–121.CrossRefGoogle Scholar
  8. Cantor, G. (1883). Ueber unendliche, lineare Punktmannichfaltigkeiten. Nummer 5. Mathematische Annalen, 21, 545–591.CrossRefGoogle Scholar
  9. Cantor, G. (1895). Beiträge zur Begründung der transfiniten Mengenlehre (Erster Artikel). Mathematische Annalen, 46, 481–512.CrossRefGoogle Scholar
  10. Carnap, R. (1934). Logische Syntax der Sprache. Vienna: Julius Springer.CrossRefGoogle Scholar
  11. Church, A. (1940). A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 56–68.CrossRefGoogle Scholar
  12. Church, A. (1956). Introduction to mathematical logic. Princeton: Princeton University Press.Google Scholar
  13. Curry, H. B. (1963). Foundations of mathematical logic. New York: McGraw-Hill.Google Scholar
  14. de Bruijn, N. G. (1975). Set theory with type restrictions. In A. Hajnal, R. Rado, & T. Sós (Eds.), Infinite and finite sets: to Paul Erdős on his 60th birthday (pp. 205–214). North-Holland.Google Scholar
  15. de Bruijn, N. G. (1995). Types in mathematics. Cahiers du Centre de Logique, 8, 27–54.Google Scholar
  16. Dedekind, R. (1888). Was sind und was sollen die Zahlen? Braunschweig: Vieweg und Sohn.Google Scholar
  17. Diller, J., & Troelstra, A. (1984). Realizability and intuitionistic logic. Synthese, 60, 253–282.CrossRefGoogle Scholar
  18. Dummett, M. (1973). Frege. Philosophy of language. London: Duckworth. Cited from the second edition (1981).Google Scholar
  19. Dybjer, P. (1994). Inductive families. Formal Aspects of Computing, 6, 440–465.CrossRefGoogle Scholar
  20. Dybjer, P. (2000). A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65, 525–549.CrossRefGoogle Scholar
  21. Frege, G. (1892). Über Begriff und Gegenstand. Vierteljahrsschrift für wissenschaftliche Philosophie, 16, 192–205.Google Scholar
  22. Frege, G. (1893). Grundgesetze der Arithmetik I. Jena: Hermann Pohle.Google Scholar
  23. Frege, G. (1983). Nachgelassene Schriften. Hamburg: Felix Meiner Verlag.Google Scholar
  24. Geach, P. T. (1972). Logic matters. Oxford: Blackwell.Google Scholar
  25. Gentzen, G. (1936). Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112, 493–565.CrossRefGoogle Scholar
  26. Hallett, M. (1984). Cantorian set theory and limitation of size. Oxford: Clarendon Press.Google Scholar
  27. Harper, R., Honsell, F., & Plotkin, G. (1993). A framework for defining logics. Journal of the ACM, 40, 143–184.CrossRefGoogle Scholar
  28. Hausdorff, F. (1914). Grundzüge der Mengenlehre. Leipzig: Veit & Comp.Google Scholar
  29. Hausdorff, F. (2002). Gesammelte Werke. Band II. Heidelberg: Springer.Google Scholar
  30. Hilbert, D. (1899). Grundlagen der Geometrie. Leipzig: Teubner.Google Scholar
  31. Hofmann, M. (1997). Extensional constructs in intensional type theory. London: Springer. Reprint of Ph.D. thesis, University of Edinburgh (1995).Google Scholar
  32. Hofmann, M., & Streicher, T. (1998). The groupoid interpretation of type theory. In G. Sambin & J. M. Smith (Eds.), Twenty-five years of constructive type theory (pp. 83–111). Oxford: Oxford University Press.Google Scholar
  33. Howard, W. A. (1980). The formulae-as-types notion of construction. In J. P. Seldin & J. R. Hindley (Eds.), To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism (pp. 479–490). London: Academic Press.Google Scholar
  34. Husserl, E. (1913). Ideen zu einer reinen Phänomenologie und phänomenologischen Philosophie. Erstes Buch. Halle: Max Niemeyer.Google Scholar
  35. Kirk, G. S., Raven, J. E., & Schofield, M. (1983). The presocratic philosophers (2nd ed.). Cambridge: Cambridge University Press.CrossRefGoogle Scholar
  36. Klev, A. (2017a). Husserl and Carnap on regions and formal categories. In S. Centrone (Ed.), Essays on Husserl’s logic and philosophy of mathematics (pp. 409–429). Dordrecht: Springer.CrossRefGoogle Scholar
  37. Klev, A. (2017b). Truthmaker semantics: Fine versus Martin-Löf. In P. Arazim & T. Lávička (Eds.), The logica yearbook 2016 (pp. 87–108). London: College Publications.Google Scholar
  38. Klev, A. (2018a). The concept horse is a concept. Review of Symbolic Logic, 11, 547–572.CrossRefGoogle Scholar
  39. Klev, A. (2018b). The logical form of identity criteria. In P. Arazim & T. Lávička (Eds.), The logica yearbook 2017 (pp. 181–196). London: College Publications.Google Scholar
  40. Kreisel, G. (1962). Foundations of intuitionistic logic. In E. Nagel, P. Suppes, & A. Tarski (Eds.), Logic, methodology and the philosophy of science (pp. 198–210). Stanford: Stanford University Press.Google Scholar
  41. Linnebo, O. (2010). Pluralities and sets. Journal of Philosophy, 107, 144–164.CrossRefGoogle Scholar
  42. Linnebo, O., & Rayo, A. (2012). Hierarchies ontological and ideological. Mind, 121, 269–308.CrossRefGoogle Scholar
  43. Lowe, E. J. (1989). Kinds of being. Oxford: Basil Blackwell.Google Scholar
  44. Martin-Löf, P. (1982). Constructive mathematics and computer programming. In J. L. Cohen, J. Łoś, et al. (Eds.), Logic, methodology and philosophy of science VI, 1979 (pp. 153–175). Amsterdam: North-Holland.Google Scholar
  45. Martin-Löf, P. (1984). Intuitionistic type theory. Naples: Bibliopolis.Google Scholar
  46. Martin-Löf, P. (2011). When did ‘judgement’ come to be a term of logic? Lecture held at École Normale Supérieure on 14 October 2011. Video recording available at http://savoirs.ens.fr//expose.php?id=481
  47. Meier-Oeser, S. (2001). Vielheit. In J. Ritter, K. Gründer, & G. Gabriel (Eds.), Historisches Wörterbuch der Philosophie (Vol. 11, pp. 1041–1050). Basel: Schwabe.Google Scholar
  48. Nordström, B., Petersson, K., & Smith, J. (1990). Programming in Martin-Löf’s type theory. Oxford: Oxford University Press.Google Scholar
  49. Quine, W. V. (1956). Unification of universes in set theory. Journal of Symbolic Logic, 21, 267–279.CrossRefGoogle Scholar
  50. Russell, B. (1903). Principles of mathematics. Cambridge: Cambridge University Press.Google Scholar
  51. Russell, B., & Whitehead, A. N. (1910). Principia mathematica (Vol. 1). Cambridge: Cambridge University Press.Google Scholar
  52. Schmidt, A. (1938). Über deduktive Theorien mit mehreren Sorten von Grunddingen. Mathematische Annalen, 115, 485–506.CrossRefGoogle Scholar
  53. Schönfinkel, M. (1924). Bausteine der mathematischen Logik. Mathematische Annalen, 92, 305–316.CrossRefGoogle Scholar
  54. Scott, D. (1982). Domains for denotational semantics. In M. Nielsen & E. M. Schmidt (Eds.), Automata, languages and programming (pp. 577–613). Heidelberg: Springer.CrossRefGoogle Scholar
  55. Shoenfield, J. R. (1967). Mathematical logic. Reading: Addison-Wesley.Google Scholar
  56. Streicher, T. (1993). Investigations into intensional type theory. Habilitation thesis, Ludwig Maximilian University Munich.Google Scholar
  57. Sundholm, B. G. (1994). Existence, proof and truth-making: A perspective on the intuitionistic conception of truth. Topoi, 13, 117–126.CrossRefGoogle Scholar
  58. Sundholm, B. G. (2001). Frege, August Bebel and the return of Alsace-Lorraine: The dating of the distinction between Sinn and Bedeutung. History and Philosophy of Logic, 22, 57–73.CrossRefGoogle Scholar
  59. Sundholm, B. G. (2009). A century of judgement and inference, 1837–1936: Some strands in the development of logic. In L. Haaparanta (Ed.), The development of modern logic (pp. 263–317). Oxford: Oxford University Press.CrossRefGoogle Scholar
  60. Sundholm, B. G. (2012). “Inference versus consequence” revisited: Inference, consequence, conditional, implication. Synthese, 187, 943–956.CrossRefGoogle Scholar
  61. The Univalent Foundations Program (2013). Homotopy type theory: Univalent foundations of mathematics. Princeton: Institute for Advanced Study. http://homotopytypetheory.org/book Google Scholar
  62. Wadler, P. (2015). Propositions as types. Communications of the ACM, 58, 75–84. Extended version available at http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf CrossRefGoogle Scholar
  63. Wittgenstein, L. (1922). Tractatus logico-philosophicus. London: Routledge & Kegan Paul.Google Scholar
  64. Zermelo, E. (1930). Über Grenzzahlen und Mengenbereiche. Fundamenta Mathematicae, 16, 29–47.CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Institute of PhilosophyCzech Academy of SciencesPrague 1Czechia

Personalised recommendations