Théorème d'élimination des coupures

En logique mathématique, le théorème d'élimination des coupures est le résultat central établissant l'importance du calcul des séquents. Il a été initialement prouvé par Gerhard Gentzen en 1934 dans son article historique « Recherches sur la déduction logique » pour les systèmes LJ et LK formalisant la logique intuitionniste et classique, respectivement. Le théorème d'élimination des coupures stipule que toute déclaration qui possède une preuve dans le calcul des séquents, faisant usage de la règle de coupure, possède aussi une preuve sans coupure, à savoir, une preuve qui ne fait pas usage de la règle de coupure.

Texte : extrait de l'article Wikipédia « Théorème d'élimination des coupures », sous licence CC BY-SA 4.0.