Sur la preuve de consistance de Gauthier et le programme de Frege

Quand Philosophiques m’a donné l’occasion de commenter Internal Logic de Yvon Gauthier, j’étais très heureux — entre autres parce que j’avais l’occasion d’obtenir une copie d’un livre écrit par une figure redoutable de la philosophie des mathématiques au Canada. Après lecture cependant, j’ai pensé que Gauthier et Kluwer avaient conspiré pour produire un livre plutôt décevant. La preuve de consistance pour ce qu’il appelle « l’arithmétique de Fermat » comme thème central du livre constitue une des sources majeures de déception. Pour plusieurs raisons, la preuve est extrêmement difficile à suivre. Une de ces raisons est qu’on aurait souhaité que Gauthier prenne le temps de corriger quelques maladresses avant la publication de l’ouvrage — par exemple, il présente sa logique comme une forme particulière de calcul séquentiel tout en soutenant que « Since our system is a system of local logic (with minimalist and intuitionist properties), in practice we can consider only sequents Γ where ∆ consists of a unique formula » (p. 85). Malheureusement, les règles séquentielles ne sont pas fixées sous cette forme mais toujours sous une forme générale permettant plusieurs formules arbitraires comme conséquents. Pourquoi ne pas avoir pris la peine de présenter adéquatement le système à l’étude ? Les autres raisons sont plus importantes. Une de celles-là concerne la tendance de Gauthier à soutenir que la notation s’explique d’elle-même. C’est là une hypothèse hasardeuse qui fait en sorte que les publications en logique apparaissent souvent terriblement pédantes aux non-logiciens. J’ai lu la définition que Gauthier donne de la fonction d’assignation (p. 88) à plusieurs reprises et je la trouve toujours aussi opaque. Ceci s’explique entre autres par le fait que la définition introduit soudainement, sans explication, une notation que nous n’avons vue nulle part auparavant dans le livre et dont la légitimité n’est pas immédiatement manifeste. De même, lorsque nous passons à l’étape de l’« élimination des constantes logiques », nous sommes invités à réécrire les règles du calcul séquentiel en remplaçant les composantes de la séquence par les polynômes appropriés. Mais ce qui nous manque, c’est une explication arithmétique adéquate de la ligne séparant une séquence de la suivante. La seule explication qui nous est présentée est « that the line has the meaning simply of an ordered sequence of sequents (consisting of the sequences of formulas themselves. » Cela peut paraître bizarre, mais je ne trouve pas cette explication éclairante. Vraisemblablement, ce qui est requis, c’est que les transitions d’une séquence à la suivante correspondent à des transformations arithmétiques légitimes mais qui ont aussi des propriétés appropriées pour modéliser la notion de « following from ». On pourrait s’attendre à des éclaircissements là-dessus en se tournant vers les résultats métalogiques que Gauthier avance pour sa théorie des modèles. C’est-à-dire que lorsqu’il démontre que le sens dans lequel il présente le calcul séquentiel est adéquat pour la classe de modèles qu’il définit, on pourrait vraisemblablement être en mesure de tirer quelque chose de ce qu’il entend par la fonction d’assignation et de la manière par laquelle il souhaite que les règles séquentielles soient comprises. Malheureusement, nous n’avons aucune de ces preuves. En fin de compte, j’avoue que je suis incapable de présenter une évaluation sensée de cette preuve parce que je ne la comprends tout simplement pas. Cela témoigne peut-être de mes propres caprices, mais je ne crois pas me tromper en affirmant que si, moi, je ne peux saisir où Gauthier veut en venir dans ce chapitre, c’est qu’il y a de sérieux problèmes dans sa présentation — soit que la matière est formulée de façon obscure, soit que le nombre de lecteurs potentiels …