?
Constructive Axiomatic Method in Euclid, Hilbert and Voevodsky
The version of 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 formal 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.