Un metateorema y procedimiento constructivo que, dada una prueba de que la fórmula A implica la fórmula B en una lógica, produce una fórmula intermedia I (un interpolante) que utiliza sólo los símbolos no lógicos comunes a A y B y satisface que A implica I e I implica B.

Principio

Cuando A → B es demostrable en una lógica con la propiedad de interpolación, existe un interpolante construido únicamente a partir del vocabulario compartido; variantes (p. ej. Lyndon) imponen además la preservación de las polaridades de las ocurrencias de predicados.

Demostración

Ejemplo proposicional: sea A = p ∧ r y B = q ∨ r. Como A implica B (r verdadero hace que q ∨ r sea verdadero), un interpolante es I = r: A implica r e r implica B, y r usa sólo el símbolo proposicional común a A y B.

Aplicación incorrecta

Afirmar que existe un interpolante que usa símbolos comunes escogidos arbitrariamente o que preserva rasgos sintácticos (como la estructura de cuantificadores o la polaridad) en lógicas donde esas formas más fuertes de interpolación fallan.

Consecuencia

Permite la descomposición de pruebas y la transferencia de consecuencias entre teorías restringidas al vocabulario compartido; respalda el razonamiento modular, la extracción de especificaciones y ciertos flujos de trabajo de verificación automática.

Inversión

La idea inversa exigiría una fórmula intermedia usando sólo vocabulario no compartido o prohibiendo símbolos comunes; normalmente fracasa y contradice el propósito de la interpolación.

Límite

Se cumple en muchos marcos proposicionales y de primer orden pero falla en algunas extensiones (ciertas teorías con operadores de punto fijo, algunas lógicas modales y de orden superior); la igualdad, la polaridad o predicados específicos de la teoría pueden impedir la existencia o requerir variantes refinadas.

Tensión semántica

Tensión entre interpolación sintáctica (construir un interpolante a partir de una prueba) e interpolación semántica (existencia de una fórmula que separe modelos): algunas lógicas admiten una pero no la versión constructiva o la que preserva polaridad.

Síntesis

La interpolación de Craig es el puente constructivo que extrae, a partir de una prueba de A → B, una fórmula intermedia I expresada sólo en el vocabulario común, tal que A conlleva I e I basta para implicar B, posibilitando la transferencia modular de información y mostrando límites cuando el vocabulario, la polaridad o extensiones lógicas interfieren.