Existe alguma semântica categórica para lógicas não monotônicas?
Parece que a resposta simples para isso é "Não", pois a noção óbvia de composição falha em qualquer modelo de lógica não monotônica. Mas existe um modelo que realmente funcione com uma noção de composição adequadamente definida?
ct.category-theory
semantics
denotational-semantics
David Boshton
fonte
fonte
Respostas:
A lógica não monotônica é uma área ampla - você tem alguma lógica específica em mente? De qualquer forma, supondo que :) que
Uma resposta é que você pode fornecer uma semântica categórica razoável para qualquer lógica pela qual um cálculo sequencial com eliminação de corte seja conhecido. Basicamente, os tipos são objetos, as formas normais do cálculo sequencial são morfismos e a eliminação de cortes informa como implementar a composição. Isso fornece a categoria inicial em qualquer categoria de modelo que você usar para provar a integridade e a integridade.
fonte
[Minhas desculpas por escrever isso como resposta, apesar de ser basicamente apenas um comentário à resposta anterior. Mas não tenho permissão para postar um comentário lá em cima, pois não tenho "reputação" suficiente]
A resposta anterior não está correta. A lógica linear (assim como qualquer um de seus sistemas subestruturais: MLL, MALL, MELL, ALL, o que você quiser ...) é perfeitamente monótona .
A resposta de Neel confunde "relevância" e "não monotonicidade".
A relevância pode ser vista como não monotonicidade do conector de inferência do sistema . A lógica linear é relevante, na medida em que a possibilidade de⊢A⊸B ⊢X⊗A⊸B
Por outro lado, o que as pessoas chamam de lógica não monotônica são sistemas em que a provabilidade do sistema não é monótona: adicionar um novo elemento ao conjunto de fórmulas altera o conjunto de fórmulas prováveis. É uma forma de meta não monotonicidade, porque diz respeito à provabilidade e não ao conector de inferência. A lógica linear é monótona: você pode adicionar o que quiser ao conjunto de fórmulas e qualquer novo axioma ou regra de inferência ao sistema, mas se você tiver uma prova do sequenteΓ⊢M:A
Até onde eu sei, é difícil definir lógicas não-monotônicas (reais) em uma forma de cálculo sequencial, com eliminação de corte ou qualquer outro tipo de sistema de prova com uma noção equivalente de terminar a redução de prova. É por isso que as abordagens semânticas categóricas da tradição dificilmente funcionariam para elas.
fonte