Towards an algebrization of a linear temporal logic

Abstract

The subject of this paper is the Propositional Neighbourhood Logic (PNL), a case of linear temporal logic and an extension of Classical Propositional Logic that results from the inclusion of modal operators that deal with certain temporal aspects. In this context, the validity of a proposition is strictly related to some temporal interval. We highlight some formal aspects of this logic and its formalization in some deductive systems (or proof systems), which naturally reflect the formal aspects of time. We aim to investigate algebraic models for Propositional Neighbourhood Logic. However, in this work, we focus exclusively on presenting the Soundness result, one of the necessary steps towards obtaining an adequate (sound and complete) model, between the axiomatic system of PNL and the planned algebraic model.