LA SATURATION ISI

Alors l’artifice de la coordination biunivoque entre formules et nombres (qui sont eux-mêmes des formules) permet de rendre vaines les interdictions de la théorie des types (!) : Np est un nombre, individu de type 1, mais mis en correspondance avec une proposition dans laquelle une variable x (de type 1) voit son système de valeurs appliqué (de façon biunivoque) sur l’ensemble de toutes les démonstrations possibles, elle parcourt donc pratiquement tous les types. Si l’on considère non plus l'écriture, mais le sens intuitif de la proposition où figure Np, elle porte sur toutes les démonstrations, elle est donc du type immédiatement supérieur : On peut, en effet, la décider si l’on adjoint au système des Principia le type T, (2) ; mais le même phénomène se reproduirait.

On voit par là le décalage essentiel entre formalisme complet et les relations qu'il a charge d’exprimer ; la façade peut être sauvée parce que l'application des règles d'usage introduit des relations implicites qui n'apparaissent pas dans le formalisme : en y intégrant une partie de la syntaxe, GÔDEL a ressuscité le paradoxe du Menteur que l'on croyait définitivement éliminé. Il n’y a d’ailleurs paradoxe que relativement à la saturation, c’est-à-dire si l’on exige que le système se suffise à lui-même (ou qu’il y ait une seule langue) : la notion de totalité reparaissant rend vaine la distinction des types (faite à l’intérieur du système) ; on ne peut éviter la question de l’appartenance d’un élément à la classe de toutes les classes du système, question débordant le formalisme (en tant que capable de fournir les réponses) mais posée par lui.

HILBERT (*) avait essayé de « forcer la solution » (‘) par

(1) C’est bien entendu grâce à cet artifice et au résultat qu'il procure que la syntaxe est formalisable dans la langue.

(2) GÔDEL (Il), p. 191 n.

(3) HizBERT (XIV), p. 485.

(4) BERNAYS (III), p. 216.