UMA 2022
La lógica proposicional paraconsistente {\bf Ciore} fue desarrollada por Carnielli, Marcos y de Amo en el contexto del estudio de bases de datos inconsistentes. Esta lógica tiene características muy particulares como la propagación y retropropagación del operador de consistencia, además, es algebrizable en el sentido de Blok y Pigozzi. Un estudio detallado de la versión de primer orden de {\bf Ciore}, {\bf QCiore}, puede encontrarse en [3]. En [1], presentamos un cálculo de secuentes libre de corte, {\bf ${\cal G}$Ciore}, correcto y completo con respecto a {\bf Ciore}, aplicando el método general desarrollado en [2].
En esta oportunidad, continuamos con el estudio iniciado en [1]. En primer lugar, introducimos la noción de {\em subfórmula generalizada} para {\bf Ciore} y probamos que {\bf ${\cal G}$Ciore} goza de la Propiedad de la Subfórmula Generalizada. Esto es, toda prueba libre de corte en {\bf ${\cal G}$Ciore} tiene la propiedad que todas las fórmulas que intervienen en cualquier secuente de la prueba, son subfórmulas generalizadas de fórmulas en el secuente final de la prueba. Como consecuencia de esto, establecemos un proceso de desición para {\bf ${\cal G}$Ciore}, permitiendonos concluir que la lógica {\bf Ciore} es decidible. Otra consecuencia interesante del Teorema de Eliminación de Corte, es que, si bien {\bf Ciore} es una lógica paraconsistente (y, por lo tanto, no necesariamente explota ante una contradicción), en {\bf ${\cal G}$Ciore} ninguna contradicción es demostrable.\\ Finalmente, extendemos {\bf ${\cal G}$Ciore} a un cálculo de secuentes de primer orden {\bf ${\cal G}$QCiore} encontrando las reglas que regulan el comportamiento de los cuantificadores y su interacción con el operador de consistencia. Probamos el correspondiente Teorema de Correctitud y, aplicando la técnica de Sch\"utte, probamos los teoremas de Completitud y Eliminación de Corte.
Trabajo en conjunto con: Martín Figallo (Universidad Nacional del Sur, Argentina).
Referencias
[1] V. Arce Pistone, & M. Figallo. Cálculo de secuentes con eliminación de corte para una lógica paraconsistente. Libro de resumenes de la LXX Reunión de Comunicaciones Científicas, virtUMA 2021.
[2] Avron, A., Ben-Naim, J. & Konikowska, B. (2007). Cut-Free Ordinary Sequent Calculi for Logics Having Generalized Finite-Valued Semantics. Log. univers. 1, 41–70.
[3] Coniglio, M., Gomez-Pereira, G., & Figallo, M. (2021). Some model theoretic results on the 3-valued paraconsistent first-order logic QCiore. The Review of Symbolic Logic, 14(1), 187-224.