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 dice que si una fórmula φ implica una fórmula ψ, y las dos tienen al menos un símbolo de variable atómica en común, entonces existe una fórmula ρ, llamada interpolante, tal que cada símbolo no lógico en ρ ocurre. 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. Las variantes del teorema son válidas para otras lógicas, como la lógica proposicional . Roger Lyndon demostró en 1959 una forma más sólida del teorema de interpolación de Craig para la lógica de primer orden; ^{[1] [2]} el resultado general a veces se denomina teorema de Craig-Lyndon .

Ejemplo

En lógica proposicional , dejemos

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

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

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

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

Por lo tanto, si se cumple, entonces se cumple. A su vez, tautológicamente implica . Debido a que las dos variables proposicionales que ocurren en ocurren en ambos y , esto significa que es un interpolante para la implicación . ${\displaystyle \varphi }$ ${\displaystyle P\lor \lnot R}$ ${\displaystyle P\lor \lnot R}$ ${\displaystyle \psi }$ ${\displaystyle P\lor \lnot R}$ ${\displaystyle \varphi }$ ${\displaystyle \psi }$ ${\displaystyle P\lor \lnot R}$ ${\displaystyle \varphi \to \psi }$

Teorema de interpolación de Lyndon

Supongamos que S y T son dos teorías de primer orden. Como notación, sea S ∪ T la teoría más pequeña que incluye tanto S como T ; la firma de S ∪ T es la más pequeña que contiene las firmas de S y T . Sea también S ∩ T la intersección de los lenguajes de las dos teorías; la firma de S ∩ T es la intersección de las firmas de los dos idiomas.

El teorema de Lyndon dice que si S ∪ T es insatisfactorio, entonces hay una oración de interpolación ρ 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 cada 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 cada símbolo de relación con una ocurrencia negativa en ρ tiene una ocurrencia negativa. ocurrencia en alguna fórmula de S y una ocurrencia positiva en alguna fórmula de T .

Prueba del teorema de interpolación de Craig

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

Teorema  :  si ⊨φ → ψ, entonces hay un ρ (el interpolante ) tal que ⊨φ → ρ y ⊨ρ → ψ, donde átomos (ρ) ⊆ átomos (φ) ∩ átomos (ψ). Aquí átomos (φ) es el conjunto de variables proposicionales que ocurren en φ, y ⊨ es la relación de vinculación semántica para la lógica proposicional.

Prueba

Supongamos ⊨φ → ψ. La prueba procede por inducción sobre el número de variables proposicionales que ocurren en φ y que no ocurren en ψ, denotadas | átomos (φ) − átomos (ψ)|.

Caso base | átomos (φ) − átomos (ψ)| = 0: Desde | átomos (φ) − átomos (ψ)| = 0, tenemos que átomos (φ) ⊆ átomos (φ) ∩ átomos (ψ). Además tenemos que ⊨φ → φ y ⊨φ → ψ. Esto basta para demostrar que φ es un interpolante adecuado en este caso.

Supongamos para el paso inductivo que el resultado se ha mostrado para todo χ donde | átomos (χ) − átomos (ψ)| = norte . Ahora supongamos que | átomos (φ) − átomos (ψ)| = norte +1. Elija q ∈ átomos (φ) pero q ∉ átomos (ψ). Ahora define:

φ' := φ[⊤/ q ] ∨ φ[⊥/ q ]

Aquí φ[⊤/ q ] es lo mismo que φ con cada aparición de q reemplazada por ⊤ y φ[⊥/ q ] reemplaza de manera similar q con ⊥. Podemos observar tres cosas de esta definición:

De ( 1 ), ( 2 ) y el paso inductivo tenemos que existe un interpolante ρ tal que:

Pero de ( 3 ) y ( 4 ) sabemos que

Por tanto, ρ es un interpolante adecuado para φ y ψ.

Dado que la prueba 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 conectivos lógicos que φ (consulte Notación O grande para obtener detalles sobre esta afirmación). Se pueden proporcionar pruebas 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 pruebas generalmente no son constructivas :

• Teóricamente del modelo , 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.
• Teóricamente demostrable , mediante un cálculo secuencial . Si la eliminación del corte es posible y, como resultado, se mantiene 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.

Aplicaciones

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 .

Referencias

1. Lyndon, Roger (1959), "Un teorema de interpolación en el cálculo de predicados", Pacific Journal of Mathematics , 9 : 129–142, doi : 10.2140/pjm.1959.9.129.
2. Troelstra, Anne Sjerp ; Schwichtenberg, Helmut (2000), Teoría básica de la prueba , tratados de Cambridge sobre informática teórica, vol. 43 (2ª ed.), Cambridge University Press, pág. 141, ISBN 978-0-521-77911-1.
3. Harrison págs. 426–427
4. Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Solucionadores de satisfacibilidad booleana y sus aplicaciones en la verificación de modelos". Actas del IEEE . 103 (11): 2021-2035. doi :10.1109/JPROC.2015.2455034. S2CID  10190144.

Otras lecturas

• 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ógica modal e intuicionista (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 de teoría de modelos . Tesis doctoral, Ámsterdam 2001.
• W. Craig, Tres usos del teorema de Herbrand-Gentzen al relacionar la teoría de modelos y la teoría de la prueba , The Journal of Symbolic Logic 22 (1957), no. 3, 269–285.