Élimination des coupures

L'élimination des coupures est le théorème de Gentzen selon lequel la règle de coupure, qui formalise l'utilisation des lemmes, peut être supprimée de toute preuve en calcul des séquents, ne laissant qu'une preuve construite uniquement à partir des formules qu'elle concerne.

Definition

L'élimination des coupures est le théorème et la procédure constructive montrant que toute dérivation en calcul des séquents utilisant la règle de coupure peut être transformée en une dérivation qui ne l'utilise pas, de sorte que chaque séquent prouvable possède une preuve dans laquelle seules des sous-formules du séquent final apparaissent.

Scope

Ce sujet aborde la règle de coupure et son rôle dans le calcul des séquents, la procédure d'élimination des coupures et sa terminaison, la propriété de la sous-formule des preuves sans coupure, les conséquences qui en découlent en termes de cohérence et de décidabilité, ainsi que les bornes sur la taille des preuves que l'élimination peut entraîner.

Core questions

• Qu'exprime la règle de coupure et pourquoi sa suppression est-elle significative ?
• Comment la procédure d'élimination des coupures se termine-t-elle ?
• Qu'est-ce que la propriété de la sous-formule et qu'implique-t-elle pour la recherche de preuves ?
• Quel est le coût computationnel de l'élimination des coupures ?

Key theories

Gentzen Hauptsatz

Le théorème principal de Gentzen stipule que la règle de coupure est admissible dans le calcul des séquents, de sorte que toute preuve utilisant des coupures peut être convertie en une preuve sans coupure du même séquent final.

Propriété de la sous-formule

Toute formule apparaissant dans une preuve sans coupure est une sous-formule du séquent final, ce qui contraint la forme de la preuve et sous-tend les procédures de décision et les arguments de cohérence.

Cohérence via l'élimination des coupures

Puisqu'une preuve sans coupure du séquent vide est impossible, l'élimination des coupures fournit une preuve directe que le calcul, et par conséquent la théorie qu'il formalise, est cohérent.

Clinical relevance

L'élimination des coupures est un résultat fondamental aux vastes conséquences : il permet d'obtenir des preuves de cohérence, la propriété de la sous-formule essentielle à la démonstration automatique de théorèmes et aux méthodes de tableaux, les théorèmes d'interpolation et, via la correspondance preuves-programmes, la normalisation des programmes typés.

History

Gentzen a prouvé l'élimination des coupures, son Hauptsatz, en 1934 pour la logique du premier ordre, et la méthode est devenue la pierre angulaire de la théorie de la preuve structurelle. Tait et Girard ont étendu la technique à des systèmes plus puissants et à la logique d'ordre supérieur, et les bornes sur la croissance de la taille des preuves sous l'élimination des coupures sont devenues un sujet d'étude à part entière.

Key figures

• Gerhard Gentzen
• William Tait
• Jean-Yves Girard
• Gaisi Takeuti

Seminal works

• takeuti1987
• troelstra2000
• negri2001

Frequently asked questions

Qu'est-ce qu'une coupure dans une preuve ?

La règle de coupure permet de prouver un lemme puis de l'utiliser : à partir d'une dérivation établissant une formule et d'une autre utilisant cette formule comme prémisse, elle conclut le résultat combiné. L'élimination des coupures montre que de tels lemmes intermédiaires peuvent toujours être supprimés en principe.

Pourquoi l'élimination des coupures peut-elle rendre les preuves beaucoup plus longues ?

La suppression d'une coupure peut nécessiter la duplication de grandes parties d'une dérivation, et l'itération de ce processus peut faire exploser la taille de la preuve par une tour d'exponentielles. Ainsi, les preuves sans coupure sont conceptuellement plus simples mais peuvent être considérablement plus grandes que les preuves originales avec coupures.