Document Open Access Logo

An Extensional Kleene Realizability Semantics for the Minimalist Foundation

Authors Maria Emilia Maietti, Samuele Maschio

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2014.162.pdf
  • Filesize: 0.63 MB
  • 25 pages

Document Identifiers

Author Details

Maria Emilia Maietti
Samuele Maschio

Cite AsGet BibTex

Maria Emilia Maietti and Samuele Maschio. An Extensional Kleene Realizability Semantics for the Minimalist Foundation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 162-186, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.TYPES.2014.162

Abstract

We build a Kleene realizability semantics for the two-level Minimalist Foundation MF, ideated by Maietti and Sambin in 2005 and completed by Maietti in 2009. Thanks to this semantics we prove that both levels of MF are consistent with the formal Church Thesis CT. Since MF consists of two levels, an intensional one, called mtt, and an extensional one, called emtt, linked by an interpretation, it is enough to build a realizability semantics for the intensional level mtt to get one for the extensional one emtt, too. Moreover, both levels consists of type theories based on versions of Martin-Löf's type theory. Our realizability semantics for mtt is a modification of the realizability semantics by Beeson in 1985 for extensional first order Martin-Löf's type theory with one universe. So it is formalized in Feferman's classical arithmetic theory of inductive definitions, called ID1^. It is called extensional Kleene realizability semantics since it validates extensional equality of type-theoretic functions extFun, as in Beeson's one. The main modification we perform on Beeson's semantics is to interpret propositions, which are defined primitively in MF, in a proof-irrelevant way. As a consequence, we gain the validity of CT. Recalling that extFun+CT+AC are inconsistent over arithmetics with finite types, we conclude that our semantics does not validate the Axiom of Choice AC on generic types. On the contrary, Beeson's semantics does validate AC, being this a theorem of Martin-Löf's theory, but it does not validate CT. The semantics we present here seems to be the best approximation of Kleene realizability for the extensional level emtt. Indeed Beeson's semantics is not an option for emtt since AC on generic sets added to it entails the excluded middle.
Keywords
  • Realizability
  • Type Theory
  • formal Church Thesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. G. Barthes, V. Capretta, and O. Pons. Setoids in type theory. J. Funct. Programming, 13(2):261-293, 2003. Special issue on "Logical frameworks and metalanguages". Google Scholar
  2. M. Beeson. Foundations of Constructive Mathematics. Springer-Verlag, Berlin, 1985. Google Scholar
  3. E. Bishop. Foundations of Constructive Analysis. McGraw-Hill Book Co., 1967. Google Scholar
  4. T. Coquand. Metamathematical investigation of a calculus of constructions. In P. Odifreddi, editor, Logic in Computer Science, pages 91-122. Academic Press, 1990. Google Scholar
  5. S. Feferman. Iterated inductive fixed-point theories: application to Hancock’s conjecture. In Patras Logic Symposion, pages 171-196. North Holland, 1982. Google Scholar
  6. M. Hofmann. Extensional Constructs in Intensional Type Theory. Distinguished Dissertations. Springer, 1997. Google Scholar
  7. J. M. E. Hyland. The effective topos. In The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), volume 110 of Stud. Logic Foundations Math., pages 165-216. North-Holland, Amsterdam-New York, 1982. Google Scholar
  8. J. M. E. Hyland, P. T. Johnstone, and A. M. Pitts. Tripos theory. Bull. Austral. Math. Soc., 88:205-232, 1980. Google Scholar
  9. M. E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, 2009. Google Scholar
  10. M. E. Maietti and G. Rosolini. Elementary quotient completion. Theory and Applications of Categories, 27(17):445-463, 2013. Google Scholar
  11. M. E. Maietti and G. Rosolini. Quotient completion for the foundation of constructive mathematics. Logica Universalis, 7(3):371-402, 2013. Google Scholar
  12. M. E. Maietti and G. Rosolini. Unifying exact completions. Applied Categorical Structures, DOI 10.1007/s10485-013-9360-5, 2013. Google Scholar
  13. M. E. Maietti and G. Sambin. Toward a minimalist foundation for constructive mathematics. In L. Crosilla and P. Schuster, editor, From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, number 48 in Oxford Logic Guides, pages 91-114. Oxford University Press, 2005. Google Scholar
  14. M. E. Maietti and G. Sambin. Why topology in the Minimalist Foundation must be pointfree. Logic and Logical Philosophy, 22(2):167-199, 2013. Google Scholar
  15. P. Martin-Löf. Notes on Constructive Mathematics. Almqvist & Wiksell, 1970. Google Scholar
  16. P. Martin-Löf. Intuitionistic Type Theory. Notes by G. Sambin of a series of lectures given in Padua, June 1980. Bibliopolis, Naples, 1984. Google Scholar
  17. B. Nordström, K. Petersson, and J. Smith. Programming in Martin Löf’s Type Theory. Clarendon Press, Oxford, 1990. Google Scholar
  18. P. Odifreddi. Classical recursion theory, volume 125 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., 1989. Google Scholar
  19. E. Palmgren. Bishop’s set theory. Slides for lecture at the TYPES summer school, 2005. Google Scholar
  20. A. S. Troelstra and D. van Dalen. Constructivism in mathematics, an introduction, vol. I. In Studies in logic and the foundations of mathematics. North-Holland, 1988. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact