Au commencement était la Parole, et la Parole était avec Dieu, et la Parole était Dieu. Ensuite est apparue l’écriture, et enfin la théorie de la preuve dans le courant du XIXe siècle. On intéressera ici plutôt à la théorie de la preuve.

Photographie par Roman Cadre, série "Babel"

Photographie par Roman Cadre, série « Babel »

LES disciplines scientifiques se caractérisent en partie par le langage dans lequel elles s’expriment, que ce soit une langue vivante agrémentée de quelques mots spécifiques comme en sciences humaines, ou des systèmes entièrement formels comme en mathématiques. Chaque époque possède une façon particulière d’appréhender le langage, qui induit un lot d’objets et de concepts. L’espoir, c’est que leur étude satisfasse l’envie de « comprendre quelque chose à la connaissance ». Les auteurs pensent que la logique, qui ne s’intéresse qu’aux langages mathématiques (plus simples et mieux formalisés), naît justement de cet espoir de compréhension. On essaiera ici d’esquisser le chemin parcouru depuis le XIXe siècle. La logique est l’exemple d’une discipline mathématique en perpétuelle construction, où le progrès n’est pas tant dans les réponses données que dans l’évolution des manières de poser les questions.

L’exemple de Tarski : il pleut. 

Comment procéder pour étudier un langage mathématique ? La première idée, c’est de lui donner du sens. Un exemple : Tarski est à l’intérieur de sa maison ; devant lui est inscrit sur une feuille : il pleut. Tarski se demande quand est-ce que cette phrase est vraie ou fausse, cherchant à trouver sa signification. Il comprend qu’elle est vraie lorsqu’il pleut dehors, dans le monde extérieur, et qu’elle est fausse lorsqu’il n’y pleut pas. En fait, la démarche de Tarski est plus complexe qu’il n’y paraît, car cette phrase n’est qu’un ensemble de caractères, qui n’a a priori pas de signification. Mais Tarski crée un lien entre celle-ci et le monde extérieur, et lui donne alors un sens. C’est la même chose avec les langages formels : on crée des mondes mathématiques (comme les entiers naturels, les espaces vectoriels, les nombres complexes), où l’on interprète notre langage formel. Ces mondes mathématiques sont appelés des modèles.

La théorie des modèles

Cette approche est formalisée par la théorie des modèles, qui étudie l’interaction entre deux univers a priori sans relation : l’univers des phrases écrites dans des langages formels, et celui des mondes mathématiques où l’on tente d’interpréter les phrases. L’idée motrice de cette démarche se retrouve dans toutes les disciplines scientifiques : on essaie de savoir où notre théorie s’applique, où nous pouvons lui donner un sens. Cependant, cette démarche ne comble pas nos attentes. Voyons pourquoi. Avec l’espoir de « comprendre la connaissance », on a décidé de trouver un sens au langage, ce qui nous a conduits à la formalisation de la notion de « phrase vraie » : une phrase est vraie lorsqu’on peut trouver un monde mathématique où elle l’est. On l’a fait en s’inspirant de la parabole de Tarski et de la pluie. Mais la différence fondamentale avec la parabole, c’est que Tarski crée un lien entre une phrase formelle et un monde réel, tangible, dans lequel la notion de vérité a un sens : il y a donc un vrai gain. Au contraire, lorsque l’on construit un monde mathématique, celui-ci n’est ni tangible, ni réel, car il est lui-même décrit dans un langage formel, où il n’y pas de notion de vérité. Dire que notre phrase formelle est vraie lorsqu’elle est vraie dans un monde tout aussi formel semble donc être une démarche qui se mord la queue, à la limite de la malhonnêteté. Ce sont des impressions qui reviennent souvent lorsqu’on essaie de définir formellement la Vérité ou d’autres notions en majuscule.

Tant qu’on s’intéresse uniquement au langage, il n’est pas facile de trouver d’autre notion pertinente que celle de Vérité. On s’aperçoit alors qu’on a oublié une chose majeure : la démonstration. C’est pourtant cette notion qui caractérise la science en général, et les manières de démontrer, qui distingue les disciplines scientifiques. Il faut donc nécessairement l’étudier pour « comprendre quelque chose à la connaissance. » De plus, les démonstrations sont des objets très concrets : ce ne sont que des ensembles de phrases qui commencent par des hypothèses et se terminent par une conclusion. C’est donc beaucoup plus simple à définir et à utiliser que la Vérité et il y a moins de risques de tomber dans des réflexions douteuses.

Comment différencier deux démonstrations ? 

Mais qu’a-t-on fait des démonstrations chez Tarski ? Pas grand-chose : s’il y a une démonstration de A sous les hypothèses B, la seule chose qu’on puisse conclure, c’est qu’un monde mathématique qui vérifie les hypothèses B, vérifie A. Mais ainsi, on n’étudie pas la démonstration en tant qu’objet, on la réduit à un « transmetteur de vérité » et on est incapable de différencier deux démonstrations qui ont les mêmes hypothèses et la même conclusion. Tomber dans l’écueil inverse n’est pas non plus souhaitable : à savoir dire que toutes les démonstrations sont différentes et être incapable d’y trouver des ressemblances. On veut en fait réussir à capter une réalité de tous les jours : il arrive que deux personnes démontrent une même chose, mais avec un argumentaire différent, et on ressort avec l’idée que ces démonstrations n’ont rien à voir. À l’opposé, les deux personnes peuvent ne pas utiliser exactement les mêmes mots, mais on sent que les démonstrations sont « en gros » les mêmes.

Retournons aux mathématiques. On cherche alors à « interpréter les preuves », c’est-à-dire à associer à chaque démonstration un objet appartenant à un univers préalablement choisi. Les démonstrations « en gros » identiques seront associées au même objet et celles qui sont totalement différentes à des objets différents. Par exemple, une interprétation connue est celle par les chemins. On peut interpréter une preuve de A sous les hypothèses B, par un chemin de la ville B vers la ville A. Les chemins permettent de refléter des propriétés bien connues sur les preuves. Exemple: si l’on a une démonstration de A en supposant B et une de B en supposant C, alors on a une démonstration A en supposant C. Dans les chemins, cela devient : s’il y a un chemin de la ville B à la ville A et un chemin de la ville C à la ville B, alors il y a un chemin de la ville C à la ville A.

Interpréter les démonstrations se révèle souvent être une activité ardue et les interprétations non triviales et utiles se comptent sur les doigts de la main. On peut citer l’interprétation du Lambda-calcul simplement typé dans les catégories cartésiennes fermées, et l’interprétation de la théorie des types homotopiques dans les groupoïdes.

Félix Loubaton et Hugo Moeneclaey