On Constructive Axiomatic Method

Andrei Rodin


The received notion of axiomatic method stemming from Hilbert  is not fully adequate to the recent successful practice of axiomatizing mathematical theories. The axiomatic architecture of Homotopy type theory (HoTT) does not fit the pattern of formal axiomatic theory in the standard sense of the word.  However this theory falls under a more general and in some respects more traditional notion of axiomatic theory, which I call after Hilbert and Bernays constructive and demonstrate using the Classical example of the First Book of Euclid's  Elements. I also argue that HoTT is not unique in the respect but represents a wider trend in today's mathematics, which also includes Topos theory and some other developments. On the basis of these modern and ancient examples I claim that the received semantic-oriented formal axiomatic method defended recently by Hintikka is not self-sustained but requires a support of  constructive method. Finally I provide an epistemological argument showing that the constructive axiomatic method is more apt to present scientific theories than the received axiomatic method.


S.N. Artemov. Kolmogorov and gödel’s approach to intuitionistic logic: Current developments. Russian Mathematical Surveys, 59(2):203–229, 2004.

S. Awodey. Natural models of homotopy type theory. arXiv:1406.3219, 2014.

F. Cardone and J.R. Hindley. History of lambda-calculus and combinatory logic. D.R. Gabbay and J. Woods (eds.) Handbook of the History of Logic, 5:723–817, 2009.

J. Cavaillès. Méthode axiomatique et formalisme - Essai sur le problème du fondement des mathématiques. Paris, Hermann, 1938.

S.S. Demidov. On axiomatic and genetic construction of mathematical theories. J. Hintikka et al. (eds.) Theory Change, Ancient Axiomatics and Galileo’s Methodology. Proceedings of the 1978 Pisa Conference on the History

and Philosophy of Science (Synthese Library vol. 145), Reidel Publishing Company, 1:215–222, 1981.

Euclid. Elements. English translation by Richard Fitzpatrick. lulu.com, 2011.

J. Fantl. Knowledge How. The Stanford Encyclopedia of Philosophy (Spring 2014 Edition), Edward N. Zalta (ed.), 2012.

M. Hallett and U. Majer (eds.). David Hilbert’s Lectures on the Foundations of Geometry, 1891-1902, vol. 1. Springer, 2004.

D. Hilbert. Grundlagen der Geometrie. Leipzig, 1899.

D. Hilbert. Ueber den zahlbegriff. Jajresbericht der DMV, 8:180–194, 1900.

D. Hilbert. On the concept of number. W. Ewald (ed.), From Kant to Hilbert: A Source Book in the Foundations of Mathematics, 2:1089–1096, 1996.

D. Hilbert and P. Bernays. Grundlagen der Mathematik (in two volumes). Springer, 1934-1939.

D. Hilbert and P. Bernays. Foundations of Mathematics 1 (eds. C.-P. Wirth, J. Siekman, M. Gabbay, D. Gabbay). College Publications (UK), 2010.

J. Hintikka. What is axiomatic method? Synthese, 183(1):69–85, 2011.

A.N. Kolmogorov. On the interpretation of intuitionistic logic. V.M. Tikhomirov (ed.) Selected Works of A.N. Kolmogorov, Springer (original publication in German: Zur Deutung der Intuitionistischen Logik. Math. Ztschr.,

, S. 58-65 (1932)), 1:151–158, 1991.

A.N. Kolmogorov. On the papers on intuitionistic logic. V.M. Tikhomirov (ed.) Selected Works of A.N. Kolmogorov, Springer, 1:451–452, 1991.

E. Landry. The genetic versus the axiomatic method: Responding to Feferman 1977. The Review of Symbolic Logic, 6(1):24–51, 2013.

F.W. Lawvere. An elementary theory of the category of sets. Proc. Nat. Acad. Sci. U.S.A., 52:1506 – 1511, 1964.

F.W. Lawvere. Diagonal arguments and cartesian closed categories. P. J. Hilton, editor, Category Theory, Homology Theory and their Applications II, (volume 92 of Lecture Notes in Mathematics), Springer, 2:134 – 145, 1969.

F.W. Lawvere. Quantifiers and sheaves. M. Berger, J. Dieudonne et al. (eds.), Actes du congres international des mathematiciens, Nice, pages 329 – 334, 1970.

F.W. Lawvere. Functorial semantics of algebraic theories and some algebraic problems in the context of functorial semantics of algebraic theories (reprint with the author’s comments). Reprints in Theory and Applications

of Categories, 5:1–121, 2004.

F.W. Lawvere. An elementary theory of the category of sets (long version) with the author’s commentary. Reprints in Theory and Applications of Categories, 11:1– 35, 2005.

F.W. Lawvere. Adjointness in foundations with the author’s commentary. Reprints in Theory and Applications of Categories, 16:1–16, 2006.

J. Lmbek and P.J. Scott. Higher Order Categorical Logic. Cambridge University Press, 1986.

S. MacLane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer, 1992.

K. Manders. The euclidean diagram. Mancosu, P., The Philosophy of Mathematical Practice, Oxford University Press 2008, pages 80–133, 1995.

K. Manders. Diagram-based geometric practice. Mancosu, P., The Philosophy of Mathematical Practice, Oxford University Press 2008, pages 65–79, 2008.

J.-P. Marquis. From a Geometrical Point of View: A Study of the History and Philosophy of Category Theory (Series: Logic, Epistemology, and the Unity of Science, vol. 14 ). Springer, 2009.

J.-P. Marquis. Mathematical forms and forms of mathematics: leaving the shores of extensional mathematics. Synthese, 190(12):2141–2164, 2013.

P. Martin-Löf. Intuitionistic Type Theory (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli: BIBLIOPOLIS, 1984.

C. McLarty. Elementary Categories, Elementary Toposes. Oxford: Clarendon Press, 1992.

C. McLarty. Two constructivist aspects of category theory. Philosophia Scientiae, Cahier spécial, 6:95–114, 2006.

M. Panza. The twofold role of diagrams in euclidŠs plane geometry. Synthese, 1(186):55–102, 2012.

J. Piaget. Méthode axiomatique et méthode operationnelle. Synthese, 10(1):23–43, 1956.

A.-V. Pietarinen and G. Sandu. If logic, game-theoretical semantics, and the philosophy of science. S. Rahman, J. Symons, D. Gabbay and J.P. van Bendegem (eds.) Logic, Epistemology, and the Unity of Science, Springer, 1:105–

, 2004.

Proclus. Procli Diadochi in Primum Euclidis Elementorum Librum Commentarii ex recognitioni Godofredi Friedlein. Princeton Univ Press, 1873.

Proclus. A commentary on the first book of Euclid’s elements. Translated by G. R. Morrow. Teubner, Leipzig, 1970.

Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (Princeton); available

at http://homotopytypetheory.org/book/, 2013.

W.O. Quine. From a Logical Point of View. Harvard Univ. Press., 1953.

M. Rathjen. Constructive hilbert program and the limits of Martin-Löf’s Type theory. Synthese, 147(1):81–120, 1960.

A. Rodin. Axiomatic Method and Category Theory (Synthese Library vol. 364). Springer, 2014.

D. Schlimm. Axiomatics and progress in the light of 20th century philosophy of science and mathematics. B. Löwe, V. Peckhaus and T. Räsch (eds.), Foundations of the Formal Sciences IV The History of the Concept of the Formal Sciences. Papers of the conference held in Bonn, February 14-17, 2003. Studies in Logic Series, College Publications, London, pages 233–253, 2006.

D. Schlimm. Axioms in mathematical practice. Philosophia Mathematica, 21(1):37–92, 2013.

U. Schreiber. Quantization via Linear homotopy types. arXiv: 1402.7041, 2014.

U. Schreiber and M. Shulman. Quantum Gauge Field Theory in Cohesive Homotopy Type Theory. arXiv:1408.0054, 2014.

J.P. Seldin. The logic of church and curry. D.R. Gabbay and J. Woods (eds.) Handbook of the History of Logic, 5:819–894, 2009.

V.A. Smirnov. Genetic method for scientific theory construction. Philosophical Problems of Contemporary Formal Logic, Moscow, Nauka (in Russian), pp. 263–284, 1962.

M.H. Sorensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism, (Studies in Logic and the Foundations of Mathematics vol. 149). Elsevier, 2006.

A. Szabo. Beginnings of Greek Mathematics. Reidel Publishing Company, 1978.

A. Tarski. Sentential calculus and topology. Logic, Semantics, Metamathematics: Papers from 1923 to 1938 translated by J.H. Woodger; Oxford at Clarendon Press, pages 421–454, 1956.

B.C. van Fraassen. The Scientific Image. OUP, 1980.

V. Voevodsky. Univalent foundations. Mathematisches Forschungsinstitut Oberwolfach, Mini-Workshop: The Homotopy Interpretation of Constructive

Type Theory, Report N 11/2011, pages 7–10, 2011.

S. Yablo. Aboutness. Princeton University Press, 2014.


  • There are currently no refbacks.