coupure

Cet article est extrait de l'ouvrage Larousse « Dictionnaire de la philosophie ».

Logique

Règle selon laquelle, si C se déduit d'un ensemble de prémisses Γ, et si D se déduit de C et d'un autre ensemble de prémisses Δ, alors D se déduit de Γ et de Δ.

Introduite en 1934 par G. Gentzen⁽¹⁾ dans son « calcul des séquents », la règle de coupure peut être intuitivement justifiée comme suit : si D découle de Δ et de C, alors elle doit aussi découler de Δ et de tout ensemble de prémisses capable d'entraîner C (la règle fait passer d'une situation dans laquelle C intervient à une situation dans laquelle elle a été « coupée » et a disparu). Cette règle, qui n'est pas une règle « logique » à proprement parler (aucune constante logique ne figure dans son énoncé), est plutôt une règle « structurelle », dont on peut donner la représentation suivante :
Γ Γ, Δ
CΔ
D D

Si l'on convient de nommer « séquent » une proposition du type « l'ensemble de prémisses Γ permet de déduire l'énoncé A », on peut présenter comme suit le résultat majeur (« Hauptsatz ») de Gentzen : la règle de coupure est « éliminable », au sens où un calcul dans lequel cette règle est admise ne permet pas de dériver plus de séquents qu'un calcul d'où elle est absente. Ce résultat fondamental a pour conséquence la propriété dite de la « sous-formule » : puisque les coupures peuvent toujours être éliminées de la dérivation d'un séquent, c'est que cette dérivation peut être mise sous une forme « directe », « sans détours », dans laquelle les seules formules qui interviennent sont des sous-formules des formules qui figurent dans le séquent final.

Jacques Dubucs

→ déduction, démonstration, modus ponens