Programme

• « Le moment universel de la démonstration
  par Ali Benmakhlouf, Professeur à l’Université de Nice
  La formule $5+7 = 12$ est considérée par Kant comme indémontrable, en raison du fait qu’il ne s’agirait là que d’un calcul et non d’une démonstration, c’est-à-dire d’un calcul qui ne fait pas usage des propositions universelles comme les axiomes ou les postulats. Comment donc évaluer ce moment de l’universel dans une démonstration quand on fait usage de tels principes ? Un détour par Leibniz et par Frege aidera à débrouiller la question.
• « Au coeur des flèches »
  par Loïc Pottier, Chercheur à l’INRIA SophiaAntipolis
  Les mathématiciens sont experts depuis longtemps dans l’art de la formalisation. Calculs, formules, algorithmes sont souvent énoncés sans ambiguité. A tel point que leur mécanisation est largement possible. Les énoncés logiques, théorèmes, conjectures, bénéficient eux aussi d’une formalisation dans le langage mathématique courant.
  Mais pour les démonstrations on en est loin. Pourtant l’essor de la théorie des types a permis depuis trente ans de donner une vision synthétique et profonde de la notion de preuve formelle. Le temps est venu où la mécanisation et la vérification formelle des preuves mathématiques est possible. On tentera d’illustrer cette thèse sur des exemples simples.
• « L’importance de la théorie de la démonstration »
  par Jean-Michel Salanskis, Professeur à l’Université de Paris X
  La « théorie de la démonstration » est un domaine essentiel de la logique mathématique, en plein développement aujourd’hui. Il est né de l’effort qui fut celui de Hilbert au début du siècle pour donner à la pratique mathématique un cadre adéquat et légitime.
  On voudrait, dans cet exposé, expliquer à la fois ce que la théorie de la démonstration apporte à notre compréhension de la notion de preuve mathématique, le lien qui s’établit à travers elle avec l’informatique, et l’intérêt philosophique qui est le sien.