Towards Automated Proof-Theoretic Semantics: Inference-Behaviour Semantics for 3-Dimensional K3 and LP

Resumen Técnico: Hacia la Semántica de la Prueba Automatizada: Semántica de Comportamiento-Inferencia para K3 y LP de 3 Dimensiones

Planteamiento del Problema
La automatización del razonamiento lógico está bien establecida (por ejemplo, mediante resolución, probadores de teoremas y asistentes interactivos como Rocq y Lean), pero la provisión automatizada de una semántica de la prueba teórica (P-tS) para dicho razonamiento sigue siendo un desafío abierto. Mientras que sistemas como MUltlog pueden generar automáticamente cálculos de secuentes, tablas de verdad y sistemas de deducción natural para arbitrarias lógicas de valores finitos a partir de tablas de verdad de modelos, carecen de la capacidad inversa: generar especificaciones de significado de la prueba teórica para los conectivas dentro de esos sistemas. Los enfoques de P-tS existentes, como la validez de la prueba teórica o la semántica de extensión de bases, suelen depender del cálculo, lo que impide la comparación del significado de las conectivas entre diferentes lógicas (por ejemplo, clásica vs. intuicionista). El artículo pretende integrar el enfoque de la Semántica de Comportamiento-Inferencia (I-bS) —que modela los significados de las conectivas mediante su comportamiento de inferencia mínimo— en el marco de MUltlog para automatizar la generación de P-tS para lógicas de valores múltiples.

Metodología
El artículo extiende el marco de I-bS, previamente limitado a cálculos de secuentes de 2 dimensiones, a cálculos de secuentes de n-dimensiones. La metodología procede a través de los siguientes pasos:

1. Aparato Formal: El autor define los secuentes de $n$-dimensiones como $n$-tuplas de multiconjuntos de fórmulas. Para interpretarlos sin recurrir a valores de verdad de modelos, adoptan una lectura multilateralista. Para los secuentes de 3 dimensiones (específicamente para la lógica de Strong Kleene, K3, y la Lógica de la Paradoja, LP), esto implica tres actos de habla: aserción (dimensión 1), suspensión del juicio (dimensión 2) y negación (dimensión 3).
2. Relación de Derivabilidad Mínima: Para aislar el significado de las conectivas de las características estructurales de una lógica específica, el autor define una relación de derivabilidad mínima que consiste en Identidad ($Id_3$) y una regla de Corte restringida ($Cut_2$). Esto evita los efectos de "confusión" de las reglas estructurales completas (como Contracción y Debilitamiento) presentes en los cálculos estándar.
3. Definibilidad y Comportamiento de Inferencia: Siguiendo una definición al estilo de Belnap, una conectiva se define si extiende de manera conservadora el cálculo base y es inter-derivable de forma única con una contraparte. La métrica central es el comportamiento de inferencia ($ib$), una función que rastrea las ubicaciones horizontales (dimensiones) y las aplicaciones de reglas de una conectiva durante su prueba de definibilidad.
4. Extensión de Significado: Para comparar conectivas a través de diferentes dimensionalidades (por ejemplo, 2D clásica vs. 3D paraconsistente), el artículo introduce la extensión de significado. Una conectiva de $m$-dimensiones extiende el significado de una conectiva de $n$-dimensiones ($m > n$) si el comportamiento de inferencia de esta última se preserva de manera conservadora dentro de un fragmento de $n$-dimensiones de la primera.

Contribuciones Clave y Resultados
El artículo aplica este marco extendido a dos lógicas de 3 valores: K3 y LP, utilizando los cálculos de secuentes de 3 dimensiones generados por MUltlog.

• Cláusulas Semánticas para K3/LP: El autor demuestra la unicidad y la conservatividad para las versiones multiplicativas y aditivas de las conectivas de K3 respecto a la relación mínima $\{Id_3, Cut_2\}$. Deriva cláusulas semánticas distintas para cada versión de las conectivas (por ejemplo, la conjunción multiplicativa $\otimes$ frente a la conjunción aditiva $\sqcap$), demostando que los cálculos estándar de K3 confluyen significados semánticamente distintos debido a sus reglas estructurales.
• Identidad de los Significados de K3 y LP: Un resultado central es que las conectivas de K3 y LP poseen significados idénticos. Aunque K3 y LP difieren en sus valores designados (K3 designa solo la dimensión 3; LP designa las dimensiones 2 y 3), sus propiedades de derivabilidad vertical y sus reglas operacionales son idénticas. Consecuentemente, sus comportamientos de inferencia en las pruebas de definibilidad son idénticos, produciendo las mismas cláusulas semánticas.
• Extensión de Significado de la Lógica Clásica: El artículo demuestra que las conectivas de 3 dimensiones de K3 y LP son extensiones de significado de sus contrapartes clásicas en LK (2-dimensional). Al proyectar las cláusulas semánticas de 3 dimensiones sobre la 1ª y 3ª dimensión (eliminando la 2ª dimensión), las reglas resultantes son sintácticamente idénticas a las cláusulas semánticas de las conectivas de la LK clásica. Esto confirma que las conectivas de K3/LP extienden de manera conservadora los significados clásicos sin alterarlos.
• Manejo de Reglas Estructurales: El análisis revela que las restricciones de contexto (por ejemplo, limitar el número de fórmulas en los componentes del secuente) son necesarias para mantener el comportamiento de inferencia mínimo. Sin estas restricciones, las reglas estructurales estándar (como la Contracción) alterarían el comportamiento de inferencia, cambiando efectivamente el significado de las conectivas.

Significancia y Reivindicaciones
El artículo afirma proporcionar el primer estudio de caso fundacional para extender I-bS a dimensiones mayores que dos. Su principal significancia radica en:

1. Comparación entre Cálculos: Establece un mecanismo para comparar los significados de las conectivas a través de lógicas de diferentes dimensionalidades, abordando una brecha en la literatura previa de P-tS que tenía dificultades para comparar lógicas con diferentes propiedades estructurales.
2. Validación del Pluralismo Lógico: El hallazgo de que K3 y LP comparten significados de conectivas idénticos respalda una visión de la semántica de la prueba del pluralismo lógico, donde diferentes lógicas pueden compartir los mismos significados de conectivas a pesar de tener diferentes valores designados o condiciones de validez.
3. Camino hacia la Automatización: Al mapear exitosamente los cálculos de 3 dimensiones a I-bS, el artículo sienta las bases para integrar I-bS en MUltlog. El objetivo final es automatizar la generación de cláusulas semánticas para cualquier lógica de valores finitos. El autor señala que, aunque el presente trabajo es un estudio de caso manual, el marco está diseñado para ser implementado computacionalmente, permitiendo potencialmente la generación automatizada de semántica de la prueba para arbitrarias lógicas de valores múltiples.

El autor mantiene la modestia respecto a la automatización inmediata de todo el proceso, reconociendo que generar las pruebas de definibilidad necesarias para arbitrarios cálculos de $n$-dimensiones sigue siendo un desafío computacional, aunque el marco teórico ya está establecido.