Je sais bien que l'on va encore dire que je suis populiste, poujadise, négatif, anti-intellectuel et défaitiste, mais je trouve qu'il y a quelque chose d'un peu mystérieux et magique dans l'usage des interpolants de Craig pour l'abstraction par prédicats — surtout de part l'usage éminemment syntaxique qui en est fait pour extraire les nouveaux prédicats.

Quant à l'argumentation selon laquelle c'est une méthode complète pour falsifier une propriété d'inaccessibilité, il me semble que c'est une évidence, sachant que les interpolants vont imposer la création de traces de contre-exemple de plus en plus grandes, finissant par atteindre la taille de la plus petite trace concrète falsifiant la propriété.

Nous vivons donc une époque bien triste.