What is Constructive Axiomatic Method?
Institute of Philosophy of Russian Academy of Sciences; Smolny College of Liberal Arts and Sciences, Saint-Petersburg State University
The received notion of axiomatic theory, which stems from Hilbert, is that of set T of propositions (either contentful or non-interpreted aka propositional forms) with subset A of axioms provided with a notion of consequence, which generates T from A in the obvious way. I argue that this standard notion is too narrow for being an adequate theoretical model of many mathematical theories; the class of such counter-examples is apparently very large and it includes such different theories as the geometrical theory of Euclid’s Elements, Book 1, and the more recent Homotopy type theory. In order to fix this problem I introduce a more general notion of theory, which uses typing and a generalized notion of consequence applicable also to objects of other types than propositions. I call such a theory constructive axiomatic theory and show that this particular conception of being constructive indeed captures many important ideas concerning the mathematical constructivity found in the earlier literature from Hilbert to Kolmogorov to Martin-Lof. Finally I provide an epistemological argument intended to show that the notion of constructive axiomatic theory is more apt to be useful in natural sciences and other empirical contexts than the standard notion. Disclaimer: The notion of constructive axiomatic theory is not my invention. The idea and its technical implementation are found in Martin-Lof ‘s constructive type theory if not already in Euclid. My aim is to make this notion explicit and introduce it into the continuing discussions on axiomatic method and mathematical and logical constructivity.
Andrei Rodin has research interests in history and philosophy of mathematics and science. He got his Ph.D. in Philosophy of Science (Ph.D. Title: “First Four Books of Euclid’s Elements in the Context of Plato’s and Aristotle’s Philosophy”) from Institute of Philosophy of Russian Academy of Sciences in 1995. He is currently affiliated with this Institute as a senior researcher, a member of Philosophy of Science group, organizer of a regular seminar on Philosophy of Sciences and Technology. He had visiting positions at ENS (Paris), University Paris-Diderot and Columbia University. He is the author of two monographs: “Axiomatic Method and Category Theory,” Synthese Library, vol. 364, Springer 2014 and “Euclid’s Mathematics in Context of Plato’s and Aristotle’s Philosophy,” Moscow, Nauka, 2003.