Le programme a été développé et affiné dans une suite d'articles : la série des Transcendental syntax qui date un peu, à l'exception du dernier (Mars 2020) qui présente les détails du déconfinement de l'arithmétique.
Ainsi qu'une série de textes en français non publiés : La logique 2.0 (Octobre 2017), suivi d'Un tract anti-système (Novembre 2019) et d'Un tract anti-système II : le monstre de Gila et d'L'architecture de la logique ou la fin du monstre de Gila (printemps 2020) qui on donné lieu aux transparents La logique déconfinée.
Pour résumer l'originalité du propos, je vais me concentrer sur deux questions naïves, de l'ordre de celles que l'on pose quand on ne connaît rien à la logique mais que l'on écarte d'un revers de la main quand on croit la connaître.
A ⇒ A, pourquoi ?
La doxa du réalisme axiomatique hausse les épaules : voyons, mon brave, c'est que les deux A réfèrent à la même réalité (« dénotation » frégéenne) ! Si A est vrai, alors A est vrai. Un peu court quand même puisqu'incapable d'expliquer en quoi A ⇒ A diffère de l'autre principe de base de la logique, la coupure (forme stable du bon vieux Modus Ponens « De A et A ⇒ B, conclure B »). Pourtant, dès Lewis Carroll (1893), on sait qu'il y a une différence, même si le « pédophile victorien » s'est emmêlé les pinceaux dans une inepte parodie de Zénon où la Tortue poursuit Achille sans arriver à le rattraper.
Pour les réalistes, les deux A de l'implication sont deux manifestations, deux « occurrences » de la même essence résidant au Ciel et douée, comme la Vierge Marie, de bilocation. Montrez-leur des jumeaux, ils vous expliqueront qu'ils sont des occurrences de la même personne.
Car deux entités syntaxiques écrites à des endroits distincts sont nécessairement distinctes. Les deux A ne peuvent, au mieux, qu'être isomorphes. Et comme on parle de logique et non pas de théologie, cette isomorphie doit référer à un processus finitaire, i. e., accessible et vérifiable. Mais il y a deux candidats.
L'usage : à travers la coupure, A ⇒ A réfère à un processus permettant de transformer une démonstration de A (celle de gauche) en une démonstration de A (celle de droite), en fait la même, mais délocalisée. L'usage est vérifiable, mais seulement au coup par coup : la potentialité des démonstrations de A nous est, en effet, à jamais inaccessible.
L'usine : à travers des tests spécifiques, des cas d'école, on peut se convaincre que A implique réellement A. C'est un peu faire passer un examen à un produit avant de le commercialiser : on en consomme un peu, mais pas tout sinon il n'y aurait plus rien à vendre. Comme je l'ai observé récemment, ces tests ne sont pas forcément nécessaires : ils peuvent être plus stricts que ce que réclame l'usage. C'est ainsi qu'on préserve la finitude des tests.
Ces deux finitudes sont de nature distincte. Elles sont reliées par un résultat prouvant le caractère suffisant, i. e., prédictif, des tests d'usine. Ce qui prend la forme technique d'une élimination des coupures, prouvée sans restriction quant aux méthodes utilisées. Qui se départit définitivement du finitisme : il faut bien d'ailleurs que quelque chose s'en écarte, nous dit l'incomplétude.
a = a, pourquoi ?
La doxa du réalisme axiomatique hausse encore les épaules : voyons, mon brave, c'est que les deux a ont les mêmes propriétés ! Pourtant l'un est à gauche, l'autre à droite du symbole d'égalité. À quoi le cuistre analytique de service répond que la propriété « être à gauche de » est illégale, immorale : elle ne respecte pas la dénotation. Quelles sont donc celles qui la préservent ? Celles compatibles avec l'égalité, mon bon !
Pour éviter cette aporie qui suppose l'égalité pour mieux la définir, le réalisme s'est fait axiomatique : il a condamné la logique au confinement dans des systèmes qui ne proposent que des propriétés (prédicats) compatibles avec l'égalité. D'où cette aberration, l'oxymore du système logique, qui subordonne la raison pure à l'arbitraire axiomatique. Cette expression sonne comme « dictature démocratique » ou encore « religion rationnelle ».
Le calcul des prédicats est un tissu d'erreurs logiques. Par exemple le principe ∀ ⇒ ∃, qui ne sert par ailleurs strictement à rien, repose sur une erreur, la présence de variables non déclarées. Plutôt que de corriger le tir, on a préféré régler son compte au modèle vide qui réfutait l'erreur : c'est la méthode Al Capone de liquidation des témoins gênants. Les réalistes tiennent tellement à leur sacro-sainte réalité qu'ils la modèlent à l'image de leurs préjugés.
Tout cela repose sur un vieux préjugé logique : il y aurait, venus d'on ne sait trop où, des individus, lesquels auraient des propriétés, un peu comme le chien a des poils ou le poisson des écailles. Pourtant, après un bon siècle de logique, il y a toujours comme un appel d'air au moment de l'introduction des individus : « supposons nous être donné un univers de référence externe... » À partir de là tout s'enchaîne pour se terminer dans l'aporie de l'égalité de Leibniz qui ne survit que protégée par la muraille d'un système.
Mais la solution saute aux yeux, tellement évidente que personne n'y avait jamais pensé. Les individus sont des propositions particulières et leur égalité n'est autre que l'équivalence logique. Ce qui suppose la logique linéaire ; il n'est pas question, en effet, de tout réduire au « classique » qui ne laisserait que deux individus, le vrai et le faux. Pour qui se demandait à quoi sert la logique linéaire, la réponse est claire : à déconfiner, à se passer de système.
Les préjugés essentialistes ont la peau dure. C'est ainsi que la logique linéaire, dans son enfance, avait cru devoir définir des constantes multiplicatives sur la base des catégories, sémantique raffinée, mais sémantique tout de même. Ces deux éléments neutres se sont révélés cauchemardesques et sont donc des erreurs. Par contre, il y a bien deux atomes multiplicatifs auto-duaux, フ et ヲ (fu et wo). Ce sont les deux versions possibles du réseau à un point, qui diffèrent quant à leur gestion de la vérité. Celle-ci n'obéit plus au pléonasme tarskiste « La vérité est qualité de ce qui est vrai », mais à un calcul topologique basé sur l'invariant d'Euler-Poincaré.
Il est toujours difficile de s'évader d'une prison. Celle des valeurs de vérité était la plus sévère car les autodidactes qui ont cru s'en affranchir en changeant les tables n'ont fait qu'échanger une cellule étroite mais commode pour une autre, biscornue, voir les exsangues « logiques » à plusieurs valeurs. C'est l'idée-même de valeur de vérité qu'il convient d'abandonner car l'invariant d'Euler-Poincaré ne s'applique pas aux propositions mais à leurs preuves, ce qui fait voler en éclats les lapalissades à la Tarski. Ainsi, une conjonction peut-elle être vraie, i. e., avoir une preuve vraie, sans que ses deux composantes ne le soient.
L'arithmétique, traitée axiomatiquement depuis le temps de Peano, devient purement logique : les propositions multiplicatives construites à partir de フ correspondent aux entiers relatifs.