Séminaire de Logiques Non Classiques : Andrey Rodin
"Constructive Axiomatic Method"
Hilbert and Bernays describe their formal axiomatic method by distinguishing it from the more traditional genetic aka constructive axiomatic method used by Euclid, Newton and Clausius. I consider a modern version of the constructive method based on the Curry-Howard correspondence and argue that this method of theory-building plays a role in today's mathematics. I illustrate this thesis by examples from Topos theory and Homotopy Type theory. In this context I discuss a possible epistemic role of logic in mathematics and natural sciences.