Upcoming Talk at the 15th Congress on Logic, Methodology, and Philosophy of Science (Helsinki, 3-8 August 2015)
Title: Constructive Axiomatic Method in Euclid, Hilbert and Voevodsky
The standard version of formal axiomatic method stemming from Hilbert [Hilbert (1899)] and recently defended by Hintikka [Hintikka (2011)] is not fully adequate to the recent successful practice of axiomatizing mathematical theories. In particular, the axiomatic architecture of Homotopy Type theory (HoTT) [Voevodsky et. al. 2013] does not quite fit the standard Hilbertian pattern of axiomatic theory. At the same time HoTT and some other recent theories fall under a more general and in some respects more traditional notion of axiomatic theory, which I call after Hilbert and Bernays [Hilbert&Bernays (1934-1939)] “genetic” or “constructive” (interchangeably) and demonstrate it using the Classical example of the First Book of Euclid’s “Elements”. On the basis of these modern and ancient examples I claim that Hintikka’s semantic-oriented formal axiomatic method is not self-sustained but requires a support of some more basic constructive method. I provide an independent epistemological grounding for this claim by showing the need to complement Hintikka’s account of axiomatic method with a constructive notion of formal semantics.
[Euclides(1883-1886)] Euclides (1883-1886) Heiberg (ed.) Euclidis Opera Omnia, Lipsiae, v. 1.
[Hilbert(1899)]: Hilbert D. (1899), Grundlagen der Geometrie, Leipzig.
[Hilbert&Bernays(1934-1939)]: Hilbert D. and Bernays P. (1934-1939), Grundlagen der Mathematik (in two volumes), Springer.
[Hintikka(2011)]: Hintikka J (2011) What is axiomatic method?, Synthese 183(1):69–85.
[Voevodsky et al. (2013)] Voevodsky V. et al. (2013), Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study (Princeton).