A minimalist two-level foundation for constructive mathematics

Annals of Pure and Applied Logic 160 (3):319-354 (2009)
  Copy   BIBTEX

Abstract

We present a two-level theory to formalize constructive mathematics as advocated in a previous paper with G. Sambin.One level is given by an intensional type theory, called Minimal type theory. This theory extends a previous version with collections.The other level is given by an extensional set theory that is interpreted in the first one by means of a quotient model.This two-level theory has two main features: it is minimal among the most relevant foundations for constructive mathematics; it is constructive thanks to the way the extensional level is linked to the intensional one which fulfills the “proofs-as-programs” paradigm and acts as a programming language

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2009.01.006

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 106,951

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Consistency of the intensional level of the Minimalist Foundation with Church’s thesis and axiom of choice.Hajime Ishihara, Maria Emilia Maietti, Samuele Maschio & Thomas Streicher - 2018 - Archive for Mathematical Logic 57 (7-8):873-888.
Quotient Completion for the Foundation of Constructive Mathematics.Maria Emilia Maietti & Giuseppe Rosolini - 2013 - Logica Universalis 7 (3):371-402.
Why Topology in the Minimalist Foundation Must be Pointfree.Maria Emilia Maietti & Giovanni Sambin - 2013 - Logic and Logical Philosophy 22 (2):167-199.
Quotient topologies in constructive set theory and type theory.Hajime Ishihara & Erik Palmgren - 2006 - Annals of Pure and Applied Logic 141 (1):257-265.
Inaccessible set axioms may have little consistency strength.L. Crosilla & M. Rathjen - 2002 - Annals of Pure and Applied Logic 115 (1-3):33-70.
Elementary Constructive Operational Set Theory.Andrea Cantini & Laura Crosilla - 2010 - In Ralf Schindler, Ways of Proof Theory. De Gruyter. pp. 199-240.
Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
Extensionality Versus Constructivity.Silvio Valentini - 2002 - Mathematical Logic Quarterly 48 (2):179-187.
Fundamentals of the CTT Approach.Shahid Rahman & Nicolas Clerbout - unknown
Stewart Shapiro. Introduction—intensional mathematics and constructive mathematics. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, vol. 113, North-Holland, Amsterdam, New York, and Oxford, 1985, pp. 1–10. - Stewart Shapiro. Epistemic and intuitionistic arithmetic. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 11–46. - John Myhill. Intensional set theory. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 47–61. - Nicolas D. Goodman. A genuinely intensional set theory. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 63–79. - Andrej Ščedrov. Extending Godel's modal interpretation to type theory and set theory. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 81–119. - Robert C. Flagg. Church's. [REVIEW]Craig A. Smorynski - 1991 - Journal of Symbolic Logic 56 (4):1496-1499.

Analytics

Added to PP
2013-12-22

Downloads
45 (#555,858)

6 months
8 (#540,103)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Studies in logical theory.John Dewey - 1903 - New York: AMS Press.
Constructive Type Theory, an appetizer.Laura Crosilla - 2024 - In Peter Fritz & Nicholas K. Jones, Higher-Order Metaphysics. Oxford University Press.

View all 16 citations / Add more citations

References found in this work

Constructivism in Mathematics: An Introduction.A. S. Troelstra & Dirk Van Dalen - 1988 - Amsterdam: North Holland. Edited by D. van Dalen.
Adjointness in Foundations.F. William Lawvere - 1969 - Dialectica 23 (3‐4):281-296.
Choice Implies Excluded Middle.N. Goodman & J. Myhill - 1978 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 24 (25-30):461-461.
Choice Implies Excluded Middle.N. Goodman & J. Myhill - 1978 - Mathematical Logic Quarterly 24 (25‐30):461-461.

View all 14 references / Add more references