Théorème d'élimination des coupures
De Wikipedia, l'encyclopédie encyclopedia
En logique mathématique, le théorème d'élimination des coupures (ou Hauptsatz de Gentzen) 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[1],[2].