Pour mémoire, le théorème d'incomplétude de Gödel est un théorème de logique mathématique qui dit que dans tout système formel * (grossièrement parlant, un système de règles permettant de faire des raisonnements mathématiques) suffisamment puissant pour représenter l'arithmétique de Péano (les règles usuelles sur les entiers avec addition et multiplication), alors il existe des énoncés indécidables. Un « énoncé indécidable », c'est la version mathématique et formelle des questions sur l'âge du capitaine : rien ne permet de conclure à une réponse positive ou négative, ou, en d'autres termes, aussi bien une réponse positive que négative restent cohérentes. Ce que dit Gödel, c'est que même dans un domaine apparemment aussi contraint que l'arithmétique, il existe forcément des énoncés indécidables, et que même si on leur donne « de force » une valeur (« nous supposerons à partir de maintenant que l'âge du capitaine est supérieur à 45 »), on obtient un nouveau système avec encore des énoncés indécidables.

* Tout système formel au premier ordre, consistant (merci David), avec ensemble des axiomes récursivement énumérable, pour être précis.

Je ne vais pas plus parler sur le théorème de Gödel, qui a déjà fait couler beaucoup d'encre, et je renverrai par exemple à ce petit ouvrage. Je note cependant qu'une démonstration assez « simple » (du moins pour un informaticien) de ce théorème s'obtient à partir de la construction de Cook pour démontrer la complétude relative de la logique de Hoare par rapport à l'arithmétique sous-jacente, voir par exemple l'ouvrage de Winskel.

Revenons à Bouveresse. Dans le compte-rendu de cette conférence on lui attribue les propos suivants :

L'indécidabilité logique dont il est question dans la théorie des systèmes formels n'a absolument rien à voir avec la question de la signification, puisque l'ensemble des expressions qui constituent l'équivalent des expressions douées de sens d'une langue naturelle, autrement dit, des expressions bien formées du système, est toujours décidable ou, comme on dit, récursif.

L'ensemble des expressions bien formées d'une langue naturelle (au sens de : respectant les règles de grammaire) est certes récursif si l'on admet l'idée de Chomsky qu'on peut les obtenir par une grammaire génératrice hors contexte. Cette assertion est cependant déjà discutable en raison de règles de grammaire non locales comme l'accord des pronoms. Si l'on veut désigner plutôt l'ensemble des expressions qui ont un sens, j'ai peur que la classification en récursif vs non récursif n'ait... pas de sens, le problème n'étant pas posé mathématiquement et étant probablement non mathématisable.

Mais, de toute façon, le problème n'est pas là. L'ensemble des énoncés bien formés de l'arithmétique de Péano (au sens du respect des règles de grammaire formelle) est bien sûr récursif. Cela n'empêche pas que l'ensemble des énoncés démontrables ne soit pas récursif (bien qu'il soit bien sûr récursivement énumérable).

Mmmh. Je crois que je vais lire Prodiges et vertiges de l'analogie. Je me méfie des compte-rendus de conférences, il est tellement facile de « savonner » à l'oral, surtout sur un sujet aussi piégeux que le théorème de Gödel. (Piégeux notamment parce qu'il est facile de s'emmêler entre la logique étudiée et la méta-logique, ce que je n'ai certainement pas manqué de faire.)