PROGRAM
Wednesday, 18th October
Université Paris Cité, Olympe de Gouges building, Room 628
- 2 pm to 3.30 pm - Øystein LINNEBO (Université d’Oslo)
Potentialism in the Philosophy and Foundations of Mathematics
Aristotle famously claimed that the only coherent form of infinity is potential, not actual. However many objects there are, it is possible for there to be yet more ; but it is impossible for there in fact to be infinitely many objects. Although this view was superseded by Cantor’s transfinite set theory, even Cantor regarded the collection of all sets as “unfinished” or incapable of “being together”. In recent years, there has been a revival of interest in potentialist approaches to the philosophy and foundations of mathematics. This talk provides a survey of such approaches, covering both technical results and associated philosophical views.
- 3.45 pm to 7.15 pm - Roy WAGNER (ETH Zürich)
Mathematical entities as unstable translations between presentations
Dominant philosophies of mathematics capture only some aspects of mathematical practice at the expense of what does not fit into some privileged foundation, some privilege cognitive acts, or some contingent empirical or normative context. They sometimes even assume that proper mathematics is perfectly stable and human-independent, demoting the contingencies of real life mathematics to mere shadows of truth.
For me, as a historian-philosopher of mathematical practice, these exclusions go too far. In this talk, I will therefore follow recent decades of Science and Technology Studies to propose a framework that connects mathematics with empirical experience, the plurality of foundational and computational systems, different aspects of cognition, and social-normative constraints. More specifically, I will propose to define mathematical entities as the result of incomplete, underdetermined, intermittent and open-ended translations between systems of material-semiotic presentations. I will explain the terms of this definition, and illustrate it with examples.
Thursday, 19th October
Université Paris 1 Panthéon-Sorbonne, Centre Panthéon, room 6
- 9.30 am to 11.00 am - Antoine CHAMBERT-LOIR (Université Paris Cité, IMJ)
What do we expect from a demonstration : the example of the simplicity of the alternating group.
Taking as an example a theorem from the classical corpus of group theory, the simplicity of the alternating group over at least 5 letters, I’d like to address the following question : what do we expect from a proof, depending on whether we’re learning it, teaching it or writing it ? And, when we do write it, depending on the substrate that hosts it : a draft notebook, a course book, a book of synthesis, a computer library of formal proofs.
- 11.15 am to 12.45 pm - Faustine OLIVA (Université Aix-Marseille, CEPERC)
What does a computer-assisted proof prove ?
In 2005 Gonthier’s team published a third proof of the Four Color Theorem which is an alleged formalization of its second proof in a programming language that makes it checkable by the proof assistant Coq. This proof appears as a mere formalization of an existing proof of a known result, and when we look at its details we notice that the proof of the original statement relies on the proof of its combinatorial version which concerns new objects : combinatorial hypermaps. Thus this proof raises some epistemological and ontological questions that can be grouped into one big question : what does this computer-assisted proof of the 4CT in Coq prove ? To answer we would like to take a step aside and address another question : how does this computer-assisted proof prove ? We will look at what motivates the formalization in the Coq environment and study the formalization choices made to fulfil the purpose of this new proof in order to provide some answers to these questions.
- LUNCH
- 2.30 pm to 4.00 pm - Paola CANTU (Université Aix-Marseille, CEPERC)
What role does axiomatics play today ?
The axiomatic treatment of scientific theories was at the heart of philosophy of mathematics at the beginning of the twentieth century, and a fundamental feature of philosophy of science up to logical empiricism. More recently, general philosophy of science has moved towards less systematic approaches, which, by undermining the unity of science at various levels, have called into question the methodological unity based on the axiomatization of theories. Is mathematics in step with other sciences, or does it still have a deep interest in axiomatics ? And if this interest is no longer linked to the question of foundations, how should we conceive of axiomatics nowadays, and what might its aims be ? In considering the relationship with mathematical practice, a social and dynamic role of axiomatics comes to the fore.
- 4.15 pm to 5.45 pm - Arnon AVRON (Tel Aviv University)
Poincaré-Weyl’s Prédicativity : going beyond Γ0
On the basis of Poincaré and Weyl’s view of predicativity as invariance, we develop an extensive framework for predicative, type-free first-order set theory in which $\g_0$ and much bigger ordinals can be defined as von-Neumann ordinals. This refutes the accepted view of $\g_0$ as the ``limit of predicativity’’. We also explain what is wrong in Feferman-Schütte analysis of predicativity on which this view of $\g_0$ is based.
Friday, 20th October
Université Paris Cité, bât. Olympe de Gouges, salle 628
- 9.30 to 11.00 am - Brendan LARVOR (University of Hertfordshire)
The concept of mathematical proof : how much trouble are we in ?
Philosophers of mathematical practice have been discussing the nature of mathematical proof for a quarter of a century, if we take Yehuda Rav’s (1999) paper as a point of origin. Recent developments in computer proof assistants have added urgency to this discussion as it is now possible to create fully formalised proofs of significant theorems in systems available to undergraduates (such as Lean). One natural approach is to insist on the diversity (BUNTES Gemisch) of mathematical proofs and argue that ’mathematical proof’ is a Wittgensteinian family resemblance concept or a cluster concept in the sense of Lakoff.
I will argue that neither of these approaches succeeds. We do not have a diversity of discrete uses of the term ’proof’, each unproblematic within its proper language-game, because mathematics is not a constellation of discrete language-games, all sealed off from each other (so the Wittgensteinian route is blocked). Nor do we have a cluster of proof-like properties that combine to form a consistent paradigmatic proof-concept (so the Lakoff route is blocked). Rather, we have a single, rich, incoherent concept of mathematical proof. This is not a problem for research mathematicians, but it does present difficulties for anyone committed to making ideological use of the concept of proof, and for everyone employed to teach it.
- 11.15 am to 12.45 pm - Romain PETER (Université de Strasbourg, CRePhAC)
The practice of conceptual philosophers of mathematics
If research into the philosophy of mathematical practice has established itself as a highly fruitful option in the philosophy of mathematics, enabling researchers to turn their attention back to mathematics as it is done, in all its protean richness and below the idealizations that tend to distort what it is, it may not be pointless to consider that the same kind of gaze could be cast on the practice of the philosophy of mathematics itself. More precisely, it is reasonable to think that an approach that has made it possible to better grasp the true practice of mathematicians considered to be eminently "conceptual" (Eisenstein, Gauss, Jacobi, Dirichlet, Riemann, Dedekind), by highlighting the gap that can exist between this ideal and true practice, could also prove useful in better grasping the work of philosophers of mathematics generally considered to be "conceptual".
We’ll start from the premise that any philosophy of mathematics is first and foremost not a doctrine or an assortment of justified theses, but a "theorist’s practice", which constructs conceptual devices by means of heterogeneous montages between writing processes, conceptualization styles, individual and collective knowledge practices, data transformations, normative scaffolding and the tracing of imaginary horizons. We’ll see how Cavaillès animates from within the historical textual material that serves as reference in his theses, and how these different modalities allow us to pose from a different angle the now classic question of retrospective necessity that he identifies between different moments in the development of a theory. We’ll also look at the typical "chains of reference" by which Lautman establishes a series of discontinuities between the basal referential level of mathematical materials and his theses on the dominating dialectic of mathematics. These discontinuities calibrate the work of the concept and enable us to work on "theory movements".
- LUNCH
- 2.30 pm - 4.00 pm - Simon GENTIL (Université Paris Cité, SPHERE)
What is a curve ?
While the study of the first curves can be traced back to antiquity, the same cannot be said of the philosophical discussions that accompany such objects. And with good reason : the idea of a "curved line" was not popularized until several centuries later, when an algebraic method of description was introduced into geometry. The diversity of curves considered in mathematics today legitimizes questions about the links between curves and generality. In particular, the question arises of our ability to define an idea as general, yet equally intuitive today, as that of a curve. The aim of my presentation is to question the general idea of a curve and the obstacles encountered when attempting to define the notion of "curve in general".
The first objective of this presentation will be to show that our intuition is not sufficient to draw a clear boundary delimiting the environment of curves within geometric objects, and that the desire for a mathematical discourse integrating this notion imposes the need for a rigorous definition of what a curve is. The next objective is to show, through a historical analysis, that the notion of "curve in general", which came into its own during the Classical Age, seems to preclude any satisfactory definition of such a notion. Although we may have the intuition of a certain unity between curves, the diversity of imaginable curves makes it impossible to rigorously express such unity. Finally, the third objective will be to show that current definitions do not define all known curves, but rather a subset of them, sometimes even including objects that we would intuitively like to exclude from the term curve. These various conclusions will provide food for thought about our ability, or inability, to propose a satisfactory definition of the notion of curve in all its generality. We will, however, attempt to show how the difficulty of providing a rigorous definition of an intuitive and general notion can be conceived as a driving force in mathematical research.
- 4.15 pm to 5.45 pm - Juliette KENNEDY (Université d’Helsinki)
How first order is first order logic ?
Fundamental to the practice of logic is the dogma regarding the first order/second order logic distinction, namely that it is ironclad. Was it always so ? The emergence of the set theoretic paradigm is an interesting test case. Early workers in foundations generally used higher order systems in the form of type theory ; but then higher order systems were gradually abandoned in favour of first order set theory—a transition that was completed, more or less, by the 1930s.
I will argue in this talk that if one cares to view set theory as a logic—and if we do think of set theory as a logic, it is a logic with the cumulative hierarchy V as its standard (class) model—then set theory turns out to be a stronger logic than second order logic. This is perhaps as it should be, given that the latter restricts the domain of quantifiable objects to those generated by (at most) a single iteration of the power set operation, while set theory allows for arbitrary iterations of the power set operation.
