L’isomorphisme Curry Howard, une révolution mathématique dans le langage mathématique

Le prochain séminaire Aromaths aura lieu le mercredi 24 janvier à 18h10 en salle 15-25-104 et sera présenté par Antonio Mosca.

Sujets abordés : logique, calcul, langage mathématique, preuves, programmes, linguistique, rhétorique, biais cognitifs, pseudo-sciences 

Résumé.

Les histoires de la logique (cf. la bande dessinée Logicomix) , ainsi que les cours universitaires de logique, écrivent le plus souvent leur fin mot avec le théorème d’incomplétude de Gödel. Ce dernier marque en vérité le début d’une toute autre histoire, car il met en avant le clivage (fondamental, car caractérisant en linguistique tout vrai langage) entre ce qu’on fait – les constructions – et ce qu’on dit qu’on fait – les démonstrations -dans et par les formalismes mathématiques. Les théoriciens de la démonstration et les théoriciens du calcul, après avoir vu leurs chemins se séparer ainsi, découvrent toutefois, et établissent, dans les années 1960, une stricte identité entre les preuves et les programmes, et jettent par là un pont tout à fait inattendu entre le « niveau logique » et le « niveau algorithmique » du langage mathématique. Cette correspondance assez spectaculaire, connue comme isomorphisme Curry-Howard, représente un véritable coup de théâtre épistémologique, permettant de relire de façon critique le récit de l’histoire de la logique telle qu’il est souvent fait par et pour les « logiciens philosophes », ainsi que la révolution informatique dont nous faisons aujourd’hui l’expérience.

On verra aussi comment l’isomorphisme Curry-Howard permet d’établir des ponts entre linguistique et mathématique, et comment ce nouveau regard sur la logique peut nous aider à analyser de façon critique les dérives causées par les dynamiques discursives collectives pseudo-logiques (fake news, conspirationnismes, pseudo-sciences, etc).

Votre commentaire

Entrez vos coordonnées ci-dessous ou cliquez sur une icône pour vous connecter:

Logo WordPress.com

Vous commentez à l’aide de votre compte WordPress.com. Déconnexion /  Changer )

Photo Google

Vous commentez à l’aide de votre compte Google. Déconnexion /  Changer )

Image Twitter

Vous commentez à l’aide de votre compte Twitter. Déconnexion /  Changer )

Photo Facebook

Vous commentez à l’aide de votre compte Facebook. Déconnexion /  Changer )

Connexion à %s