On the Constructive Axiomatic Method

Logique et Analyse. 2018. Vol. 242. No. 2. P. 201–231.

Rodin A.

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 ft 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 axi omatic method is more apt to present scientifc theories than the received axiomatic method.

Keywords: теория типов, axiomatic method, Homotopy Type theory, аксиоматический метод

Publication based on the results of: Формальная эпистемология, логика и прагматика агентности в рациональных интеракция (2018)