¿Hay alguna semántica categórica para las lógicas no monotónicas?
Parece que la respuesta simple a esto es "No" ya que la noción obvia de composición falla para cualquier modelo de lógica no monotónica. Pero, ¿hay un modelo que realmente funcione con una noción de composición adecuadamente definida?
ct.category-theory
semantics
denotational-semantics
David Boshton
fuente
fuente
Respuestas:
La lógica no monotónica es una especie de área amplia: ¿tiene alguna lógica particular en mente? De todos modos, asumiendo derrotado :) que
Una respuesta es que puede dar una semántica categórica razonable a cualquier lógica para la que se conozca un cálculo posterior con eliminación de cortes. Básicamente, los tipos son objetos, las formas normales del cálculo posterior son morfismos, y la eliminación de cortes le indica cómo implementar la composición. Esto le da la categoría inicial en cualquier categoría de modelos que termine usando para demostrar solidez e integridad.
A B A B A X BA⊸B A B A B A X B ) Sin embargo, tiene una excelente teoría de prueba, y sus modelos categóricos están estrechamente vinculados a la teoría de las categorías monoidales.
fuente
[Mis disculpas por escribir esto como respuesta, a pesar de que es básicamente un comentario a la respuesta anterior. Pero no se me permite publicar un comentario allí, ya que no tengo suficiente "reputación"]
La respuesta anterior no es correcta. La lógica lineal (así como cualquiera de sus sistemas subestructurales: MLL, MALL, MELL, ALL, lo que quieras ...) es perfectamente monótono .
La respuesta de Neel confunde "relevancia" y "no monotonicidad".
La relevancia puede verse como no monotonicidad del conector de inferencia del sistema . Lógica lineal es pertinente, en que la demostrabilidad de no implica la demostrabilidad de . La relevancia es una especie de no monotonicidad interna de la lógica.⊢ X ⊗ A ⊸ B⊢A⊸B ⊢X⊗A⊸B
Por otro lado, lo que las personas llaman lógicas no monótonas son sistemas en los que la demostrabilidad del sistema no es monótona: agregar un nuevo elemento al conjunto de fórmulas cambia el conjunto de fórmulas comprobables. Es una forma de metano -monotonicidad, porque concierne a la demostrabilidad y no al conector de inferencia. La lógica lineal es monótona: puede agregar lo que desee al conjunto de fórmulas y cualquier nueva regla de inferencia o axioma al sistema, pero si tenía una prueba del secuenciante antes, lo hará todavía lo tengo ahora, porque no has cambiado las otras reglas de inferencia del cálculo posterior.Γ⊢M:A
Por lo que sé, las lógicas no reales (monótonas) son difíciles de dejar en una forma de cálculo posterior que disfruta de la eliminación de cortes, o cualquier otro tipo de sistema de prueba con una noción equivalente de terminar la reducción de la prueba. Esta es la razón por la cual los enfoques semánticos categóricos tradicionales difícilmente funcionarían para ellos.
fuente