Sémantique de la théorie de la preuve

La sémantique de la théorie de la preuve est une approche de la sémantique formelle qui tente de localiser le sens des propositions et des connecteurs logiques non pas en termes d'interprétations, comme dans les approches tarskiennes de la sémantique, mais dans le rôle que joue la proposition ou le connecteur logique au sein du système formel.

Aperçu[modifier | modifier le code]

Gerhard Gentzen est le fondateur de la sémantique de la théorie de la preuve. Il en fournit la base formelle dans son théorème d'élimination des coupures pour le calcul des séquents, ainsi que quelques remarques philosophiques provocantes sur le fait que la signification des connecteurs logiques soit localisée dans leurs règles d'introduction dans la déduction naturelle. Depuis lors, l'histoire de la sémantique de la théorie de la preuve a été consacrée à l'exploration des conséquences de ces idées.^{[réf. nécessaire]}

Dag Prawitz a étendu la notion de Gentzen de preuve analytique à la déduction naturelle, et a suggéré que la valeur d'une preuve en déduction naturelle peut être comprise comme sa forme normale.^{[réf. nécessaire]} Cette idée se trouve à la base de l'isomorphisme de Curry-Howard et de la théorie des types intuitionniste. Son principe d'inversion est au cœur de la plupart des travaux modernes en sémantique de la théorie de la preuve.

Michael Dummett a introduit l'idée fondamentale de l'harmonie logique en s'appuyant sur une suggestion de Nuel Belnap. En bref, un langage, compris comme associé à certains modèles d'inférences, a une harmonie logique s'il est toujours possible de récupérer des preuves analytiques de toute démonstration, comme on peut le faire pour le calcul séquentiel au moyen du théorème d'élimination des coupures et pour la déduction naturelle au moyen du théorème de normalisation. Dans un langage sans harmonie logique, l'existence de formes d'inférence incohérentes n'est pas exclu et il sera même probablement incohérent.