Règle de coupure

Ne doit pas être confondu avec Coupure de Dedekind.

Cet article est une ébauche concernant la logique.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

En logique mathématique, la règle de coupure est une règle d'inférence du calcul des séquents, qui généralise le modus ponens. Sa signification est que, si une formule A apparaît comme conclusion dans un séquent et comme hypothèse dans un autre, on peut alors inférer un séquent dans lequel la formule A n'apparaît pas.

Notation formelle

Son écriture formelle en calcul des séquents est:

coupure: ${\cfrac {\Gamma \vdash A,\Delta \qquad \Gamma ',A\vdash \Delta '}{\Gamma ,\Gamma '\vdash \Delta ,\Delta '}}$

Intuition

On peut s'imaginer la formule qui intervient dans la coupure comme ce que les mathématiciens appellent un « lemme ». Dans les prémisses, le premier séquent démontre le lemme, le deuxième séquent utilise le lemme. Dans la conclusion, le séquent résultant de la coupure, énonce comment les conclusions dépendent des hypothèses sans faire référence au lemme.

Élimination

La règle de coupure est l'objet d'un théorème important de logique, le théorème d'élimination des coupures. Il précise que toute formule qui possède une preuve dans le calcul des séquents, qui utilise à un moment ou à un autre la règle de coupure, possède également une preuve sans coupure, c'est-à-dire, une preuve qui n'utilise pas la règle de coupure.

Références

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Cut rule » (voir la liste des auteurs).

Bibliographie

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 la règle de coupure, page 187.