Formalism, Formalization, Intuition and Understanding in Mathematics: <br />From Informal Practice to Formal Systems and Back Again
This project investigates the interplay between informal mathematical theories and their formalization. Reflecting on the interplay between informal mathematical theories and their formalization means reflecting on mathematical practice and on what makes it rigorous, and how this dynamism generates different forms of understanding. We therefore aim to investigate the connection between different levels of understanding and the notion of rigor in mathematics. <br />In investigating these forms of mathematical understanding, the project will draw on philosophical and logical analyses of case studies from the history of mathematical practice, in order to construct a compelling new picture of the relationship of formalization to informal mathematical practice. The notion of formal rigor (in the proof theoretic sense) has been extensively investigated in philosophy and logic, though an account of the epistemic role of the process of formalization is currently missing. We argue that formal rigor is best understood as a dynamic abstraction from informally rigorous mathematical arguments. <br />One of the main consequences of this investigation will be to show that the process of acquiring mathematical understanding is far more complex than current philosophical views allow us to account for.
The main methodology of research for this project is philosophical reflection, carried out either individually or by means of common discussion (seminars, workshops, conferences). Philosophical reflection is combined with logical and historical analysis, in order to provide a philosophical account of the interplay between formalization and understanding that accounts for mathematical research as carried out in mathematical practice.
The philosophical and logical analysis of case studies from the history of mathematics is crucial to the project in two ways. Firstly, the history of mathematics provides illuminating case studies for illustrating the levels of understanding. Secondly, we also promote a way of looking at the history of formal disciplines as exemplifying the epistemological role that they play within ordinary mathematical practice. Mathematical logic is itself a mathematical discipline, and thus analogous to other such disciplines in having been born from a process of formalization of some aspects of mathematical practice.
The most significant event was undoubtedly the presentation of our project to the international community in the field at the 16th International Congress of Logic, Methodology and Philosophy of Science and Technology held in Prague in August 2019. The symposium, organized by our post-doc of the project, Maté Szabo, was attended by a very large audience and generated interest that was expressed through cooperation intentions.
Two examples of promising scientific advances discussed widely in the French team:
First question: Does it make sense to speak in pure mathematics of thought experiments?
Answer: in the dynamic hierarchy of formalisms, the proof- and construction-instances of level n-1can be considered as realizations of mathematical experiments with respect to “rigorous” proofs and constructions of level n. In mathematical thought experiments, we make an additional hypothesis about epistemic possibilities based on mathematical experiments using the iconic (intuitive) function of exemplification.
2nd Question: What does a certain informal theory make formal? What makes that a formal theory is the interpretation of an informal theory?
Answer: The introduction of new expressive means implies a form of recasting an old corpus of theory and this allows mathematicians to focus on the same characteristics of the content of such a mathematical corpus, and to make it essential in the context of the new theory involving these new expressive means. A form of mathematical understanding results if a given 'informal' mathematical theory is interpreted by a new theory, where it is only a form of recasting that provides understanding insofar as it improves the “control” on the relevant content.
A joint workshop with the ANR project PROGRAMme is planned for the month of December. The aim is to discuss possible collaborations between the two projects in terms of formalization of algorithms in mathematics and computer science, and of the relations between proofs and computer programs. One of two coordinators (MP) is completing a book (to be submitted to Springer Publishing, Synthese Library) whose writing has benefited enormously from internal discussions in the project. The book deals with the notion of epistemic economy, whose conception depends essentially on the vision of the relations between informal knowledge and formalization developed in the project. This will be one of the major results of the project.
Marianna Antonutti Marfori
• (2018) « Human Effective Computability” (with L. Horsten).?Philosophia Mathematica 27(1):61–87. DOI: doi.org/10.1093/philmat/nky011
• (2018), Introduction (avec M. Bourdeau et P. Wagner), Sur la philosophie scientifique et l’unité de la science. Le congrès de Paris 1935 et son héritage. Actes de Cerisy, Philosophia Scientiae 22 (3), 3-15.
• (with Andrea Sereni) “Frege’s Constraint and the Nature of Frege’s Foundational Program”, Review of Symbolic Logic, 12, 1, 2019, pp. 97-143.
• (2018) (avec Christophe Eckes), « The Classificatory Function of Diagrams : Two Examples from ?Mathematics », Lecture Notes in Computer Science 10871, 120 - 136.
• (Avec Abel Lassale Casanave) « Enthymemathical Proofs and Canonical Proofs in Euclid’s Plane Geometry », in H. Tahiri (Ed.) The Philosophers and Mathematics, Springer, Cham, 2018, ch. 7, pp. 127-144.
• « Was Frege a Logicist for Arithmetic? », in A. Coliva, P. Leonardi, S. Moruzzi (eds), Eva Picardi on Language, Analysis and History, Palgrave MacMillan, Springer Nature, Cham, Switzerland, 2018, pp. 87-112.
• (with Mirna Dzamonja) « Asymptotic quasi-completeness and ZFC », in W. Carnielli and J. Malinowski (eds.) Contradictions, from Consistency to Inconsistency, Springer Nature (Trends in Logic), Switzerland, 2018, pp. 159-182.
• (avec Marco Panza) Constructions and proofs in Euclid's geometry, Formalisation vs. Meaning in Mathematics: Formal theories as tools for understanding Themes from the work of Göran Sundholm, 13 juin, 2019
• (avec Pierre Cartier, Jean Dhombres, Cédric Villani),
Conversation sur les mathématiques, Paris :
Flammarion (Champs sciences), 2019.
This project investigates the interplay between informal mathematical theories and their formalization, and argues that this dynamism generates three different forms of understanding:
1. Different kinds of formalizations fix the boundaries and conceptual dependences between concepts in different ways, thus contributing to our understanding of the content of an informal mathematical theory. We argue that this form of understanding of an informal theory is achieved by recasting it as a formal theory, i.e. by transforming its expressive means.
2. Once a formal theory is available, it becomes an object of understanding. An essential contribution to this understanding is made by our recognition of the theory in question as a formalization of a particular corpus of informal mathematics. This form of understanding will be clarified by studying both singular intended models, and classes of models that reveal the underlying conceptual commonalities between objects in different areas of mathematics.
3. The third level concerns how the study of different formalizations of the same area of mathematics can lead to a transformation of the content of those areas, and a change in the geography of informal mathematics itself.
In investigating these forms of mathematical understanding, the project will draw on philosophical and logical analyses of case studies from the history of mathematical practice, in order to construct a compelling new picture of the relationship of formalization to informal mathematical practice. One of the main consequences of this investigation will be to show that the process of acquiring mathematical understanding is far more complex than current philosophical views allow us to account for.
While formalization is often thought to be negligible in terms of its impact on mathematical practice, we will defend the view that formalization is an epistemic tool, which not only enforces limits on the problems studied in the practice, but also produces new modes of reasoning that can augment the standard methods of proof in different areas of mathematics.
Reflecting on the interplay between informal mathematical theories and their formalization means reflecting on mathematical practice and on what makes it rigorous, and how this dynamism generates different forms of understanding. We therefore also aim to investigate the connection between the three levels of understanding described above, and the notion of rigor in mathematics. The notion of formal rigor (in the proof theoretic sense) has been extensively investigated in philosophy and logic, though an account of the epistemic role of the process of formalization is currently missing. We argue that formal rigor is best understood as a dynamic abstraction from informally rigorous mathematical arguments. Such informally rigorous arguments will be studied by critically analyzing case studies from different subfields of mathematics, in order to identify patterns of rigorous reasoning.
Monsieur Gerhard HEINZMANN (Laboratoire d'Histoire des Sciences et de Philosophie - Archives henri-Poincaré)
The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.
IECL Institut Elie Cartan de Lorraine
IHPST Institut d'Histoire et de Philosophie des Sciences et des Techniques
MCMP Munich Center of Mathematical Philosophy
LHSP-AP Laboratoire d'Histoire des Sciences et de Philosophie - Archives henri-Poincaré
Help of the ANR 450,287 euros
Beginning and duration of the scientific project: April 2018 - 36 Months