séquent de Gentzen

Imaginez une démonstration présentée comme un dossier : à gauche figurent les hypothèses disponibles, à droite la conclusion à établir. Le signe placé entre les deux se lit « permet de démontrer ». L'ensemble forme un séquent.

Chaque règle transforme un ou plusieurs dossiers déjà justifiés en un nouveau. En remontant ces transformations jusqu'à des évidences comme « P permet de démontrer P », on rend visibles toutes les étapes du raisonnement.

Un séquent met en regard un contexte d'hypothèses et ce que l'on cherche à en déduire. Notons Γ la collection d'hypothèses et A la formule visée. Dans une présentation à conclusion unique, il s'écrit $\mathrm{\Gamma }⊢A\backslash Gamma\; \backslash vdash\; A$ et affirme qu'il existe une dérivation formelle de A à partir de Γ dans le calcul choisi. Le symbole ⊢ exprime donc une relation syntaxique de démontrabilité.

Une dérivation est un arbre. Ses feuilles sont des séquents initiaux, par exemple une formule déduite d'elle-même. Ses branches appliquent des règles d'inférence, et sa racine est le séquent démontré. Les règles logiques introduisent ou analysent des connecteurs comme « et ». Les règles structurelles, lorsqu'elles appartiennent au calcul retenu, agissent sur les hypothèses : l'affaiblissement en ajoute une, la contraction fusionne des répétitions et l'échange change l'ordre.

La notation varie selon le système. Dans un calcul classique à conclusions multiples, une collection Δ remplace A et le séquent prend la forme $\mathrm{\Gamma }⊢\mathrm{\Delta }\backslash Gamma\; \backslash vdash\; \backslash Delta$. Une lecture courante est alors : si toutes les formules de Γ sont vraies, au moins une formule de Δ l'est. D'autres calculs imposent une conclusion unique ou restreignent certaines règles structurelles ; il faut donc annoncer le système avant d'interpréter la ponctuation.

Montrons que l'hypothèse « P et Q » autorise la conclusion « Q et P ». La lettre P désigne une première proposition et Q une seconde. L'arbre de dérivation rend visibles les deux branches nécessaires avant leur réunion.

Données.
Hypothèse : P ∧ Q.
Conclusion : Q ∧ P.
Règles utilisées : identité, affaiblissement à gauche, introduction de ∧ à droite et analyse de ∧ à gauche.

Étape 1. Les séquents initiaux Q ⊢ Q et P ⊢ P expriment que chaque proposition se démontre elle-même.

Étape 2. L'affaiblissement ajoute l'autre proposition parmi les hypothèses. On obtient P, Q ⊢ Q sur une branche et P, Q ⊢ P sur l'autre.

Étape 3. La règle de ∧ à droite réunit les deux conclusions, puis la règle de ∧ à gauche regroupe les deux hypothèses :

Contrôle. Chaque feuille est initiale, et chaque trait correspond à une règle annoncée. La racine est exactement le séquent demandé : aucune hypothèse ni aucun connecteur n'a disparu sans règle.

Pour construire une preuve formelle, on part du séquent visé et l'on cherche quelle règle pourrait en produire le connecteur principal. Face à Q ∧ P à droite, la règle de ∧ impose deux sous-objectifs. Une table de vérité teste la validité, mais elle ne montre pas cette architecture de preuve.

Pour vérifier une dérivation, on contrôle chaque trait de l'arbre séparément : les prémisses doivent avoir exactement la forme exigée par la règle et conduire au séquent écrit dessous. Cette lecture locale est préférable à une simple intuition lorsque la démonstration comporte de nombreuses branches.

Pour rapprocher une preuve en déduction naturelle d'un calcul de séquents, on suit les hypothèses disponibles à chaque étape. Le séquent les affiche explicitement ; on choisit plutôt la présentation en déduction naturelle lorsque l'enchaînement des introductions et éliminations est l'objet principal de la lecture.

Démontrabilité et conséquence sémantique. Le symbole ⊢ indique qu'une dérivation existe dans un système formel. Le symbole ⊨ affirme qu'une conclusion est vraie dans tous les modèles où les hypothèses le sont. Écrire les règles d'une dérivation tranche en faveur de ⊢ ; raisonner sur tous les modèles relève de ⊨.

Séquent et implication. P ⊢ Q exprime une relation syntaxique de dérivabilité entre formules ou contextes : une dérivation de Q à partir de P existe dans le calcul considéré. P → Q est au contraire une formule du langage logique, qui peut apparaître à gauche ou à droite d'un séquent.

Calcul des séquents et déduction naturelle. Ce sont deux présentations formelles de la déduction, pas deux noms interchangeables. Un arbre de séquents affiche un contexte et une conclusion à chaque nœud ; une dérivation naturelle organise directement les introductions et éliminations des connecteurs.

Le séparateur ne suffit pas à fixer le système. Le signe ⊢ est le séparateur standard entre les deux côtés d'un séquent. Une autre notation n'a ce rôle que si une convention distincte la définit explicitement ; en particulier, la flèche → désigne normalement une formule d'implication. Il faut aussi consulter les règles autorisées pour connaître le système considéré.

Le côté droit n'a pas toujours la même taille. Certains calculs acceptent plusieurs conclusions, d'autres au plus une. Une virgule à droite est le symptôme d'un cadre à conclusions multiples ; il faut lire le séquent selon ce cadre, sans le rabattre automatiquement sur la convention à conclusion unique.

Un côté peut être vide. À gauche, le vide signifie qu'aucune hypothèse n'est utilisée. Dans une lecture classique à conclusions multiples, un côté droit vide représente la fausseté : les formules du contexte gauche ne peuvent pas être toutes vraies simultanément. Il faut conserver ce vide : ajouter arbitrairement une formule changerait le séquent.

Les règles structurelles dépendent du calcul. L'exemple emploie l'affaiblissement, mais certains systèmes le restreignent ou l'écartent. Si une étape ajoute, duplique ou réordonne une hypothèse sans règle déclarée, il faut vérifier le calcul au lieu de considérer l'opération comme automatique.

La fiche déduction naturelle présente l'autre organisation formelle citée dans la définition et permet de comparer la manière dont les hypothèses circulent dans une preuve.

La notice Gentzen Gerhard replace le nom attaché aux séquents dans le parcours du mathématicien qui les a introduits.