Una construcción lógica que, dadas fórmulas A y B con A lógicamente implicando B, produce una fórmula I (el interpolante) que está implicada por A, implica B y menciona solo los símbolos no lógicos comunes a A y B.

Principio

Cuando A ⊨ B se cumple en una lógica con la propiedad de interpolación, existe una I formada exactamente con el vocabulario compartido tal que A ⊨ I e I ⊨ B; el interpolante separa la información aportada por A y B a través de su lenguaje común.

Demostración

En lógica proposicional, sea A = (p ∧ q) y B = (p ∨ r). Como A implica B, un interpolante es I = p: A ⊨ p y p ⊨ B, y I usa solo el símbolo p que aparece en ambas fórmulas.

Aplicación incorrecta

Forzar que el interpolante contenga símbolos que no son compartidos por A y B, o asumir que existe un interpolante en una lógica que carece de la propiedad de interpolación (por ejemplo, ciertas extensiones no clásicas o del primer orden), conduce a afirmaciones de separación incorrectas.

Consecuencia

La interpolación proporciona un testigo modular que aísla la información compartida entre premisas y conclusión; sustenta la verificación composicional, la alineación modular de ontologías y algunas descomposiciones en model checking.

Inversión

La ausencia de una fórmula separadora que use solo símbolos comunes (fallo de interpolación) revierte la garantía: no es posible aislar sintácticamente el contenido compartido aunque semánticamente A ⊨ B pueda sostenerse.

Límite

Se cumple en lógica proposicional y en la lógica clásica de primer orden estándar (teorema de Craig) pero puede fallar en extensiones o fragmentos (algunos sistemas modales, de punto fijo o de segundo orden); la interpolación se refiere al vocabulario no lógico compartido y excluye conectivos lógicos y cuantificadores de la restricción.

Tensión semántica

Los interpolantes son a la vez objetos sintácticos (fórmulas construidas con símbolos) y separadores semánticos (distinguieron modelos de A de contraejemplos de B); hay tensión cuando existe un separador semántico pero ninguna fórmula sintáctica en el lenguaje compartido puede expresarlo.

Síntesis

La interpolación es el proceso de extraer de una implicación A ⊨ B una fórmula I que capture sintácticamente el vocabulario compartido que separa el soporte de A de la consecuencia B, permitiendo razonamiento modular y ocultamiento de información, reconociendo que algunas lógicas no admiten tal separador sintáctico.