Skip to main content
Springer Nature Link
Log in

A type-free formalization of mathematics where proofs are objects

  • Conference paper
  • First Online:
Types for Proofs and Programs (TYPES 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1512))

Included in the following conference series:

  • 124 Accesses

Abstract

We present a first-order type-free axiomatization of mathematics where proofs are objects in the sense of Heyting-Kolmogorov functional interpretation. The consistency of this theory is open.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

Explore related subjects

Discover the latest articles, books and news in related subjects, suggested using machine learning.

References

  1. P.B. Andrews, Resolution in type theory, The Journal of Symbolic Logic, 36, 3 (1971) pp. 414–432.

    Article  MATH  MathSciNet  Google Scholar 

  2. M.J. Beeson, Foundations of Constructive Mathematics, Springer-Verlag (1985).

    Google Scholar 

  3. G. Boolos, The logic of provability, Cambridge University Press (1993).

    Google Scholar 

  4. N.G. de Bruijn, A Survey of the project automath, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.R. Hindley, J.P. Seldin (Eds.), Academic Press (1980).

    Google Scholar 

  5. A. Church, A formulation of the simple theory of types. The Journal of Symbolic Logic, 5 (1940) pp. 56–68.

    Article  MATH  MathSciNet  Google Scholar 

  6. Th. Coquand, An analysis of Girard's paradox, Rapport de Recherche 531, Institut National de Recherche en Informatique et en Automatique (1986).

    Google Scholar 

  7. Th. Coquand, A new paradox in type theory, Logic, Methodology and Philosophy of Science IX, D. Prawitz, B. Skyrms and D. Westerståhl (Ed.), Elsevier (1994) pp. 555–570.

    Google Scholar 

  8. Th. Coquand, G. Huet, The calculus of constructions, Information and Computation, 76 (1988) pp. 95–120.

    Article  MATH  MathSciNet  Google Scholar 

  9. H.B. Curry, The combinatory foundations of mathematical logic, The Journal of Symbolic Logic, 7, 2, (1942) pp. 49–64.

    Article  MATH  MathSciNet  Google Scholar 

  10. H.B. Curry, R. Feys, Combinatory logic, Vol. 1, North Holland, Amsterdam (1958).

    Google Scholar 

  11. G. Dowek, Lambda-calculus, combinators and the comprehension scheme, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 902 (1995) pp. 154–170. Rapport de Recherche 2565, Institut National de Recherche en Informatique et en Automatique (1995).

    MATH  MathSciNet  Google Scholar 

  12. G. Dowek, Collections, types and sets, Rapport de Recherche 2708, Institut National de Recherche en Informatique et en Automatique (1995). Mathematical Structures in Computer Science (to appear).

    Google Scholar 

  13. G. Dowek, A type-free formalization of mathematics where proofs are objects Rapport de Recherche 2915, Institut National de Recherche en Informatique et en Automatique (1996).

    Google Scholar 

  14. S. Feferman, Finitary inductively presented logics, Logic Colloquium '88, R. Ferro, C. Bonotto, S. Valentini and A. Zanardo (Ed.), North Holland (1989).

    Google Scholar 

  15. S. Feferman, Reflecting on incompleteness, The Journal of Symbolic Logic, 56, 1, (1991) pp. 1–49.

    Article  MATH  MathSciNet  Google Scholar 

  16. J.Y. Girard, Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, Thèse de Doctorat d'État, Université de Paris 7 (1972).

    Google Scholar 

  17. K. Gödel, An interpretation of the intuitionistic propositional calculus, 1933, in K. Gödel collected works, S. Feferman, J.W. Dawson Jr., S.C. Kleene G.H. Moore, R.M. Solovay, J. van Heijenoort (Ed.), Oxford University Press (1986).

    Google Scholar 

  18. V. Halbach, A system of complete and consistent truth, Notre Dame Journal of Formal Logic, 35, 3 (1994) pp. 311–327.

    Article  MATH  MathSciNet  Google Scholar 

  19. W. A. Howard, The Formulæ-as-type notion of construction, 1969, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.R. Hindley, J.P. Seldin (Ed.), Academic Press (1980).

    Google Scholar 

  20. G. Huet, personal communication.

    Google Scholar 

  21. J.L. Krivine, M. Parigot, Programming with proofs, J. Inf. Process. Cybern. EIK 26 (1990) pp. 149–167.

    MATH  MathSciNet  Google Scholar 

  22. V. McGee, How truthlike can a predicate be? A negative result, Journal of Philosophical Logic 14 (1985) pp. 399–410.

    Article  MATH  MathSciNet  Google Scholar 

  23. P. Martin-Löf Constructive mathematics and computer programming, Logic, Methodology and Philosophy of Science VI, 1979, L.J. Cohen, J. Łoś, H. Pfeiffer, K.-P. Podewski (Ed.), North-Holland (1982) pp. 153–175.

    Google Scholar 

  24. P. Martin-Löf, Intuitionistic type theory, Bibliopolis, Napoli (1984).

    Google Scholar 

  25. Ch. Paulin-Mohring, Inductive definitions in the system COQ, Rules and properties, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 664 (1993) pp. 328–345.

    Article  MATH  MathSciNet  Google Scholar 

  26. Ch. Paulin-Mohring, B. Werner, Synthesis of ML programs in the system Coq, Journal of Symbolic Computation, 15, 5–6 (1993) pp. 607–640.

    MATH  MathSciNet  Google Scholar 

  27. G. Plotkin. Building-in equational theories, Machine Intelligence, 7 (1972) pp. 73–90.

    MATH  MathSciNet  Google Scholar 

  28. W. W. Tait, Infinitely long terms of transfinite type, Formal Systems and Recusrive Functions, J.N. Crossley, M. Dummett (Ed.), North-Holland (1965).

    Google Scholar 

  29. A.N. Whitehead, B. Russell, Principia mathematica, Cambridge University Press (1910–1913, 1925–1927).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA-Rocquencourt, B.P. 105, 78153, Le Chesnay Cedex, France

    Gilles Dowek

Authors
  1. Gilles Dowek
    View author publications

    Search author on:PubMed Google Scholar

Editor information

Eduardo Giménez Christine Paulin-Mohring

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dowek, G. (1998). A type-free formalization of mathematics where proofs are objects. In: Giménez, E., Paulin-Mohring, C. (eds) Types for Proofs and Programs. TYPES 1996. Lecture Notes in Computer Science, vol 1512. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0097788

Download citation

  • DOI: https://doi.org/10.1007/BFb0097788

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65137-6

  • Online ISBN: 978-3-540-49562-8

  • eBook Packages: Springer Book Archive

Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Publish with us

Policies and ethics