Élimination des coupures et sémantique
La règle de coupure, dans un calcul logique, est une règle s’approchant du modus ponens : Si on sait que A implique B, et que l’on a A, on peut déduire B. Règle qui apparaît comme la base de la logique. Un résultat, alors paradoxal en apparence, fondamental pourtant, montre que dans de bons systèmes logiques cette règle est redondante : toute preuve peut être exprimée sans cette règle.
Les démonstrations syntaxiques d’élimination des coupures se font le plus souvent en raisonnant sur le contexte des occurrences de cette règle dans une preuve. On regarde tous les cas possibles, et on cherche à réécrire la preuve pour éliminer l’occurrence considérée. La démonstration est fastidieuse, au cas par cas, et obscurcit probablement les propriétés qui la garantissent.
Dans ce contexte, la démonstration d’Okada apparaît singulière. S’appuyant sur une sémantique algébrique, elle évite le cas par cas. La sensation que je compte montrer du doigt ici est dans l’élégance de cette preuve, dont l’éblouissante simplicité semble éclaircir une voie. Voie sur laquelle Kazushige Terui a fait quelques pas depuis.
La simplicité de la preuve m’est d’autant plus frappante que je ne connais pas de bonne description intuitive de la sémantique des phases ; et si je peux suivre la démonstration pas à pas et accorder crédit à chacun d’entre eux, je reste comme étranger à son idée ; la simplification de la démonstration d’élimination des coupures y est formidable, sensible ; et d’autant plus que le système dans lequel se déroule la démonstration (la sémantique des phases) m’est une terre inconnue ; ses rituels me sont exotiques, et d’une efficacité déconcertante pourtant.