Andrei Rodin

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 fit 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 axiomatic method is more apt to present scientific theories than the received axiomatic method. © 2018 Elsevier B.V., All rights reserved.

Kolmogorov's Calculus of Problems is an interpretation of Heyting's intuitionistic propositional calculus published by A.N. Kolmogorov in 1932. Unlike Heyting's intended interpretation of this calculus, Kolmogorov's interpretation does not comply with the philosophical principles of Mathematical Intuitionism. This philosophical difference between Kolmogorov and Heyting implies different treatments of problems and propositions: while in Heyting's view, the difference between problems and propositions is merely linguistic, Kolmogorov keeps the two concepts apart and does not apply his calculus to propositions. In this paper the differences between Kolmogorov's and Heyting's interpretations are stressed, and it is shown how the two interpretations have diverged during their development. The impact of Kolmogorov's philosophical views on mathematics on his interpretation of the Intuitionistic logic is shown. Some later works motivated by Kolmogorov's Calculus of Problems are reviewed. Finally, Kolmogorov's controversial distinction between problems and propositions is given a modern justification in terms of Univalent Mathematics.

In this paper we present novel conceptions of identity arising in and motivated by a recently emerged branch of mathematical logic, namely, Homotopy Type theory (HoTT). We consider an established 2013 version of HoTT as well as its more recent generalised version called Directed HoTT or Directed Type theory (DTT), which at the time of writing remains a work in progress. In HoTT, and in particular in DTT, identity is not just a relation but a mathematical structure which admits for an interpretation in terms of Homotopy theory (directed Homotopy theory in the case of DTT), which in its turn is supported by common intuitions concerning identity of material objects through time, change and locomotion. The DDTbased conception of identity presented in the paper is nonsymmetric: here identity is “directed” or has a “sense”. We compare the HoTT-based conceptions of identity with standard theories of identity based on the Classical Predicate calculus, and show how the HoTT-based identity helps to treat traditional logical and philosophical problems related to identity and time. In the concluding part of the paper we explore some ontological implications of the HoTT-based identity and show how HoTT and DTT can serve for designing formal process ontologies. The paper is self-contained and comprises expositions and informal explanations of all relevant philosophical, logical and mathematical contents.

The received Hilbert-style axiomatic foundations of mathematics has been designed by Hilbert and his followers as a tool for metatheoretical research. Foundations of mathematics of this type fail to satisfactory perform more basic and more practically oriented functions of theoretical foundations such as verification of mathematical constructions and proofs. Using alternative foundations of mathematics such as the univalent foundations is compatible with using the received set-theoretic foundations for metamathematical purposes provided the two foundations are mutually interpretable. Changes in foundations of mathematics do not, generally, disqualify mathematical theories based on older foundations but allow for reconstruction of these theories on new foundations. Mathematics is one but its foundations are many.

This volume explores the many different meanings of the notion of the axiomatic method, offering an insightful historical and philosophical discussion about how these notions changed over the millennia. The author, a well-known philosopher and historian of mathematics, first examines Euclid, who is considered the father of the axiomatic method, before moving onto Hilbert and Lawvere. He then presents a deep textual analysis of each writer and describes how their ideas are different and even how their ideas progressed over time. Next, the book explores category theory and details how it has revolutionized the notion of the axiomatic method. It considers the question of identity/equality in mathematics as well as examines the received theories of mathematical structuralism. In the end, Rodin presents a hypothetical New Axiomatic Method, which establishes closer relationships between mathematics and physics. Lawvere's axiomatization of topos theory and Voevodsky's axiomatization of higher homotopy theory exemplify a new way of axiomatic theory building, which goes beyond the classical Hilbert-style Axiomatic Method. The new notion of Axiomatic Method that emerges in categorical logic opens new possibilities for using this method in physics and other natural sciences. This volume offers readers a coherent look at the past, present and anticipated future of the Axiomatic Method.

Ranta’s view that all substitutions of variables between MLTT contexts in some sense “extend” these contexts, so the MLTT contexts always form a partial order, is not justified. It is well known that the category of MLTT contexts is, generally, locally Cartesian closed but not necessarily a poset. Thus, Domanov’s reading of such general substitutions as mutual interpretations between contexts, which represent their corresponding epistemic agents, is more adequate. The formal analysis offered by Domanov can be improved if this latter viewpoint is developed more systematically than the author does it in his paper.

The identity concept developed in the Homotopy Type theory supports an analysis of Frege's famous Venus example, which explains how empirical evidences justify judgements about identities. In the context of this analysis we consider the traditional distinction between the extension and the intension of concepts as it appears in HoTT, discuss an ontological significance of this distinction and, finally, provide a homotopical reconstruction of a basic kinematic scheme, which is used in the Classical Mechanics, and discuss its relevance in the Quantum Mechanics.

In his seminal address delivered in 1945 to the Royal Society Gilbert Ryle considers a special case of knowing-how, viz., knowing how to reason according to logical rules. He argues that knowing how to use logical rules cannot be reduced to a propositional knowledge. We evaluate this argument in the context of two different types of formal systems capable to represent knowledge and support logical reasoning: Hilbert-style systems, which mainly rely on axioms, and Gentzen-style systems, which mainly rely on rules. We build a canonical syntactic translation between appropriate classes of such systems and demonstrate the crucial role of Deduction Theorem in this construction. This analysis suggests that one's knowledge of axioms and one's knowledge of rules under appropriate conditions are also mutually translatable. However our further analysis shows that the epistemic status of logical knowing-how ultimately depends on one's conception of logical consequence: if one construes the logical consequence after Tarski in model-theoretic terms then the reduction of knowing-how to knowing-that is in a certain sense possible but if one thinks about the logical consequence after Prawitz in proof-theoretic terms then the logical knowledge-how gets an independent status. Finally we extend our analysis to the case of extra-logical knowledge-how representable with Gentzen-style formal systems, which admit constructive meaning explanations. For this end we build a typed sequential calculus and prove for it a ``constructive'' Deduction Theorem interpretable in extra-logical terms. We conclude with a number of open questions, which concern translations between knowledge-how and knowledge-that in this more general semantic setting.

This is the first part of a work in progress, which contains Introduction, explaining the whole project, and a chapter on Euclid's "Elements". The idea of the book is to describe foundations in mathematics in their history from Euclid until today (making a reasonable choice of material) and then provide a project of future foundations of mathematics. Further historical parts of the book will contain chapters on "New Elements of Geometry" by Arnauld (first published in 1667), Hilbert's "Grundlagen der Geometrie" first published in 1899 and Bourbaki's "Elements of Mathematics". The part of the book describing prospective future foundations of mathematics will be on Category theory.

Renewing Foundations-1 This is the first part of a work in progress, which contains Introduction, explaining the whole project, and a chapter on Euclid's "Elements". The idea of the book is to describe foundations in mathematics in their history from Euclid until today and then provide a project of future foundations of mathematics. Further historical parts of the book will contain chapters on "New Elements of Geometry" by Arnauld, Hilbert's "Grundlagen der Geometrie" first published in 1899 and Bourbaki's "Elements of Mathematics". The part of the book describing prospective future foundations of mathematics will be on Category theory.

The formal axiomatic method popularized by Hilbert and recently defended by Hintikka is not fully adequate to the recent practice of axiomatizing mathematical theories. The axiomatic architecture of Topos theory and Homotopy type theory do not fit the pattern of the formal axiomatic theory in the standard sense of the word. However these theories fall under a more general and in some respects more traditional notion of axiomatic theory, which I call after Hilbert constructive. I show that the formal axiomatic method always requires a support of some more basic constructive method.

In this paper I consider the standard approach to identity in mathematics originating from Frege’s and Russell’s works and contrast it with alternative approaches due to Plato and Geach. Then I put the problem in a category-theoretic setting and show that the notion of identity cannot be “internalized” with usual categorical means. Finally I present two more specific mathematical approaches to the identity problem: one based on a categorical fibration and the other involving weak higher categories.

Formal Axiomatic method as exemplified in Hilbert’s Grundlagen der Geometrie is based on a structuralist vision of mathematics and science according to which theories and objects of these theories are to be construed “up to isomorphism”. This structuralist approach is tightly linked with the idea of making Set theory into foundations of mathematics. Category theory suggests a generalisation of Formal Axiomatic method, which amounts to construing objects and theories “up to general morphism” rather than up to isomorphism. It is shown that this category-theoretic method of theorybuilding better fits mathematical and scientific practice. Moreover so since the requirement of being determined up to isomorphism (i.e. categoricity in the usual model-theoretic sense) turns to be unrealistic in many important cases. The category-theoretic approach advocated in this paper suggests an essential revision of the structuralist philosophy of mathematics and science. It is argued that a category should be viewed as a far-reaching generalisation of the notion of structure rather than a particular kind of structure. Finally, I compare formalisation and categorification as two alternative epistemic strategies.

I consider how the notion of event is used in such important branches of twentieth-century thought as relativity, quantum mechanics, Marxist sociology and psychoanalysis. I show that in each case there is the same concept of event as of a series of communications. It is also shown that this new concept of event corresponds to traditional concepts of historical events. I analyze the difference between the concept of event and that of fact. Since a fact presupposes "an external observer" it is impossible to deal with an event without being involved in it. Since a fact presupposes its permanent logical form as a necessary condition of knowledge about it, any condition of knowledge about an event appears to be empirical itself. I show that the division between history and prehistory has the same basis as that between event and fact. The crucial question is how knowledge about an event is possible. The problem is that the concept of identity applicable to fact appears to be inapplicable to event. However, it appears possible to define an identity of event with an identity of media or "places" of communication. An open system of such "places" we call "milieu." A language is a paradigm for it. However, I suppose that unlike "the linguistic paradigm," the "paradigm of milieu" should refute the idea of the exceptional status of human language.

When the traditional distinction between a mathematical concept and a mathematical intuition is tested against examples taken from the real history of mathematics one can observe the following interesting phenomena. First, there are multiple examples where concepts and intuitions do not well fit together; some of these examples can be described as “poorly conceptualised intuitions” while some others can be described as “poorly intuited concepts”. Second, the historical development of mathematics involves two kinds of corresponding processes: poorly conceptualised intuitions are further conceptualised while poorly intuited concepts are further intuited. In this paper I study this latter process in mathematics during the twentieth century and, more specifically, show the role of set theory and category theory in this process. I use this material for defending the following claims: (1) mathematical intuitions are subject to historical development just like mathematical concepts; (2) mathematical intuitions continue to play their traditional role in today's mathematics and will plausibly do so in the foreseeable future. This second claim implies that the popular view, according to which modern mathematical concepts, unlike their more traditional predecessors, cannot be directly intuited, is not justified.

In 1900 David Hilbert announced his famous list of then-opened mathematical problems; the problem number 6 in this list is axiomatization of physical theories. Since then a lot of systematic efforts have been invested into solving this problem. However the results of these efforts turned to be less successful than the early enthusiasts of axiomatic method expected. The existing axiomatizations of physical and biological theories provide a valuable logical analysis of these theories but they do not constitute anything like their standard presentation,which can be used for transmission, evaluation, and justification of physical and biological knowledge. This state of theart in the axiomatization of physics is strong evidence that the standard notion of axiomatic theory stemming from Hilbert and Tarski is not appropriate for thet ask. However in the recent years in mathematics there emerged a new axiomatic approach best represented by the Homotopy Type theory (HoTT). We argue that the constructive axiomatic architecture used in HoTT has better chances to be successfully applied in physics as well as in computer science and engineering.

I elaborate in some detail on the First Book of Euclid's ``Elements'' and show that Euclid's theory of geometry is \underline{not} axiomatic in the modern sense but is construed differently. Then I show that the usual commonly accepted notion of axiomatic theory equally fails to account for today's mathematical theories. I provide some polemical arguments against the popular view according to which a good mathematical theory must be axiomatic and point to an alternative method of theory-building. Since my critique of the core axiomatic method is constructive in its character I briefly observe known constructive approaches in the foundations of mathematics and describe the place of my proposal in this context. The main difference of my and earlier constructive proposals for foundations of mathematics appears to be the following: while earlier proposals deal with the issue of admissibility of some particular mathematical principles and like choice and some putative mathematical objects like infinite sets my proposal concerns the very method of theory-building. As a consequence, my proposal unlike earlier constructive proposals puts no restriction on the existing mathematical practice but rather suggests an alternative method of organizing this practice into a systematic theoretical form. In the concluding section of the paper I argue that the constructive mathematics better serves needs of mathematically-laden empirical sciences than the formalized mathematics.

This article asks whether a country that suffers from serious environmental problems caused by another country could have a just cause for a defensive war? Danish philosopher Kasper Lippert-Rasmussen has argued that under certain conditions extreme poverty may give a just cause for a country to defensive war, if that poverty is caused by other countries. This raises the question whether the victims of environmental damages could also have a similar right to self-defense. Although the article concerns justice of war, we will concentrate only on the issue of what can be just causes of war, instead of evaluating the entire justification of war. This is to say that we will limit our discussion to the question concerning just cause and leave aside more general questions concerning justness and moral permissibility of war. Our aim is to list the questions that must be made and settled if defensive war in the case of serious environmental problems is said to have (or not to have) a just cause. We will argue that there are three questions that are most important in this context. They are the question concerning liability, the question of collective responsibility, and the question whether environmental harms may create a “sufficient reason” for raising a war.

Lobachevsky's Imaginary geometry in its original form involved an extension of rather than a radical departure from Euclidean intuition. It wasn't anything like a formal theory in Hilbert's sense and hence didn't require anything like a model. However, rather surprisingly, Lobachevsky uses what in modern terms can be called a non-standard model of Euclidean plane, namely as a specific surface (a horisphere) in a Hyperbolic space. In this paper I critically review some popular accounts of the discovery of Non-Euclidean geometries and suggest a revision of the epistemic view on the issue dating back to Hilbert's Grundlagen.