La sensation qui me saisit sera à la fin du dialogue entre Wali, Pierre et Marie, page 16, début du dernier paragraphe (Corrélativement…). On n’a pas encore quitté la séduction particulière des paroles de chacun ; pourtant des énoncés apparaissent juste avant, saisissables universellement, semblant effectivement n’être attachés à aucun individu en particulier. Alors, même les rythmes spécifiques des langages de l’un ou de l’autre semblent valoir pour tous.

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.

Un écho récent (peut-être accidentel ?) dans Unfolding, pour quatuor à cordes et électronique de Francesca Verunelli (2012) : chaque geste du quatuor, malgré son efficacité musicale directe, semblait souligner sa simplicité corporelle. Particulièrement les coups de pédale commandant le dispositif électronique. Les notes de programme n’en parlent pourtant pas. Est-ce pour laisser indécidable l’existence dans l’œuvre de cette simplicité, ou parce que rien de tel n’avait été visé par la compositrice ? Hasard circonstanciel, fantaisie contingente du spectateur, ou part véritable de l’œuvre ?

S X Y Z ::= X Z (Y Z)
K A B ::= A

Cette maigre base suffit à construire les booléens, les entiers, les listes, toutes les fonctions effectivement calculables… ce qui en fait déjà un langage extraordinairement expressif pour sa concision. Il permet même de définir un opérateur de point fixe Y ; quelque soit le combinateur F, Y (F) est solution de l’équation F (X) = X.

Pourtant, cette équation n’a pas toujours une solution. Ainsi, quel est le point fixe de Y ? Cette question n’a pas de réponse dans ce calcul, le terme correspondant n’étant pas réductible. On retrouve ici un argument diagonal classique, introduit originellement par Cantor, à la source de l’antinomie de Russel et des théorèmes d’incomplétude de Gödel.

De sorte que ce langage, tout minimal qu’il soit, semble déjà trop expressif, puisqu’il permet de construire des paradoxes. Cette tension sera le moment qui m’intéressera.

http://www.entretemps.asso.fr/Nicolas/TextesNic/Ferneyhough.html

Première œuvre de la série des blocs de Muriel Leray : confrontation d’une ligne et d’une forme minimale. Je localiserais ici mon moment au niveau du p de coup.