Scholie à la proposition 2 – 2/ L’intensité de l’obstacle éclipse l’influence
(sommaire) (précédent) (suivant)
Si l’on s’arrêtait à sa comparaison avec les temps grammaticaux, la Logique Linéaire ne serait qu’une logique paraconsistante de plus, pour reprendre les propos de Jean-Yves Girard. Pour commencer, elle ne tire pas son origine d’une réflexion philosophique sur la pérennité, comme la section précédente aurait pu le sous-entendre ; mais de problèmes logiques.
Elle est ainsi une logique à négation symétrique qui vérifie l’élimination des coupures et la correspondance Curry-Howard entre preuves et programmes. En décomposant logique classique et logique intuitionniste, elle fournit un cadre unifié pour les étudier. Elle montre l’importance des règles structurelles et leurs conséquences sur les propriétés d’un calcul logique.
Cette fertilité et ces changements de paradigmes ne sont pas dans « Selon ». Ce travail littéraire ne sait pas tirer ces conséquences-là. Car l’intensité de ses conséquences ne se donne que dans le cadre des démonstrations la théorie ; c’est parce qu’elles découlent nécessairement des axiomes qu’elles brillent dans le ciel de la science.
Dit brutalement : de « La surface désigna la couche superficielle d’un objet », on ne déduit pas la correspondance de Curry-Howard. Il n’y a pas à s’en désoler : le poème a d’autres ressources pour rivaliser avec cette belle théorie.