Il paraît naturel d’énumérer les éléments d’un ensemble fini E, du premier jusqu’au dernier. Ce faisant, on introduit une structure supplémentaire sur l’ensemble E, à savoir un ordre total qui compare les éléments de E entre eux. Bien souvent, un choix d’ordre total s’impose tacitement pour des raisons culturelles ou psychologiques liées à notre perception de l’ensemble E, faisant ainsi oublier son caractère arbitraire. Le formalisme des espèces vise à considérer un ensemble fini indépendamment de tout ordre total sur celui-ci. Il devient alors plus facile de considérer des ordres partiels ou même des topologies sur les ensembles finis, et d’entreprendre l’étude de ces structures.

17h-19h : Alexander Paseau : Quels quantificateurs cardinaux sont-ils logiques?

Par un quantificateur cardinal, nous entendons une expression de la forme “Il y a au moins X…”, ou X est un nombre cardinal, soit fini soit infini. La logique du premier ordre nous permet de définir tous les quantificateurs cardinaux de valeur finie; c’est à dire, “Il y a au moins un…”, “Il y a au moins deux…”, et ainsi de suite. Cependant, les quantificateurs cardinaux infinis ne peuvent point être exprimés par une formule de premier ordre. Cela implique-t-il qu’ils ne sont pas logiques? Nous soutenons, qu’au contraire, tous les quantificateurs cardinaux sont logiques. Nous proposons plusieurs raisons qui mènent à cette conclusion.

JEUDI 28 JUIN

9h-11h : Mathieu Anel : Quelques conséquences du paradigme homotopique

Après avoir rappelé comment les ∞-groupoïdes proposent une nouvelle notion primitive se substituant aux ensembles, on étudiera en quelques problèmes que cela pose.

Problème 1 : que deviennent les notions classiques (groupe, groupe abélien, espace vectoriel, espace topologique…) lorsque les ensemble sous-jacents sont remplacés par des ∞-groupoïdes sous-jacents? On parlera des espaces d’∞-lacets, des spectres et des complexes de chaines du point de vue homotopique.

Problème 2 (complétude) : peut-on définir de manière purement homotopique tous les objets homotopiques qu’on peut construire dans le paradigme des ensembles?

On expliquera comment construire les types d’homotopies des espaces projectifs (réels, complexes et quaternioniques).

11h-13h : Yacin Hamami : Les Démonstrations dans la Pratique Mathématique : Logique, Représentations, et Agentivité

Les démonstrations telles qu’elles figurent dans la pratique mathématique apparaissent le plus souvent comme relativement éloignées de l’idéal mathématique de la démonstration incarné aujourd’hui par la notion de preuve formelle–une notion issue des travaux intenses en logique sur les fondements des mathématiques au cours de la première moitié du siècle dernier. Cet état de fait a conduit plusieurs philosophes et logiciens à entreprendre le développement d’une conception logique et épistémologique des démonstrations plus fidèle à la pratique mathématique. Dans cet exposé, je proposerai un panorama des recherches contemporaines en philosophie des mathématiques poursuivies dans cette direction. Je reviendrai, tout d’abord, sur les différentes dimensions de la notion de preuve formelle en tant qu’incarnation de l’idéal mathématique de la démonstration. J’examinerai, ensuite, en quoi les démonstrations dans la pratique mathématique dévient de cet idéal. Bien qu’ayant généré une littérature substantielle, l’observation de cette déviation ne doit pas constituer une fin en soi, mais doit plutôt apparaître comme un point de départ vers le développement d’une conception plus riche des démonstrations mathématiques. Une manière possible de poursuivre ce projet philosophique consiste à identifier différentes dimensions des démonstrations dans la pratique pouvant se soumettre à des analyses spécifiques. Dans cette perspective, je présenterai quatre dimensions qui ont fait l’objet de travaux récents : (1) le rôle et la nature des représentations non-propositionnelles dans les démonstrations, telles que les diagrammes et les systèmes de notation ; (2) l’importance de la notion de méthode mathématique vis-à-vis de la compréhension et de l’évaluation des démonstrations, mais également dans le rôle épistémologique des démonstrations en tant que véhicules de transmission de la connaissance mathématique ; (3) l’importance de concevoir les démonstrations comme produites par des agents rationnels, pour des agents rationnels ; (4) la nécessité d’une analyse plus fine de la structure des démonstrations. L’objectif de cet exposé est ainsi d’offrir une vue d’ensemble de différentes questions pouvant permettre d’avancer vers le développement d’une conception des démonstrations plus fidèle à la pratique mathématique.

17h-19h : Jean-Michel Salanskis : Forcing et objectivité mathématique

La technique du forcing, introduite par Paul Cohen pour achever la preuve de l’indépendance de l’axiome du choix et de l’hypothèse du continu par rapport au système ZF, enveloppe-t-elle un enseignement sur le statut de l’objet mathématique ?

Ce qui peut le faire croire est qu’elle semble montrer que nous pouvons forcer l’objet à être ce que nous voulons.

Mon intention est de discuter ce problème en prenant en considération plusieurs formulations du forcing, et en me demandant pour commencer si la redistribution des éléments de la notion au fil de ces versions exprime ou révèle quelque chose de l’essence de l’opération du forcing. 

Seront ainsi examinés, au moins, la présentation modèle-théorique du forcing par Robinson, l’usage du forcing en contexte constructiviste, et la sémantique de Kripke-Joyal.

VENDREDI 29 JUIN

9h-11h : Julien Narboux : Vérification mécanique des preuves en géométrie.

La première partie consistera en une courte introduction au domaine de la preuve vérifiée par ordinateur. Pourquoi vérifier des preuves avec un ordinateur ? que peut-on vérifier ? quels sont les défis ?

Dans une seconde partie, je ferai un tour d’horizon de nos formalisations concernant les fondements de la géométrie basées sur les axiomatiques de Hilbert, Tarski et Euclide.

En particulier, je présenterai un travail commun avec Michael Beeson et Freek Wiedijk  qui a consisté à vérifier mécaniquement les preuves du premier livre des Eléments d’Euclide en essayant de rester aussi proche que possible des preuves originales.

Nous terminerons en présentant une preuve syntaxique de l’indépendance de l’axiome des parallèles (travail commun avec Michael Beeson et Pierre Boutry).

Bibliographie :

https://hal.archives-ouvertes.fr/hal-01612807

https://hal.inria.fr/hal-01071431v3

11h-13h : Sébastien Maronne : Naissance de la géométrie cartésienne

Si la Géométrie de Descartes dans ses rapports avec la méthode et la métaphysique cartésiennes a fait l’objet d’innombrables commentaires, il n’en est pas de même de la correspondance dans laquelle on rencontre des objets et des problèmes qui échappent à la juridiction stricte de la Géométrie de Descartes telle qu’elle a été reconstruite par les commentateurs. Jules Vuillemin a pu écrire à propos de ces éléments allogènes à la Géométrie dans son classique Mathématiques et métaphysique chez Descartes  que Descartes «  traite avec mépris ces découvertes [et] les regarde comme de simples procédés que sa méthode récuse.» Il en va de même des éditions latines de la Géométrie données par van Schooten : peu étudiées, elles diffèrent en de nombreux points de la Géométrie, et constituent pourtant le point d’entrée des mathématiciens de la seconde moitié du dix-septième siècle dans la Géométrie cartésienne.  Dans mon exposé, je discuterai la thèse de Vuillemin et poserai la question des rapports entre la méthode et la métaphysique cartésienne et cette géométrie «  étendue ».

17h-19h : Henri Galinon : Quelles justifications pour les “principes de réflexion” ?

Depuis Gödel et Tarski, on sait donner un contenu mathématique précis à l’affirmation de la cohérence et de la vérité d’un système formalisé, et l’on sait également que ces affirmations ne sont pas démontrables dans les systèmes formalisés visés. Depuis les travaux de Feferman dans les années soixante, on appelle  “principes de réflexion” ce genre d’énoncés et leur propriétés logiques ont été étudié systématiquement. Ce qui va nous intéresser dans cette présentation ce ne sont pas les conséquences logiques de ces principes, mais symétriquement la question de leur justification. Depuis leur formulation, en effet, il est apparu à de nombreux logiciens et philosophes que la justification des principes de réflexion présentait un caractère d’évidence particulier, une idée souvent associés à cette autre selon laquelle leur vérité –  ou du moins leur acceptabilité –  serait implicite dans notre attitude vis-à-vis de la théorie objet de la réflexion. Nous examinerons ces thèses et proposerons une autre justification des principes de réflexion.

SAMEDI 10 JUIN

9h-11h : Paul-André Melliès : A quoi ressemblerait une géométrie du raisonnement logique?

L’idée que le raisonnement logique puisse disposer d’une géométrie, ou à défaut d’une topologie, est apparue à la fin des années 1980 dans le travail mené par Jean-Yves Girard sur la logique linéaire et les réseaux de démonstration. Dans le travail que j’ai mené par la suite sur la logique tensorielle et les jeux de dialogue, une version topologique de la sémantique des jeux s’est dégagée, où une démonstration logique se trouve interprétée en un entrelacs topologique. J’expliquerai dans mon exposé comment aller un cran plus loin, et décrire le raisonnement comme un objet topologique produit au sein même de l’espace logique où Eloïse impose sa démonstration à la réfutation portée par Abélard. Pour finir, et si le temps le permet, je donnerai quelques indications de directions possibles dans ce programme de géométrisation de la logique. 

Pour en savoir plus, vous pouvez télécharger mon habilitation ici:

https://www.irif.fr/~mellies/habilitation.html

https://www.irif.fr/~mellies/hdr-mellies.pdf

11h-13h : Marina Imocrante : Termes mathématiques, référence et changement 

N’ayant aucune possibilité d’accès direct, e.g. par interaction causale, aux objets abstraits comme les objets mathématiques, on considère que le seul accès épistémique possible à ces objets est un accès linguistique : les objets mathématiques sont identifiés à travers les définitions posées dans le cadre des théories qui portent sur eux. il s’agit de la thèse de l’accès “ faible ” aux objets mathématiques (Azzouni 1994, 1997), thèse qui peut être mise en relation avec l’épistémologie structuraliste proposée par Stewart Shapiro pour les mathématiques (Shapiro 2011). En partant de ce présupposé, avons-nous les ressources théoriques pour expliquer l’existence, dans l’histoire des mathématiques, de cas de descriptions incompatibles de ce qui est conçu comme étant un même objet ? Un changement dans la définition d’un terme mathématique donné entraine-t-il forcement un changement dans la référence du terme ? 

Notre étude de cas principal concernera le concept d’infinitésimal (Edwards 1979, Bueno 2007). À partir de cet exemple, la possibilité d’élaborer une théorie de la référence pour les termes mathématiques qui soit compatible avec des cas d’ ‘incommensurabilité’ sera envisagée, s’inspirant de la critique aux théories descriptivistes de la référence proposée en philosophie du langage par Aidan Gray (Gray 2014). 

Bibliographie : 

J. Azzouni, Metaphysical Myths, Mathematical Practice, CUP, Cambridge 1994. 

J. Azzouni, “Thick Epistemic Access: Distinguishing the Mathematical from the Empirical”, Journal of Philosophy 94, 1997, pp. 472-484. 

O. Bueno, “Incommensurability in Mathematics”, dans B. van Kerkhove, J. P. van Bendegem (Eds.), Perspectives on Mathematical Practices, Springer, 2007, pp. 83-105. 

C. H. Edwards, The historical development of the calculus, Springer-Verlag, New York 1979. 

A. Gray, “Name-bearing, reference, and circularity”, Philosophical Studies 171, 2014, pp. 207-231. 

S. Shapiro, “Epistemology of Mathematics : What Are the Questions ? What Count as Answers ?”, The Philosophical Quarterly 61(242), 2011, pp. 130-150.