Interpolación de Craig

En lógica matemática , el teorema de interpolación de Craig es un resultado sobre la relación entre diferentes teorías lógicas . En términos generales, el teorema afirma que si una fórmula φ implica una fórmula ψ, y ambas tienen al menos un símbolo de variable atómica en común, entonces existe una fórmula ρ, llamada interpolante, tal que todo símbolo no lógico en ρ aparece tanto en φ como en ψ, φ implica ρ, y ρ implica ψ. El teorema fue demostrado por primera vez para la lógica de primer orden por William Craig en 1957. Existen variantes del teorema para otras lógicas, como la lógica proposicional . Una forma más fuerte del teorema de interpolación de Craig para la lógica de primer orden fue demostrada por Roger Lyndon en 1959; ^{[ 1 ] [ 2 ]} el resultado general se conoce a veces como el teorema de Craig - Lyndon .

En lógica proposicional , sea

${\displaystyle \varphi =\lnot (P\land Q)\to (\lnot R\land Q)}$

${\displaystyle \psi =(S\to P)\lor (S\to \lnot R)}$.

Entonces${\displaystyle \varphi }$implica tautológicamente${\displaystyle \psi }$Esto se puede verificar escribiendo${\displaystyle \varphi }$en forma conjuntiva normal :

${\displaystyle \varphi \equiv (P\lor \lnot R)\land Q}$.

Por lo tanto, si${\displaystyle \varphi }$sostiene, entonces${\displaystyle P\lor \lnot R}$sostiene.

${\displaystyle \rho =(P\lor \lnot R)}$.

Sucesivamente,${\displaystyle P\lor \lnot R}$implica tautológicamente${\displaystyle \psi }$. Porque las dos variables proposicionales que aparecen en${\displaystyle P\lor \lnot R}$ocurren en ambos${\displaystyle \varphi }$y${\displaystyle \psi }$, esto significa que${\displaystyle P\lor \lnot R}$es un interpolante para la implicación${\displaystyle \varphi \to \psi }$.

Supongamos que S y T son dos teorías de primer orden. Como notación, denotemos por S ∪ T la teoría más pequeña que incluye tanto a S como a T ; la signatura de S ∪ T es la más pequeña que contiene las signaturas de S y T. Además, denotemos por S ∩ T la intersección de los lenguajes de ambas teorías; la signatura de S ∩ T es la intersección de las signaturas de ambos lenguajes.

El teorema de Lyndon dice que si S ∪ T es insatisfacible, entonces hay una sentencia interpoladora ρ en el lenguaje de S ∩ T que es verdadera en todos los modelos de S y falsa en todos los modelos de T. Además, ρ tiene la propiedad más fuerte de que todo símbolo de relación que tiene una ocurrencia positiva en ρ tiene una ocurrencia positiva en alguna fórmula de S y una ocurrencia negativa en alguna fórmula de T , y todo símbolo de relación con una ocurrencia negativa en ρ tiene una ocurrencia negativa en alguna fórmula de S y una ocurrencia positiva en alguna fórmula de T.

Presentamos aquí una demostración constructiva del teorema de interpolación de Craig para la lógica proposicional . ^{[ 3 ]}

Dado que la demostración anterior es constructiva , se puede extraer un algoritmo para calcular interpolantes. Usando este algoritmo, si n = | átomos (φ') − átomos (ψ)|, entonces el interpolante ρ tiene O (exp( n )) más conectores lógicos que φ (véase la notación Big O para más detalles sobre esta afirmación). Se pueden proporcionar demostraciones constructivas similares para la lógica modal básica K, la lógica intuicionista y el μ-cálculo , con medidas de complejidad similares.

La interpolación de Craig también puede demostrarse mediante otros métodos. Sin embargo, estas demostraciones generalmente no son constructivas :

• Desde el punto de vista de la teoría de modelos , a través del teorema de consistencia conjunta de Robinson : en presencia de compacidad , negación y conjunción, el teorema de consistencia conjunta de Robinson y la interpolación de Craig son equivalentes.
• De manera teórica de demostración , mediante un cálculo de secuencias . Si es posible la eliminación de cortes y, como resultado, se cumple la propiedad de la subfórmula , entonces la interpolación de Craig se puede demostrar mediante inducción sobre las derivaciones.
• algebraicamente , utilizando teoremas de amalgama para la variedad de álgebras que representan la lógica.
• mediante traducción a otras lógicas que disfrutan de la interpolación de Craig.

La interpolación de Craig tiene muchas aplicaciones, entre ellas pruebas de consistencia , verificación de modelos , ^{[ 4 ]} pruebas en especificaciones modulares , ontologías modulares .

• John Harrison (2009). Manual de lógica práctica y razonamiento automatizado . Cambridge, Nueva York: Cambridge University Press . ISBN 978-0-521-89957-4.
• Hinman, P. (2005). Fundamentos de lógica matemática . AK Peters. ISBN 1-56881-262-0.
• Dov M. Gabbay ; Larisa Maksimova (2006). Interpolación y definibilidad: lógicas modales e intuicionistas (Guías de lógica de Oxford) . Publicaciones científicas de Oxford, Clarendon Press . ISBN 978-0-19-851174-8.
• Eva Hoogland, Definibilidad e interpolación. Investigaciones basadas en la teoría de modelos . Tesis doctoral, Ámsterdam, 2001.
• W. Craig, Tres usos del teorema de Herbrand-Gentzen en la relación entre la teoría de modelos y la teoría de la demostración , The Journal of Symbolic Logic 22 (1957), n.º 3, 269–285.