Un cadre déductif formel dans lequel les séquents sont les unités syntaxiques principales et les preuves se construisent en appliquant des règles d'inférence structurelles et logiques aux séquents, incluant souvent une règle de coupure et éventuellement des règles structurelles comme l'affaiblissement, la contraction et la permutation.

Principe

Le calcul des séquents organise la déduction autour de manipulations locales des composantes antécédente et conséquente ; cette localité favorise les transformations modulaires de preuves (par ex. élimination de la coupure) et la recherche systématique de preuves.

Démonstration

Dans le calcul des séquents classique LK, on peut dériver A∨B ⇒ A∨B initialement par des axiomes d'identité puis utiliser les règles d'introduction gauche/droite pour construire des preuves plus longues ; une démonstration classique est l'élimination de la coupure, transformant une preuve qui utilise la coupure en une preuve sans coupure.

Mauvaise application

Traiter les règles du calcul des séquents comme des règles de réécriture sémantique plutôt que comme des étapes d'inférence syntaxiques, ou appliquer des règles structurelles non restreintes dans des contextes (par ex. logique linéaire) où elles sont interdites, conduisant à des dérivations non valides ou hors sujet.

Conséquence

Le calcul des séquents permet d'obtenir des résultats méta-théoriques (élimination de la coupure, consistance, propriété de sous-formule dans certaines formulations) et des outils pratiques (recherche de preuve descendante systématique, base pour démonstrateurs automatiques et transformations de preuves).

Inversion

L'inversion consiste à adopter des cadres alternatifs (déduction naturelle, systèmes de Hilbert) où les règles d'inférence agissent sur des formules plutôt que sur des séquents ; la comparaison met en évidence des compromis différents entre symétrie, localité et taille des preuves.

Limite

S'applique à la théorie syntaxique des preuves et aux systèmes formels qui représentent l'entaillement par des séquents ; il ne fournit pas lui-même de modèles sémantiques et doit être instancié par une signature logique et un ensemble de règles — des choix différents donnent des variantes classiques, intuitionnistes, linéaires, etc.

Tension sémantique

La tension apparaît entre le calcul des séquents et la déduction naturelle : le calcul privilégie la symétrie et la manipulation structurelle des contextes, tandis que la déduction naturelle privilégie l'introduction/élimination des connecteurs et souvent des preuves plus compactes pour le raisonnement humain.

Synthèse

Le calcul des séquents est une architecture déductive centrée sur les séquents et régie par des règles, qui explicite les opérations structurelles, permet des théorèmes rigoureux de transformation des preuves et facilite la recherche mécanisée de preuves, tout en étant paramétrable par le choix des règles.