El teorema de eliminación de corte para la lógica modal GL. Una demostración no mecanizada.

Ponente(s): Ricardo Jaimes Urbán, Favio E. Miranda Perea

En 2015 Brighton demostró el teorema de eliminación de corte para la lógica modal GL utilizando árboles de regresión. En 2021 Goré, Ramanayake y Shillito mostraron que la demostración de Brighton es incorrecta, por lo que dieron una demostración asistida por computadora (DAC) utilizando el asistente de pruebas COQ. A pesar de que las DAC se han vuelto populares en los últimos años, aún no son universalmente aceptadas. Por este motivo, se planteó dar una prueba tradicional, basada en la DAC presentada en 2021. Sin embargo, debido a las constantes actualizaciones de COQ, fue imposible revisar la demostración con la versión actual. Por este motivo, se optó por dar una prueba basada en los bosquejos dados por los autores, demostrando todos los resultados que se presentan sin demostrarse, apelando a la DAC, y omitiendo las desviaciones necesarias para facilitar la implementación. De este modo, obtuvimos una prueba más directa y robusta que puede ser leída por un público más general. El éxito de este enfoque muestra que, en este caso, la DAC es confiable desde un punto de vista tradicional. Este trabajo se desarrolló con apoyo del proyecto PAPIIT DGAPA UNAM IN101723.