Une procédure en théorie des preuves qui transforme une preuve en calcul des séquents (ou en déduction naturelle) afin de supprimer les inférences de coupure (applications de la règle 'cut'), produisant une preuve sans coupure satisfaisant typiquement la propriété des sous-formules.

Principe

Les coupures jouent le rôle de lemmes qui peuvent être introduits pour raccourcir des preuves ; l'élimination des coupures remplace systématiquement les coupures par des développements de leurs preuves de sorte que toute formule dans la preuve transformée soit une sous-formule du séquent final, souvent obtenue en réduisant une mesure de complexité des coupures jusqu'à disparition complète.

Démonstration

Hauptsatz de Gentzen : dans les calculs de séquents LK (classique) et LJ (intuitionniste), il existe une procédure d'élimination des coupures. Par exemple, une preuve qui utilise une coupure sur A peut être transformée en composant les dérivations des prémisses et de la conclusion de A puis en permutant et simplifiant les règles d'inférence jusqu'à faire disparaître la coupure, au prix d'une possible augmentation de la longueur de preuve.

Mauvaise application

Penser que l'élimination des coupures produit toujours une preuve plus petite ou plus simple du point de vue computationnel est faux : la procédure peut entraîner une explosion exponentielle ou non élémentaire de la taille de la preuve. Employer l'élimination des coupures naïvement dans des systèmes avec induction ou certains principes de point fixe peut échouer ou nécessiter des arguments méta-systémiques supplémentaires.

Conséquence

Lorsque applicable, l'élimination des coupures fournit des preuves de consistance, la propriété des sous-formules qui soutient des décisions ou des bornes de complexité pour des fragments, et une interprétation constructive des preuves comme calculs normalisés ; elle sous-tend également des résultats d'interpolation et de conservativité.

Inversion

Introduire des coupures (lemmes) dans une preuve sans coupure est la réversion : les coupures peuvent compresser les preuves et les rendre modulaires. La tension entre l'analyticité sans coupure et l'économie par les coupures révèle des rôles complémentaires de la normalisation et de l'ingénierie des preuves.

Limite

Les théorèmes classiques d'élimination des coupures s'appliquent à des calculs de séquents ou systèmes de déduction naturelle bien spécifiés sans certains axiomes puissants ; les extensions aux systèmes avec induction, certains opérateurs modaux ou fix‑points, ou des règles structurelles non classiques peuvent être partielles, exiger des approches stratifiées ou échouer complètement.

Tension sémantique

Se confronte à l'usage pragmatique des coupures comme abréviations de preuve : pureté théorique (preuves analytiques sans coupure) vs concision pratique (utiliser des coupures pour garder les preuves maniables). Il existe aussi une tension entre la normalisation syntaxique et les modèles sémantiques où les coupures correspondent à des effets computationnels.

Synthèse

L'élimination des coupures est une méthode de normalisation syntaxique qui supprime les inférences non analytiques en développant et en permutant la structure de la preuve pour atteindre la propriété des sous-formules ; elle est fondamentale pour des résultats méta-théoriques (consistance, interpolation) mais peut se payer par une augmentation de la taille de la preuve et une perte d'efficacité pratique.