Théorème d'élimination des coupures

Un séquent est une expression logique concernant plusieurs phrases, sous la forme  « ${\displaystyle A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots }$ », qui est lu « ${\displaystyle A_{1},A_{2},A_{3},\ldots }$ prouve ${\displaystyle B_{1},B_{2},B_{3},\ldots }$ », et (comme déclaré par Gentzen) doit être compris comme équivalente à la proposition «  Si (${\displaystyle A_{1}}$ et ${\displaystyle A_{2}}$ et ${\displaystyle A_{3}}$ …) alors (${\displaystyle B_{1}}$ ou ${\displaystyle B_{2}}$ ou ${\displaystyle B_{3}}$ …). »[3] Notez que le côté gauche (CG) est une conjonction (et) et le côté droit (CD) est une disjonction (ou).

Le CG peut avoir arbitrairement plus ou moins de formules; lorsque le CG est vide, le CD devient une tautologie. Dans LK, le CD peut aussi avoir un certain nombre de formules, s'il n'en a pas, le CG est une contradiction, alors que dans LJ, le CD ne peut avoir soit qu'une formule, soit aucune: nous voyons ici qu'avoir plus d'une formule du CD est équivalent, en présence de la règle de contraction droite, à l'admissibilité du principe du tiers exclu (car ${\displaystyle \vdash P,\lnot P}$ est alors prouvable). Depuis la logique LC de Jean-Yves Girard, il est facile d'obtenir une formalisation assez naturelle de la logique classique où le CD contient au plus une formule.

La « coupure » est une règle du calcul des séquents, et est équivalente à une variété de règles d'autres théories de la démonstration, ce qui, étant donné

• ${\displaystyle \Gamma \vdash A,\Delta }$

et

• ${\displaystyle \Pi ,A\vdash \Lambda }$

permet de déduire

• ${\displaystyle \Gamma ,\Pi \vdash \Delta ,\Lambda }$

Autrement dit, il « coupe » les occurrences de la formule ${\displaystyle A}$ hors de la relation d'inférence.

Le théorème d'élimination des coupures stipule que, pour un système donné, tout séquent prouvable en utilisant la règle de coupure peut être prouvé sans l'utilisation de cette règle.

Pour le calcul des séquents, qui ont seulement une formule du CD, la règle de coupure, étant donné

1. ${\displaystyle \Gamma \vdash A}$

et

1. ${\displaystyle \Pi ,A\vdash B}$

permet de déduire

1. ${\displaystyle \Gamma ,\Pi \vdash B}$

Si nous considérons ${\displaystyle B}$ comme un théorème, alors l'élimination de la coupure dans ce cas, dit simplement qu'un lemme ${\displaystyle A}$ utilisé pour démontrer ce théorème peut être inliné. Chaque fois que la démonstration du théorème mentionne le lemme ${\displaystyle A}$, nous pouvons remplacer les occurrences de la démonstration de ${\displaystyle A}$. Par conséquent, la règle de coupe est admissible.

• Karim Nour, René David, Christophe Raffalli Introduction à la logique : Théorie de la démonstration - Cours et exercices corrigés, ed. Dunod. Plus spécifiquement concernant l'élimination des coupures, pages 200-211.

• Gerhard Gentzen, « Untersuchungen über das logische Schließen. I », Mathematische Zeitschrift, vol. 39 (2),‎ 1935, p. 176–210 (DOI 10.1007/bf01201353)
• Gerhard Gentzen, « Untersuchungen über das logische Schließen. II », Mathematische Zeitschrift, vol. 39 (3) 1935, p. 405–431 (DOI 10.1007/bf01201363)
• Gerhard Gentzen, « Investigations into logical deduction », American Philosophical Quarterly, vol. 1,‎ 1964, p. 249–287
• Gerhard Gentzen, « Investigations into logical deduction », American Philosophical Quarterly, vol. 2,‎ 1965, p. 204–218
• Untersuchungen über das logische Schließen I
• Untersuchungen über das logische Schließen II
• (de) Haskell Brooks Curry, Foundations of mathematical logic, New York, Dover Publications Inc., 1977 (1^re éd. 1963), 408 p. (ISBN 978-0-486-63462-3, lire en ligne)
• (de) Stephen Cole Kleene, Introduction to metamathematics, Ishi Press International, 2009 (1^re éd. 1952), 576 p. (ISBN 978-0-923891-57-2)