calcul des séquents

En 1935 Gentzen a proposé la déduction naturelle, un formalisme pour décrire les preuves du calcul des prédicats, dont l'idée était de coller au plus près à la manière dont les mathématiciens raisonnent. Il a ensuite tenté d'utiliser la déduction naturelle pour produire une preuve syntaxique de la cohérence de l'arithmétique, mais les difficultés techniques l'ont conduit à reformuler le formalisme en une version plus symétrique : le calcul des séquents. C'est dans ce cadre qu'il a démontré ce qui devait devenir l'un des théorèmes principaux de la théorie de la démonstration : le théorème d'élimination des coupures. Dag Prawitz a montré en 1965 que ce théorème pouvait se transporter à la déduction naturelle
Pour la suite, voir Wikipédia.org…