Sesión Lógica y ComputabilidadInterpolación de Craig constructiva para QCiore
Victoria Arce Pistone
Universidad Nacional del Sur, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
La lógica paraconsistente de primer orden QCiore fue introducida por Coniglio, Gomez-Pereira y Figallo como una versión de primer orden de la lógica proposicional Ciore, preservando sus principales características y evitando ciertas relaciones no deseadas entre los cuantificadores. En un trabajo reciente, presentamos un cálculo de secuentes de primer orden para QCiore, denominado GQCiore, y probamos los correspondientes teoremas de correctitud, completitud y eliminación de corte. En esta charla mostraremos cómo este último resultado permite obtener una prueba constructiva del Teorema de Interpolación de Craig para QCiore. La demostración sigue el método de Maehara y constituye una aplicación directa de la propiedad de eliminación de corte del cálculo GQCiore.
Referencias
[1] Arce Pistone, V. A constructive proof of the Craig’s interpolation theorem for QCiore. Logic Journal of the IGPL, 33 (5), (2025). https://doi.org/10.1093/jigpal/jzaf068
[2] Arce Pistone, V. and Figallo, M. Proof-theoretic aspects of paraconsistency with strong consistency operator. Studia Logica (2025). https://doi.org/10.1007/s11225-023-10089-8
[3] Coniglio, M., Gomez-Pereira, G., and Figallo, M. Some model theoretic results on the 3-valued paraconsistent first-order logic QCiore. The Review of Symbolic Logic, 14(1), 187-224 (2021). 10.1017/S1755020319000595