Orateur
Description
Je voudrais réfléchir ici à la langue dans laquelle nous faisons des mathématiques, d'abord au sens commun, puis au sens du vocabulaire, presque toujours implicite à nos raisonnements, de la théorie des ensembles. De fait, les librairies de mathématiques formalisées utilisent plutôt (mais pas uniquement) un autre langage, celui de la théorie des types qui, par certains aspects, est plus proche de notre discours dans lequel les « types » des objets mathématiques empêchent d'écrire certaines relations : par exemple, quand bien même un nombre réel peut être défini, au sein de la théorie des ensembles, comme une coupure (Dedekind), c'est-à-dire un ensemble de nombres rationnels.
il fait rarement sens d'écrire l'égalité d'un nombre réel et d'un ensemble de nombres entiers. Et si plusieurs systèmes formels ont droit de cité, pourront-ils communiquer l'un avec l'autre ?