Sesión Lógica y ComputabilidadTeoría de prueba en el contexto de paraconsistencia con operador de consistencia fuerte
Martín Figallo
Universidad Nacional del Sur, Departamento de Matemática, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
El enfoque de Newton da Costa a la paraconsistencia, hoy globalmente conocida como ''Escuela Brasileña de Paraconsistencia'', fue generalizado de modo natural por W. Carnielli y J. Marcos con la noción de Lógicas de la Inconsistencia Formal (LFI). Estas son lógicas paraconsistentes que internalizan las nociones de consistencia e inconsistencia a nivel del lenguaje objeto.
Por otro lado, A. Avron, B. Konikowska y A. Zamansky ([2]) estudiaron de forma sistemática y modular la teoría de prueba de una familia grande de LFIs. Más precisamente, presentaron cálculos de secuentes con la propiedad de eliminación de corte para las versiones proposicionales de estas lógicas. Sin embargo, como estos mismos autores observaron, para desarrollar herramientas eficientes que permitan el razonamiento automatizado bajo incertidumbre (theorem provers) es importante desarrollar la teoría de prueba de las versiones de primer orden de estas LFIs.
En esta comunicación, damos un primer paso en este sentido. Esto es, estudiamos la teoría de prueba de la versión de primer orden de una LFI 3-valorada con operador de consistencia fuerte, que fuera desarrollada en el contexto del estudio de bases de datos inconsistentes ([3]). Entre otras cosas, presentaremos un cálculo de secuentes correcto y completo con la propiedad de eliminación de corte; y mostraremos algunas aplicaciones.
Trabajo en conjunto con: Victoria Arce Pistone (Universidad Nacional del Sur, Bahía Blanca, Argentina).
Referencias
[1] Arce Pistone, V. and Figallo, M. (2023). Proof-theoretic aspects of paraconsistency with strong consistency operator. http://arxiv.org/abs/2304.11481
[2] Avron, A., Konikowska, B. and Zamansky, A. (2012). Modular Construction of Cut-Free Sequent Calculi for Paraconsistent Logics. Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, 85–94
[3] Carnielli, W. A., Marcos, J. and de Amo, S. (2000). Formal inconsistency and evolutionary databases. Logic and Logical Philosophy, 8, 115–152.