La formalisation ne peut pas trancher à la place de la philosophie
Ce que la forme fait bien
La formalisation enregistre les dépendances, sépare des concepts voisins, vérifie une dérivation sous règles fixes et propage les effets d’une prémisse modifiée. Elle rend visibles des sauts que la prose peut dissimuler.
Son intérêt n’est pas le prestige mathématique, mais la possibilité de contrôler le registre. Pourtant, si la notation prétend achever le jugement, elle fait disparaître le choix du champ, des objets et des règles qui l’a rendue possible.
Le jugement n’est pas une fonction déjà donnée
Un système formel répond à ce qui suit de prémisses et de règles fournies. Il ne décide pas seul quelle expérience doit être saisie, quelle distinction compte, quelle logique emprunter ni comment interpréter le résultat. Ces choix portent une responsabilité philosophique.
Les cinq configurations prouvent que certains postulats sont séparables ; elles ne décident pas quelle configuration le réel doit adopter. La forme teste une relation. Elle ne donne pas l’ordre d’y croire.
Le théorème de l’ouvrier
Le théorème de l’ouvrier affirme que l’exécution de prémisses et de règles fixes ne complète pas le jugement. Un ouvrier peut pousser très loin une branche, mais non retailler de lui-même son substrat. On le reconnaît à son travail, non à son origine humaine ou machinique.
Humains et IA peuvent donc être ouvriers lorsqu’ils exécutent un cadre. Interroger le cadre est un autre travail, lui aussi faillible. Logiques, notations et outils empruntés doivent être inscrits, avec ce que la formalisation conserve, perd et ajoute.