Program

Wednesday, October 18 - Université Paris Cité, Olympe de Gouges building, room 628

14:00-15:30 - Øystein LINNEBO (University of 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.

15:45-17:15 - 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, October 19 - Université Paris 1 Panthéon-Sorbonne, Centre Panthéon, room 6

9:30-11:00 - Antoine CHAMBERT-LOIR (University Paris Cité, IMJ)

Qu'attendons-nous d'une démonstration : l'exemple de la simplicité du groupe alterné.

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-12:45 - Faustine OLIVA (University 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 break

14:30-16:00 - Paola CANTÙ (University 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.

16:15-17:45 - 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 Γ₀ and much bigger ordinals can be defined as von-Neumann ordinals. This refutes the accepted view of Γ₀ as the ``limit of predicativity''. We also explain what is wrong in Feferman-Schütte analysis of predicativity on which this view of Γ₀ is based.

18:00-19:30 - Meeting of the members of the GDR PhilMath.

Friday, October 20 - Université Paris Cité, Olympe de Gouges building, room 628

9:30-11:00 - 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-12:45 - Romain PETER (University of Strasbourg, CRePhAC)

La pratique des philosophes conceptuels des mathématiques

If the philosophy of mathematical practice has established itself as a fruitful option for philosophy of mathematics, by refocusing the researchers’ attention on mathematics as they are really made, in all their protean richness, and beyond the idealizations which tend to misrepresent what they are, maybe it would be useful to consider that the same approach can be applied to philosophy of mathematics itself. More precisely, it is reasonable to think that an approach which has allowed to better grasp the authentic practice of mathematicians considered as « conceptual » (Eisenstein, Gauss, Jacobi, Dirichlet, Riemann, Dedekind) by highlighting the gap between this ideal and the reality of practice, can be equally useful to grasp the work of philosophers of mathematics generally considered as « conceptual ».

Assuming that every philosophy of mathematics is not a doctrine or a set of justified propositions, but first and foremost a practice of theorists which develops conceptual devices by means of writing processes, conceptualization styles, individual and collective practices of knowledge, data transformation, normative scaffolding and by the drawing of imaginary horizons. We will see how Cavaillès animates from the inside the historical texts used as a basis in his doctoral theses, and how these different practical modalities provides an angle to discuss the classical question of retrospective necessity. We will also see the typical « chains of references » that Lautman builds between the basal level of mathematical materials and his claims on a domineering dialectic in mathematics. They create a series of discontinuities which calibrate conceptual work and allow him to work on movements of theories.

Lunch break

14:30-16:00 - Simon GENTIL (University Paris Cité, SPHERE)

Qu’est ce qu’une courbe ?

While the study of the first curves can be traced back to antiquity, the same cannot be said for the philosophical discussions that accompany such objects. And with good reason: the idea of a "curved line" did not become popular until several centuries later, when a method of algebraic description was introduced into geometry. The diversity of curves considered in mathematics today legitimises questions about the links between curves and generality. In particular, we need to ask ourselves whether we are capable of defining an idea as general as that of a curve, even though it is equally intuitive today. 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 a « curve in general ».

The first objective of this presentation will be to show that our intuition is not sufficient to draw a clear line demarcating the environment of curves within geometric objects, and that the desire for a mathematical discourse that integrates this notion imposes the need for a rigorous definition of what a curve is. The next objective will be to show, in the light of history, that the notion of "curve in general", which came into its own during the Early Modern Period, seems to prevent any satisfying definition of such a notion. Although we may have an intuition of a certain unity between curves, the diversity of imaginable curves makes it impossible to express such unity rigorously. Finally, the third objective will be to show that the current definitions we use do not define all known curves but 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 satisfying definition of the notion of curve in all its generality. However, we will try to show how the difficulty of providing a rigorous definition of an intuitive and general notion can be seen as a driving force for research in mathematics.

16:15-17:45 - Juliette KENNEDY (University of 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.