PROGRAMME
Mercredi 18 octobre
Université Paris Cité, bât. Olympe de Gouges, salle 628
- 14h00 - 15h30 - Ø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.
- 15h45 - 17h15 - 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.
Jeudi 19 octobre
Université Paris 1 Panthéon-Sorbonne, Centre Panthéon, salle 6
- 9h30 - 11h00 - Antoine CHAMBERT-LOIR (Université Paris Cité, IMJ)
Qu’attendons-nous d’une démonstration : l’exemple de la simplicité du groupe alterné.
En prenant pour exemple un théorème du corpus classique de théorie des groupes, la simplicité du groupe alterné sur au moins 5 lettres, je voudrais aborder la question suivante : qu’attendons-nous d’une démonstration, en particulier suivant que nous l’apprenons, l’enseignons, ou la rédigeons. Et, lorsque nous la rédigeons, suivant le substrat qui l’accueille, un cahier de brouillon, un ouvrage de cours, un ouvrage de synthèse, une librairie informatique de preuves formelles.
- 11h15 - 12h45 - 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.
- PAUSE DEJEUNER
- 14h30 - 16h00 - 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.
- 16h15 - 17h45 - 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.
Vendredi 20 octobre
Université Paris Cité, bât. Olympe de Gouges, salle 628
- 9h30 - 11h00 - 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.
- 11h15 - 12h45 - Romain PETER (Université de Strasbourg, CRePhAC)
La pratique des philosophes conceptuels des mathématiques
Si la recherche en philosophie de la pratique mathématique s’est imposée comme une option très fructueuse en philosophie des mathématiques, en permettant de ramener l’attention des chercheurs vers les mathématiques telles qu’elles se font, dans toute leur richesse protéiforme et en deçà des idéalisations qui tendent à déformer ce qu’elle est, il n’est peut être pas inutile d’envisager que le même type de regard puisse être porté sur la pratique de la philosophie des mathématiques elle-même. Plus précisément, il est raisonnable de penser qu’une démarche qui a permis de mieux ressaisir la pratique véritable de mathématiciens considérés comme éminemment « conceptuels » (Eisenstein, Gauss, Jacobi, Dirichlet, Riemann, Dedekind), en mettant en avant l’écart qui peut exister entre cet idéal et la pratique véritable, puisse également s’avérer utile pour mieux saisir le travail de philosophes des mathématiques généralement considérés comme « conceptuels ».
Nous partirons donc du principe que toute philosophie des mathématiques est avant tout, non une doctrine ou un assortiment de thèses justifiées, mais une « pratique de théoriciens », qui construit des dispositifs conceptuels par le moyen de montages hétérogènes entre des processus d’écriture, des styles de conceptualisation, des pratiques individuelles et collectives du savoir, des transformations de données, des échafaudages normatifs et le tracé d’horizons imaginaires. Nous verrons ainsi comment Cavaillès anime de l’intérieur le matériau textuel historique qui lui sert de référence dans ses thèses, et comment ces différentes modalités permettent de poser sous un angle différent la question, devenue classique, de la nécessité rétrospective qu’il dégage entre différents moments de développement d’une théorie. Nous verrons également les « chaînes de références » typiques par lesquelles Lautman instaure entre le niveau référentiel basal des matériaux mathématiques et ses thèses sur la dialectique dominatrice des mathématiques une suite de discontinuités qui étalonnent le travail du concept et permettent de travailler sur des « mouvements de théories ».
- PAUSE DEJEUNER
- 14h30 - 16h00 - Simon GENTIL (Université Paris Cité, SPHERE)
Qu’est ce qu’une courbe ?
Si on peut ramener l’étude des premières courbes à l’Antiquité, il n’en est pas de même des discussions philosophiques qui accompagnent de tels objets. Et pour cause, l’idée de « ligne courbe » ne se popularise que plusieurs siècles plus tard, lors de l’introduction d’une méthode de description algébrique en géométrie. La diversité des courbes considérées aujourd’hui en mathématiques légitime un questionnement sur les liens entre courbes et généralité. En particulier, on peut se poser la question de notre capacité à définir une idée aussi générale, bien qu’également intuitive de nos jours, que celle de courbe. Ma présentation a pour but de questionner l’idée générale de courbe et les obstacles rencontrés lorsque l’on tente de définir la notion de « courbe en général ».
Le premier objectif de cette présentation sera de montrer que notre intuition ne suffit pas à tracer une frontière nette délimitant l’environnement des courbes au sein des objets géométriques et que la volonté d’un discours mathématique intégrant cette notion impose la nécessité d’une définition rigoureuse de ce qu’est une courbe. L’objectif suivant sera de montrer par une analyse historique que la notion de « courbe en général », qui prend du sens durant l’Âge classique, semble empêcher toute définition satisfaisante d’une telle notion. Bien que l’on peut avoir l’intuition d’une certaine unité entre les courbes, la diversité des courbes imaginables rend impossible l’expression rigoureuse d’une telle unité. Enfin le troisième objectif sera de montrer que les définitions actuelles que l’on utilise ne définissent pas l’ensemble des courbes connues mais un sous-ensemble de celles-ci, intégrant parfois même des objets que l’on souhaiterait intuitivement exclure de la dénomination courbe. Ces différentes conclusions viendront nourrir une réflexion sur notre capacité, ou notre impossibilité, à proposer une définition satisfaisante de la notion de courbe dans toute sa généralité. Nous tenterons toutefois de montrer comment la difficulté de fournir une définition rigoureuse d’une notion intuitive et générale peut être conçue comme un moteur de la recherche en mathématiques.
- 16h15 - 17h45 - 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.
