Le pont qui ne tient que pour le fini ✛

Dans le monde de la logique, il y a un pont. Il enjambe le gouffre qui sépare l'admissibilité d'une règle de sa dérivabilité à partir des axiomes. Tant que les règles se contentent d'un nombre fini de prémisses, le pont est solide — pour la logique classique, tout ce qui ne viole pas la vérité est déjà contenu dans la syntaxe. Mais dès qu'on ajoute des prémisses infinies, les piliers commencent à trembler. Le pont, hélas, n'est pas tout-puissant.

La complétude structurelle est une propriété d'un système logique selon laquelle toute règle admissible (qui n'ajoute pas de nouveaux théorèmes) peut être dérivée des axiomes. En 1971, W. Pogorzelski a introduit cette notion, et depuis, elle sert de pierre de touche pour de nombreuses logiques non classiques. La logique intuitionniste, par exemple, n'est pas structurellement complète : il existe des règles qui préservent la vérité sur tous les modèles de Heyting, mais qui ne sont pas dérivables des axiomes. Cependant, pour certains de ses fragments — les logiques de Dummett (LC) et de Medvedev (ML) — le pont supporte le trafic fini.

Le problème survient lorsqu'on autorise des ensembles infinis de prémisses. La propriété appelée κ-complétude structurelle (où κ est un cardinal limitant le nombre de prémisses et de variables) s'avère extrêmement fragile. Dans le nouveau travail, on prouve : si une variété congruente-distributive de type fini est engendrée par des algèbres finies, alors pour tout κ > ω, la κ-complétude structurelle équivaut à la tabularité — c'est-à-dire à l'engendrement par une seule algèbre finie. En d'autres termes, le pont ne tient que si tout l'univers tient dans une table finie. Les logiques LC et ML, dont les classes de modèles contiennent des algèbres indécomposables infinies, échouent à ce test. Une règle infinie admissible — par exemple, une quasi-équation restrictive ω — ne peut pas être dérivée d'une base finie.

La technique de construction de tels contre-exemples est élégante : pour chaque paire d'éléments inégaux d'une algèbre, on introduit une condition qui les relie à une paire distinguée du monolithe. Si l'algèbre est finie, toutes les conditions sont satisfaites, et la conclusion est forcée. Pour les algèbres infinies, en revanche, on trouve une évaluation qui réfute. Cette méthode généralise la méthode classique de Jankov et s'appuie sur des κ-quasi-équations caractéristiques pour les algèbres indécomposables, qui jouent le rôle d'atomes dans la structure de la variété.

Le pont de la logique, semble-t-il, est une construction pour les mondes finis. L'infini, en s'immisçant dans les règles, le fait s'effondrer dans le gouffre entre syntaxe et sémantique. Cette découverte n'est pas une simple curiosité : elle relie la complétude structurelle à des questions profondes d'axiomatisabilité finie et de décidabilité. À terme, cela pourrait mener à l'axiomatisation de fragments fortement complets de la logique intuitionniste, à la recherche de bases optimales et à la clarification de cette frontière subtile où les conséquences finitaires cèdent la place aux conséquences non finitaires. Le pont ne survivra que si nous restons sur la rive du fini.