Um modelo algébrico para a lógica proposicional da vizinhança

Abstract

Motivado pela falta de uma semântica algébrica bem estabelecida e com resultados de Adequação (Correção e Completude), este trabalho tem como objetivo desenvolver um modelo algébrico para uma lógica temporal intervalar no intuito de preencher esta lacuna deixada na literatura por autores que pavimentaram o caminho para sua algebrização. A lógica em questão faz parte da coleção de lógicas proposicionais da vizinhança proposta por Goranko, Montanari e Sciavicco. O sistema é precisamente o caso não-estrito dessa referida coleção de lógicas, a qual apresenta, como modelo algébrico sugerido na literatura, uma estrutura de semianel booleano munida de operadores de domínio e codomínio modais (que em nossa formalização adotará apenas o nome de álgebra da vizinhança). No entanto, no decorrer de nossos desenvolvimentos, embora o resultado de Correção seja possível, veremos que a ausência de determinados conectivos em sua linguagem original nos levará à falha em obter um resultado de Completude. Em vista disso, estendemos a lógica proposicional da vizinhança não-estrita até alcançarmos um sistema que, além de correto, seja completo em relação à estrutura algébrica proposta como modelo.

Motivated by the lack of a well-established algebraic semantics with results of adequacy, this work aims to develop an algebraic model for an interval temporal logic in order to fill the gap left in the literature by authors who paved the way for its algebraization. The logic in question is part of the collection of propositional neighbourhood logics proposed by Goranko, Montanari and Sciavicco. The system is precisely the non-strict case of that mentioned collection of logics, which presents, as an algebraic model suggested in the literature, a boolean semiring structure endowed with modal domain and codomain operators (which in our formalization we have adopted simply as the neighborhood algebra). However, in the course of our developments, although a Soundness result is possible, we will see that the absence of certain connectives in its original language lead us to fail in obtaining a Completeness result. In view of this, we extend the non-strict propositional neighbourhood logic until we reach a system that, in addition to being sound, is also complete with respect to the algebraic structure proposed as its model.