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, de modo que cada símbolo no lógico en ρ ocurre tanto en φ y ψ, φ implica ρ y ρ implica ψ. El teorema fue probado 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 . Una forma más sólida del teorema de interpolación de Craig para la lógica de primer orden fue probada porRoger Lyndon en 1959; [1] [2] el resultado general a veces se denomina teorema de Craig-Lyndon .
Ejemplo
En lógica proposicional , dejemos
- .
Luego implica tautológicamente . Esto se puede verificar escribiendoen forma conjuntiva normal :
- .
Por tanto, si aguanta, entonces sostiene. En turno, implica tautológicamente . Debido a que las dos variables proposicionales que ocurren en ocurrir en ambos y , esto significa que es un interpolador para la implicación .
Teorema de interpolación de Lyndon
Suponga 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 el más pequeño que contiene las firmas de S y T . También sea 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 insaciable, entonces hay una frase ρ interpolación en el lenguaje de S ∩ T que es cierto en todos los modelos de S y falso en todos los modelos de camiseta . 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 positivo 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 la lógica proposicional . [3] Formalmente, el teorema establece:
Si ⊨φ → ψ entonces hay un ρ (el interpolante ) tal que ⊨φ → ρ y ⊨ρ → ψ, donde átomos (ρ) ⊆ átomos (φ) ∩ átomos (ψ). Aquí los átomos (φ) es el conjunto de variables proposicionales que ocurren en φ, y ⊨ es la relación de implicación semántica para la lógica proposicional.
Prueba. Suponga ⊨φ → ψ. La demostración procede por inducción sobre el número de variables proposicionales que ocurren en φ 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 es suficiente para mostrar que φ es un interpolante adecuado en este caso.
Supongamos para el paso inductivo que se ha mostrado el resultado para todo χ donde | átomos (χ) - átomos (ψ) | = n. Ahora suponga que | átomos (φ) - átomos (ψ) | = n + 1. Elija q ∈ átomos (φ) pero q ∉ átomos (ψ). Ahora defina:
φ ': = φ [⊤ / 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:
- ⊨φ '→ ψ
( 1 )
- | átomos (φ ') - átomos (ψ) | = n
( 2 )
- ⊨φ → φ '
( 3 )
De ( 1 ), ( 2 ) y el paso inductivo tenemos que hay un interpolante ρ tal que:
- ⊨φ '→ ρ
( 4 )
- ⊨ρ → ψ
( 5 )
Pero de ( 3 ) y ( 4 ) sabemos que
- ⊨φ → ρ
( 6 )
Por tanto, ρ es un interpolante adecuado para φ y ψ.
QED
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 conectivas lógicas que φ (consulte la notación Big O 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 se puede probar con otros métodos. Sin embargo, estas pruebas generalmente no son constructivas :
- en teoría 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.
- prueba-teóricamente , a través de un cálculo secuencial . Si la eliminación de cortes es posible y, como resultado, la propiedad de la subfórmula se mantiene, entonces la interpolación de Craig se puede demostrar mediante inducción sobre las derivaciones.
- algebraicamente , usando teoremas de amalgama para la variedad de álgebras que representan la lógica.
- a través de la traducción a otras lógicas disfrutando de la interpolación de Craig.
Aplicaciones
Craig interpolación tiene muchas aplicaciones, entre ellas las pruebas de consistencia , la verificación de modelos , [4] pruebas en modulares especificaciones , modulares ontologías .
Referencias
- ^ Lyndon, Roger, "Un teorema de interpolación en el cálculo de predicados", Pacific Journal of Mathematics , 9 : 129-142.
- ^ Troelstra, Anne Sjerp ; Schwichtenberg, Helmut (2000), Teoría básica de la prueba , tratados de Cambridge sobre informática teórica, 43 (2ª ed.), Cambridge University Press, p. 141, ISBN 978-0-521-77911-1.
- ^ Harrison págs. 426–427
- ^ Vizel, Y .; Weissenbacher, G .; Malik, S. (2015). "Solucionadores de satisfacción booleana y sus aplicaciones en la comprobación de modelos". Actas del IEEE . 103 (11). doi : 10.1109 / JPROC.2015.2455034 .
Otras lecturas
- John Harrison (2009). Manual de lógica práctica y razonamiento automatizado . Cambridge, Nueva York: Cambridge University Press . ISBN 0-521-89957-5.
- 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 lógicas 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, Amsterdam 2001.
- W. Craig, Tres usos del teorema de Herbrand-Gentzen para relacionar la teoría de modelos y la teoría de la prueba , The Journal of Symbolic Logic 22 (1957), no. 3, 269-285.