Un méta-théorème et une procédure constructive qui, à partir d'une preuve que la formule A implique la formule B dans une logique, produit une formule intermédiaire I (un interpolant) qui n'utilise que les symboles non logiques communs à A et B et vérifie A implique I et I implique B.

Principe

Si A → B est démontrable dans une logique qui possède la propriété d'interpolation, il existe un interpolant construit uniquement à partir du vocabulaire partagé ; des variantes (par ex. Lyndon) imposent en outre la conservation des polarités des occurrences de prédicats.

Démonstration

Exemple propositionnel : soit A = p ∧ r et B = q ∨ r. Comme A implique B (r vrai rend q ∨ r vrai), un interpolant est I = r : A implique r et r implique B, et r n'utilise que le symbole propositionnel commun à A et B.

Mauvaise application

Affirmer qu'un interpolant existe en utilisant des symboles communs choisis arbitrairement ou qu'il préserve des caractéristiques syntactiques (comme la structure des quantificateurs ou la polarité) dans des logiques où ces formes plus fortes d'interpolation échouent.

Conséquence

Permet la décomposition des preuves et le transfert de conséquences entre théories limitées au vocabulaire partagé ; soutient le raisonnement modulaire, l'extraction de spécifications et certaines méthodes de vérification automatique.

Inversion

L'idée inverse exigerait une formule intermédiaire n'utilisant que le vocabulaire non partagé ou interdisant les symboles communs ; cela échoue en général et contredit l'objet de l'interpolation.

Limite

Valable dans de nombreux cadres propositionnels et du premier ordre mais peut échouer dans certaines extensions (quelques théories avec opérateurs à point fixe, certaines logiques modales et d'ordre supérieur) ; l'égalité, la polarité ou des prédicats spécifiques à une théorie peuvent empêcher l'existence ou nécessiter des variantes raffinées.

Tension sémantique

Tension entre interpolation syntaxique (construire un interpolant à partir d'une preuve) et interpolation sémantique (existence d'une formule séparant les modèles) : certaines logiques admettent l'une sans admettre la version constructive ou conservant la polarité.

Synthèse

L'interpolation de Craig est le pont constructif qui, à partir d'une preuve de A → B, extrait une formule intermédiaire I exprimée uniquement dans le vocabulaire commun, telle que A entraîne I et I suffit à impliquer B, permettant le transfert modulaire d'information tout en montrant ses limites lorsque le vocabulaire, la polarité ou des extensions logiques posent problème.