Considérons le problème suivant : étant donné une logique L permettant d'exprimer l'arithmétique, est-ce que pour tout programme qui ne termine pas sur l'entrée vide, on peut exhiber une preuve de ce fait dans L ? (Pour préciser la question : à tout programme on peut associer une formule Σ1 de l'arithmétique, exprimant qu'il termine, par exemple par la construction de Cook dans son théorème de complétude relative de la logique de Hoare à coup de codage de Gödel. Il s'agit de prouver cette formule.)

La réponse est négative (sauf délire de ma part) : il existe des programmes qui ne terminent pas, mais L n'arrive pas à prouver cela car il existe des modèles non standards de L où il y a un témoin de terminaison (une instanciation des quantificateurs existentiels).

Bien entendu, on peut toujours concocter des modèles, mais existe-t-il un exemple raisonnable de programme (à part un programme qui énumère des preuves..) qui produit cela ? Ceci rejoint un domaine de recherche : pondre des problèmes indécidables dans Peano sans avoir recours à la théorie de la preuve... il me semble avoir vu un exemple de suite dont le passage à zéro (donc la terminaison du programme associé) est dans ce cas.