Hostname: page-component-8448b6f56d-c4f8m Total loading time: 0 Render date: 2024-04-16T11:25:39.302Z Has data issue: false hasContentIssue false
  • English
  • Français

The generalised type-theoretic interpretation of constructive set theory

Published online by Cambridge University Press:  12 March 2014

Nicola Gambino  and
Peter Aczel
Nicola Gambino
Affiliation:
Laboratoire de Combinatoire et Informatique Mathématique, Université du Québec à Montréal, Case Postale 8888, Succursale Centre-Ville, Montréal (Québec) H3C 3P8, Canada. E-mail: gambino@math.uqam.ca
Peter Aczel
Affiliation:
Schools of Mathematics and Computer Science, University of Manchester, Manchester M13 9Pl, England. E-mail: petera@cs.man.ac.uk
Get access Rights & Permissions [Opens in a new window]

Abstract

We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.

Keywords

Key words and phrases. Constructive Set TheoryDependent Type Theory
Type
Research Article
Information
The Journal of Symbolic Logic , Volume 71 , Issue 1 , March 2006 , pp. 67 - 103
Copyright
Copyright © Association for Symbolic Logic 2006

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Aczel, P., The type theoretic interpretation of constructive set theory, Logic Colloquium '77 (MacIntyre, A., Pacholski, L., and Paris, J., editors), North-Holland, 1978, pp. 55–66.CrossRefGoogle Scholar
[2]Aczel, P., The type theoretic interpretation of constructive set theory: choice principles, The L. E. J. Brouwer Centenary Symposium (Troelstra, A. S. and van Dalen, D., editors), North-Holland, 1982, pp. 1–40.Google Scholar
[3]Aczel, P., The type theoretic interpretation of constructive set theory: inductive definitions, Logic, methodology and philosophy of science VII (Marcus, R. Barcan, Dorn, G.J.W., and Weinegartner, P., editors), North-Holland, 1986, pp. 17–49.Google Scholar
[4]Aczel, P. and Gambino, N., Collection principles in Dependent Type Theory, Types for proofs and programs (Callaghan, P., Luo, Z., McKinna, J., and Pollack, R., editors), Lecture Notes in Computer Science, vol. 2277, Springer, 2002, pp. 1–23.CrossRefGoogle Scholar
[5]Aczel, P. and Rathjen, M., Notes on Constructive Set Theory, Technical Report 40, Mittag-Leffler Institute, The Swedish Royal Academy of Sciences, 2001, available from the first author's web page at http://www.cs.man.ac.uk/~petera/papers.html.Google Scholar
[6]Awodey, S. and Bauer, A., Propositions as [types], Journal of Logic and Computation, vol. 14 (2004), no. 4, pp. 447–471.CrossRefGoogle Scholar
[7]Awodey, S. and Warren, M., Predicative algebraic set theory, Theory and applications of categories, vol. 15(2005), no. 1, pp. 1–39.Google Scholar
[8]Coquand, T., Sambin, G., Smith, J. M., and Valentini, S., Inductively generated formal topologies, Annals of Pure and Applied Logic, vol. 124 (2003), no. 1-3, pp. 71–106.CrossRefGoogle Scholar
[9]Friedman, H. M., The consistency of classical set theory relative to a set theory with intuitionistic logic, this Journal, vol. 38 (1973), pp. 315–319.Google Scholar
[10]Friedman, H. M., Set theoretic foundations of constructive analysis, Annals of Mathematics, vol. 105 (1977), pp. 1–28.CrossRefGoogle Scholar
[11]Gambino, N., Types and sets: a study on the jump to full impredicativity, Laurea dissertation, Dipartimento di Matematica Pura e Applicata, Università degli Studi di Padova, 1999.Google Scholar
[12]Gambino, N., Sheaf interpretations for generalised predicative intuitionistic systems, Ph.D. thesis, University of Manchester, 2002, available from the author's web page.Google Scholar
[13]Gambino, N., Presheaf models for constructive set theory, From Sets and Types to Topology and Analysis (Crosilla, L. and Schuster, P., editors), Oxford University Press, 2005, pp. 62–77.CrossRefGoogle Scholar
[14]Gambino, N., Heyting-valued interpretations for Constructive Set Theory, Annals of Pure and Applied Logic, vol. 137 (2006), no. 1-3, pp. 164–188.CrossRefGoogle Scholar
[15]Grayson, R. J., Heyting-valued models for Intuitionistic Set Theory, Applications of sheaves (Fourman, M. P., Mulvey, C. J., and Scott, D. S., editors), Lecture Notes in Mathematics, vol. 753, Springer, 1979, pp. 402–414.CrossRefGoogle Scholar
[16]Grayson, R. J., Forcing in intuitionistic systems without power-set, this Journal, vol. 48 (1983), no. 3, pp. 670–682.Google Scholar
[17]Griffor, E. R. and Rathjen, M., The strength of some Martin-Löf type theories. Archive for Mathematical Logic, vol. 33 (1994), pp. 347–385.CrossRefGoogle Scholar
[18]Jacobs, B., Categorical logic and type theory, North-Holland, 1999.Google Scholar
[19]Johnstone, P. T., Stone spaces, Cambridge University Press, 1982.Google Scholar
[20]Lubarsky, R. S., Independence results around constructive ZF, Annals of Pure and Applied Logic, vol. 132 (2005), no. 2-3, pp. 209–225.CrossRefGoogle Scholar
[21]MacLane, S. and Moerduk, I., Sheaves in Geometry and Logic, Springer, 1992.Google Scholar
[22]Maietti, M. E., The type theory of categorical universes, Ph.D. thesis, Dipartimento di Matematica Pura e Applicata, Università degli Studi di Padova, 1998, available from the author's web page.Google Scholar
[23]MacLane, S. and Moerduk, I., Modular correspondence between dependent type theories and categories including pretopoi and topoi, Mathematical Structures in Computer Science, to appear.Google Scholar
[24]Maietti, M. E. and Sambin, G., Towards a minimalistic foundation for constructive mathematics, From sets and types to topology and analysis (Crosilla, L. and Schuster, P., editors), Oxford University Press, 2005, pp. 91–114.CrossRefGoogle Scholar
[25]Makkai, M., First-order logic with dependent sorts, with applications to category theory, available from the author's web page, 1995.Google Scholar
[26]Makkai, M., Towards a categorical foundation of mathematics, Logic Colloquium '95 (Makowsky, J. A. and Ravve, E.V., editors), Lecture Notes in Logic, vol. 11, Association for Symbolic Logic, 1998, pp. 153–190.Google Scholar
[27]Makkai, M., On comparing definitions of weak n-category, available from the author's web page, 2001.Google Scholar
[28]Martin-Löf, P., Intuitionistic type theory — Notes by G. Sambin of a series of lectures given in Padua, June 1980, Bibliopolis, 1984.Google Scholar
[29]Moerduk, I. and Palmgren, E., Wellfounded trees in categories, Journal of Pure and Applied Logic, vol. 104 (2000), pp. 189–218.CrossRefGoogle Scholar
[30]Moerduk, I. and Palmgren, E., Type theories, toposes and Constructive Set Theory: predicative aspects of AST, Annals of Pure and Applied Logic, vol. 114 (2002), no. 1-3, pp. 155–201.CrossRefGoogle Scholar
[31]Myhill, J.R., Constructive Set Theory, this Journal, vol. 40 (1975), no. 3, pp. 347–382.Google Scholar
[32]Nordström, B., Petersson, K., and Smith, J. M., Martin-Löf Type Theory, Handbook of Logic in Computer Science (Abramski, S., Gabbay, D. M., and Maibaum, T. S. E., editors), vol. 5, Oxford University Press, 2000.Google Scholar
[33]Rathjen, M., The disjunction and related properties for Constructive Zermelo-Frankel Set Theory, this Journal, vol. 70 (2005), no. 4, pp. 1233–1254.Google Scholar
[34]Rathjen, M., Replacement versus Collection in Constructive Zermelo-Fraenkel Set Theory, Annals of Pure and Applied Logic, vol. 136 (2005), no. 1-2, pp. 156–174.CrossRefGoogle Scholar
[35]Rathjen, M., Realizability for Constructive Zermelo-Fraenkel Set Theory, Logic colloquium '03 (Väänänen, J. and Stoltenberg-Hansen, V., editors), Lecture Notes in Logic, vol. 24, Association for Symbolic Logic and AK Peters, 2006, pp. 282–314.CrossRefGoogle Scholar
[36]Rathjen, M. and Lubarsky, R. S., On the regular extension axiom and its variants, Mathematical Logic Quarterly, vol. 49 (2003), no. 5, pp. 511–518.CrossRefGoogle Scholar
[37]Sambin, G., Intuitionistic formal spaces-A first communication, Mathematical Logic and its Applications (Skordev, D., editor), Plenum, 1987, pp. 87–204.Google Scholar
[38]Sambin, G., Some points informal topology, Theoretical Computer Science, vol. 305 (2003), no. 1–3, pp. 347–408.CrossRefGoogle Scholar
[39]Sambin, G. and Valentini, S., Building up a toolbox for Martin-Löf's type theory: subset theory, Twenty-five years of Constructive Type Theory (Sambin, G. and Smith, J. M., editors), Oxford University Press, 1998, pp. 221–244.CrossRefGoogle Scholar