andrei rodin Andrei Rodin's blog about History and Philosophy of Mathematics

Homotopy Type Theory in Logic, Metaphysics and Philosophy of Physics

University of Bristol; September 13-15th, 2016.

Chers collègues,

Nous avons le plaisir de vous annoncer deux séances supplémentaires du GDT « Mathématiques XIXe-XXe, Histoire et Philosophie » :

*Andrei Rodin* (Institute of Philosophy of the Russian Academy of Sciences), chercheur invité à SPHERE, donnera deux conférences sur le thème
« Axiomatic Method between Logic and Geometry » :

1. *Lundi 23 mai, de 10h à 13h, en salle Klein (371A)* :   « Axiomatic Geometry according to Euclid and according to Hilbert. »

2. *Lundi 6 juin, de 10h à 13h, en salle Rothko (412B)* :
« Logic and Geometry in Topos theory and in Homotopy Type theory »

à l’Université Paris 7 Diderot, bâtiment Condorcet (4 rue Elsa Morante, 75013 Paris).

Voici un résumé et quelques éléments de bibliographie.

The modern notion of axiomatic theory derives from Hilbert’s /Grundlagen der Geometrie/ of 1899. It essentially differs from the more traditional idea of axiomatic theory presented in Euclid’s Elements. More surprisingly, Hilbert’s account of axiomatic thinking does not seem to do full justice to some recent axiomatic theories such as the axiomatic Topos theory due to Lawvere and Homotopy Type theory due to Voevodsky and his collaborators. In this series of two talks I provide a historical perspective on the axiomatic method and on this basis develop an up-to-date concept of axiomatic theory, which I suggest to call *constructive*. The constructive axiomatic method, which is best represented today by Homotopy Type theory, is conceptually rooted in Euclid’s mathematics, geometric works by Grassmann and Peano in the 19th century, and Kolmogorov’s approach in constructive mathematics.

Talk 1: Axiomatic Geometry according to Euclid and according to Hilbert.

Bibliography:

H. Freudental, The main trends in the foundations of geometry in the 19th century, in: Logic, Methodology and Philosophy of Science: Proceedings of the 1960 International Congress. Standford University Press 1962, pp. 613-621.

A.N. Kolmogorov, On the Interpretation of Intuitionistic Logic, in: V.M.  Tikhomirov (ed.) Selected Works of A.N. Kolmogorov, Springer 1991, pp.  151-158 (Original publication in German: Zur Deutung der Intuitionistischen Logik. Math. Ztschr., 35  (1932), S. 58-65)

I. Mueller, Greek Mathematics and Greek Logic, in: Ancient Logic and Its Modern Interpretations (Synthese Historical Library vol.9), Reidel
Publishing 1974, pp. 35-70

A. Rodin, Axiomatic Method and Category Theory (Synthese Library vol. 364), Springer 2014,  Chapters 2-4.

Talk 2: Logic and Geometry in Topos theory and in Homotopy Type theory.

Bibliography:

F.W. Lawvere, Quantifiers and sheaves, in: M. Berger, J. Dieudonne et al.  (eds.), Actes du congres international des mathématiciens, Nice 1970, pp.  329 – 334

C. McLarty, Elementary Categories, Elementary Toposes, Oxford: Clarendon Press 1992, Chapters 13-18

Andrei Rodin, Axiomatic Method and Category Theory (Synthese Library vol.  364), Springer 2014. Chapters 5, 7, 10

Andrei Rodin, On Constructive Axiomatic Method, arXiv:1408.3591, to appear in Logique et Analyse

Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study (Princeton) 2013; available at http://homotopytypetheory.org/book/}, Chapters 1-3

En espérant vous retrouver nombreux,

Cordialement,

Les organisateurs.

NEW: full paper

Cher(è)s collègues,

Vous êtes cordialement invité(e)s à la prochaine séance du séminaire de recherche L’(id)entité :: L’(id)entification, laquelle se tiendra le jeudi 26 mai de 15h à 17h dans la salle 646A-Mondrian de l’Université Paris Diderot (Bâtiment Condorcet, 4 Rue Elsa Morante, 75013). Pour cette séance, nous aurons le plaisir d’accueillir Andrei Rodin (Institute of Philosophy, Russian Academy of Science – Saint-Petersburg State University), qui fera l’exposé suivant:

Venus Homotopically

The identity concept developed in the Homotopy Type Theory (HoTT) 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 Classical Mechanics) and discuss its relevance in Quantum Mechanics.

NB: en raison des procédures actuellement en vigueur dans le cadre du plan Vigipirate, nous vous prions de répondre à ce message si vous comptez venir afin de vous inscrire dans la liste correspondante.

Bien cordialement,
Gabriel Catren
Laboratoire SPHERE – Sciences, Philosophie et Histoire (UMR 7219)
CNRS – Université Paris Diderot

Логические и эпистемологические аспекты конструктивного знания

Описание: Мы называем знание конструктивным, если это знание включает в себя явно выраженную спецификацию по крайней мере некоторых эпистемических процедур, таких как получение, верификация, представление, распространение, ревизия и применение данного знания. Цель настоящего воркшопа состоит в том, чтобы обсудить логические и эпистемологические подходы к конструктивному знанию в контексте современных информационных технологий.  Данный воркошоп приурочен к началу одноименного исследовательского проекта, поддрежанного Российским гуманитарным научным фондом.

когда: понедельник 25 апреля 2016 года
где: Институт Философии РАН ), комната 416, 4-й этаж.  Адрес: Москва, Гончарная ул. 12, строение 1. Проезд: станция метро Таганская Кольцевой линии
Программа: (копия программы с аннотациями и презентациями докладов здесь)
10:00 – 10:15
Андрей Родин (ИФ РАН): О проекте (вступительное слово)

10:15 – 11:00
Сергей Ковалев (ИПУ РАН): Машинный интеллект в инженерии аксиоматических систем

11:00-11:45 Евгений Бениаминов (РГГУ) Категорный подход к представлению знаний в проекте разработки сервера библиотек онтологий ЭЗОП

11:45 – 12:00 Кофе

12:00-12:45
Валентин Голев (СПбГУ) Жан-Ив Жирар и поиск имманентного в логике

12:45-13:30
Даниил Рогозин (ГАУГН) Теория типов и формализация математических доказательств

13:30-15:00 Обед

15:00-16:00
Константин Шишов (МГУ) Системы квантовых логик  в конструктивном знании

16:00-16:45
Андрей Родин (ИФ РАН): Модельное знание и его аксиоматическое представление

16:45-17:15
Заключительная дискуссия

Model-Based Knowledge and Its Representation.  (slides)(announcement)

What is a Formal System? The Idea of Geometrical Characteristics from Leibniz to Voevodsky.  (slides)

Философия науки и техники в России: концепция и дисциплина. Учредительная Конференция Русского Общества Истории и Философии Науки  (Москва, МГУ 25-26 марта 2016 года)

7-es Rencontres Français de Philosophie des Mathematiques, Paris 5-7 Nov (program)

New Spaces in Mathematics and Physics: Formal and Philosophical Reflections , Paris, 28 Sent – 2 Oct 2015 (program)

UPDATES:

- Book of abstracts (pdf)

-  Youtube stream records are now available (see separate links for the first and the second day in the Program below)

-  Materials of the talks (slides and in once case a paper) are available (also in the below Program).

Where: Institute of Philosophy, Russian Academy of Sciences. Moscow, Volkhonka 14, build. 5

When: 21-23 September 2015

Title: New mathematical methods in today’s physics: logical, epistemological and computational aspects

Where: Institute of Philosophy, Russian Academy of Sciences. Moscow, Volkhonka 14, build. 5

When: 21-23 September 2015

Aim and Scope

Over the last few decades there were a number of important attempts to apply the new 20-th century mathematics in physics. Mathematics in its turn borrowed from physics many important ideas and motivations. During the planned Conference these developments will be discussed and scrutinized from various viewpoints including logical, epistemological and historical ones.
The Conference will bring together physicists, mathematicians and philosophers working on mathematical foundations of physics. We aim, in partiular, at developing a new theoretical and pragmatic perspective on the famous problem of “unreasonable effectiveness of mathematics in the natural sciences” stressed by E. Wigner back in 1960. We hope that this event will help to strengthen conceptual ties between mathematics and logic, on the one hand, and physics and other natural sciences, on the other hand. The Conference is designed as the concluding event of 3-year long research project “Epistemological strategies of application of mathematics in natural sciences” funded by RFBR (grant N 13-06-00515), which will allow the participants of this project to share their results and exchange their ideas with an international scientific community and establish a new horizon for their further researches. Proceedings of the Conference will be published in 2016 (through “Proceedings of Science” or another similar tool).

Program:

Monday 21st September ( stream record)

09:00 – 09:15 : Opening words

09:15 – 10:45 :  Vladislav Terechovich (SPB)  Explanatory Potential of Mathematics in Quantum Physics (abstract)(slides)
10:45 – 11:15 : Coffee Break

11:15 – 12:30  : Mark Lachieze-Rey (University Paris-Diderot)  Which mathematics for quantum gravity ? (abstract)(slides)

12:30 – 14:00 : Lunch

14:00 – 15:30 : A.D. Panov (Skobeltsyn Institute of Nuclear Physics). Bell’s theorem, computability of quantum theory, and relativity of the ‘local realism’ (abstract)(slides)

15:30 – 16:00 : Coffee Break

16:00 – 17:30 :  Andrei Rodin (Institute of Philosophy RAS)

Constructive Axiomatic Method and Modern Physics (abstract)(slides)

Tuesday 22nd September (stream record)

09:15 – 10:45 : Sergei Kovalyov (Institute of Control Science RAS) Computational Fracture Mechanics: Towards Multi-* Analysis (abstract)(slides)

10:45 – 11:15 : Coffee Break

11:15 – 12:30: Jairo da Silva (University of São Paulo) Structuralism and the Applicability of Mathematics in Physics (abstract)(paper)

12:30 – 14:00 : Lunch

14:00 – 15:30 : Alexander Pechenkin (MSU) Foundations of Physics and Phenomenological Reduction (abstract)(slides)

15:30 – 16:00 : Coffee Break

16:00 – 18:00 : Round Table discussion

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

Slides   (NEW!)

Abstract:
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.

Bibliography:

[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).