The Internal Logic of Constructive Mathematics

  • Yvon Gauthier
Part of the Studies in Universal Logic book series (SUL)


Mathematical constructivism could be summarized by the phrase: “Arithmetical statements proven by analytical means can be proven without them, that is by elementary non-analytical means”. Herbrand expressed the idea clearly in the 1920s. It was repeated recently by H. Friedman, following Avigad (2003). The classical example in this connection is Dirichlet who proved in 1837 the prime number theorem and the theorem on arithmetical progressions by analytical means; the elementary proofs were provided only in 1949 by Selberg and Erdös. A less known example is the 1933 Gel’fond-Schneider theorem for which Gel’fond gave a constructive version in the 1960s. I give here a brief account of the theorem and its foundational implications.


Intuitionistic Logic Double Negation Sequent Calculus General Arithmetic Existential Quantifier 
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.


  1. J. Avigad (2003): Number Theory and Elementary Arithmetic. Philosophia Mathematica, XI:257–284.Google Scholar
  2. A. Baker (1975): Transcendental Number Theory. London, Cambridge, University Press.zbMATHCrossRefGoogle Scholar
  3. E. Bishop (1967): Foundations of Constructive Analysis. New York, McGraw-Hill.zbMATHGoogle Scholar
  4. E. Bishop (1970): Mathematics as a Numerical Language. In Intuitionism and Proof Theory, 53–71. North-Holland, Amsterdam and New-York.Google Scholar
  5. L.E.J. Brouwer (1975): Collected Works, vol. I. North-Holland, Oxford, Amsterdam.Google Scholar
  6. T. Coquand (2008): Herbrand et le programme de Hilbert. Gazette des Mathématiciens, 118:17–28.zbMATHMathSciNetGoogle Scholar
  7. P. de Fermat (1899): Oeuvres, volume II. Gauthier-Villars, Paris.Google Scholar
  8. M. Dummett (2000): Elements of Intuitionism. Oxford University Press, Oxford, 2nd édition.Google Scholar
  9. Y. Gauthier (1976): Fondements des mathématiques. Introduction à une philosophie constructiviste. P.U.M., Montréal.zbMATHGoogle Scholar
  10. Y. Gauthier (1978): Foundational Problems of Number Theory. Notre Dame Journal of Formal Logic, 19:92–100.zbMATHMathSciNetCrossRefGoogle Scholar
  11. Y. Gauthier (1997a): Logique et fondements des mathématiques. Diderot, Paris.zbMATHGoogle Scholar
  12. Y. Gauthier (1997b): La logique interne. Modèles et applications. Diderot, Paris.Google Scholar
  13. Y. Gauthier (2002): Internal Logic. Foundations of Mathematics from Kronecker to Hilbert. Kluwer, Synthese Library, Dordrecht/Boston/London.zbMATHGoogle Scholar
  14. Y. Gauthier (2010): Logique Arithmétique. L’arithmétisation de la logique. Presses de l’Université Laval, Québec.Google Scholar
  15. A. O. Gel’fond (1934): Sur le Septième Problème de Hilbert. Comptes Rendus Acad. Sci. URSS Moscou, 2:1–6.MathSciNetGoogle Scholar
  16. A. O. Gel’fond and U. V. Linnik (1965): Elementary Methods in Analytic Number Theory. Rand McNally and Co.Google Scholar
  17. G. Gentzen (1969): Collected Papers. E. Szabo, ed. North-Holland, Amsterdam.Google Scholar
  18. J. Herbrand (1968): Écrits logiques. J. van Heijenoort, ed. PUF, Paris.Google Scholar
  19. S. C. Kleene and J. Vesley (1965): Foundations of Intuitionistic Mathematics. North-Holland, Amsterdam.zbMATHGoogle Scholar
  20. G. Kreisel (1976): What have we learnt from Hilbert’s Second Problem? Mathematical Developments arising from Hilbert’s Problems. Providence, Rhode Island: American Mathematical Society., 93–130.Google Scholar
  21. S. Mochizuki: Inter-universal Teichmüller Theory iv. Log-volume Computations and Set-theoretic Foundations. Homepage of S. Mochizuki (2012).Google Scholar
  22. G. Peano (1959): Opere scelte, vol. II. Edizione Cremonese, Roma.Google Scholar
  23. T. Schneider (1934a): Transzendenzuntersuchungen periodischer Funktionen. J. reine angew. Math., 172:65–69.Google Scholar
  24. T. Schneider (1934b): Transzendenzuntersuchungen periodischer Funktionen. ii. J. reine angew. Math., 172:70–74.Google Scholar
  25. J.-P. Serre (2009): How to use finite fields for problems concerning infinite fields. Proc. Conf. Marseille-Luminy (2007), Contemporary Math. Series, AMS., 1–12.Google Scholar
  26. A. S. Troelstra (1969): Principles of Intuitionism. Numéro 95 de Lectures Notes in Mathematics. Springer, Berlin Heidelberg New York.Google Scholar
  27. A. S. Troelstra (1976): Choice Sequences. Clarendon Press, Oxford.Google Scholar
  28. A. S. Troelstra (2003): Constructivism and Proof Theory. ILLC, University van Amsterdam.Google Scholar
  29. A. S. Troelstra and D.van Dalen (1988): Constructivism in Mathematics. vol. I. North-Holland, Amsterdam.Google Scholar
  30. V. Voevodsky (2010): Univalent Foundation Project. (A modified version of an NSF grant application). October 1.Google Scholar
  31. A Weil (1941): On the Riemann Hypothesis in Function Fields. Proc. Natl. Acad. Sci. USA, 27:345–347.zbMATHMathSciNetCrossRefGoogle Scholar
  32. A. Weil (1949): Numbers of solutions of equations in finite fields. Bull. Am. Math. Soc., 55:497–508.zbMATHMathSciNetCrossRefGoogle Scholar
  33. A. Weil (1984): Number Theory. An Approach through History. From Hammurabi to Legendre. Birkhäuser. Boston-Basel-Berlin.Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Yvon Gauthier
    • 1
  1. 1.University of MontrealMontrealCanada

Personalised recommendations