La transformation de preuve qui supprime les inférences de coupure (applications de la règle cut) d'une preuve de style calcul des séquents pour produire une dérivation sans coupure du même séquent final, préservant la démontrabilité tout en modifiant souvent la structure et la taille de la preuve.

Principe

Permuter et simplifier les inférences de sorte que chaque application de la règle de coupure soit successivement éliminée en la remplaçant par des dérivations n'utilisant que des sous-formules de l'objectif ; cela préserve la démontrabilité et engendre des preuves analytiques jouissant typiquement de la propriété des sous-formules.

Démonstration

Dans le calcul des séquents de Gentzen, une preuve qui utilise une coupure sur la formule A peut être transformée en remplaçant la coupure par des dérivations des sous-formules de A à partir des prémisses et en les composant, ce qui donne une preuve du même séquent sans coupure ; l'application répétée supprime toutes les coupures.

Mauvaise application

Supposer que l'élimination des coupures préserve la longueur ou la complexité de la preuve, ou la faisabilité algorithmique en général ; l'utiliser pour affirmer la décidabilité là où le système comporte encore des fragments indécidables, ou ignorer que l'élimination peut faire exploser exponentiellement la taille de la preuve ou introduire des étapes non constructives dans certains cadres.

Conséquence

L'élimination des coupures fournit des preuves sans coupure avec la propriété des sous-formules, permettant des preuves de consistance, des résultats d'interpolation et une analyse fine des preuves ; elle implique que les lemmes introduits par les coupures sont admissibles plutôt qu'essentiels pour la démontrabilité dans le système considéré.

Inversion

En contraste, autoriser les coupures revient à introduire des lemmes : ajouter des coupures peut raccourcir fortement les preuves et offrir modularité et réutilisation, l'inversion mettant l'accent sur la compacité et la structuration compréhensible par l'humain plutôt que sur la forme analytique.

Limite

L'élimination des coupures tient dans de nombreux systèmes de preuve structurels comme LK et LJ de Gentzen sous les règles logiques standard, mais peut échouer ou nécessiter des modifications dans des systèmes avec des règles non standard, des points fixes ou des définitions inductives ; la complexité et la terminaison doivent être considérées séparément.

Tension sémantique

Tension entre l'élimination des coupures pour obtenir des preuves analytiques et la conservation des coupures pour maintenir brièveté et structure : l'analyticité sacrifie la compacité au profit d'un raisonnement fondé sur des sous-formules, et la pratique des prouveurs réintroduit souvent des lemmes (coupures) pour l'efficacité.

Synthèse

L'élimination des coupures est la suppression systématique des inférences non analytiques dans les preuves du calcul des séquents : en transformant et en permutant les règles pour éliminer les coupures, elle produit des preuves à structure analytique qui exposent les dépendances de sous-formules au prix, parfois, d'une taille accrue ou d'un contenu constructif modifié.