Modal Reduction Principles across Relational Semantics

Abstract

Sahlqvist theory is an important result in the model theory of modal logic, since it identifies a class of formulas which have effectively computable first order correspondents. Recently, this theory has been generalised to a larger set of logics by using their algebraic semantics. This fact has allowed researchers to define inequalities of formulas and to determine under which conditions these inequalities have effectively computable first order correspondents, that is, under which conditions they are Sahlqvist inequalities. Actually, there are algorithms that compute first order correspondents of these inequalities, such as ALBA algorithm. This algorithm translates any Sahlqvist inequality to a first order formula, but this translation still strongly depends on semantics. In this thesis, it is proposed a methodology to obtain first order correspondents of certain inequalities, called modal reduction principles, which are easily comparable across two relational semantics: crisp and many-valued polarity-based semantics. Concretely, this thesis presents an introduction to Sahlqvist theory and polarity-based semantics and proves that the first order correspondents of modal reduction principles are pure inclusion of binary relations on both semantics.

La teoría de Sahlqvist es un importante resultado de la teoría de modelos de la lógica modal, ya que identifica una clase de fórmulas que tienen un correspondiente de primer order efectivamente computable. Esta teoría ha sido recientemente generalizada a un mayor conjunto de lógicas gracias a considerar la semántica algebraica de la lógica modal. Esto ha permitido definir desigualdades de fórmulas y establecer bajo qué condiciones se puede asegurar que tienen un correspondiente de primer order efectivamente computable, es decir, bajo qué condiciones son desigualdades de Sahlqvist. De hecho, se han definido algoritmos con este objetivo, como por ejemplo el algoritmo ALBA. Este algoritmo traduce cualquier desigualdad de Sahlqvist a una fórmula de primer orden, pero esta traducción todavía depende fuertemente de la semántica considerada. En este trabajo de fin de máster, se propone una metodología para obtener correspondientes de primer order de cierto tipo de desigualdades, llamadas principios de reducción modal, que sean fácilmente comparables entre sí al interpretarlas con dos semánticas relacionales distintas: la semántica de polaridad bi-valuada y multi-valuada. Concretamente, este trabajo presenta una introducción a la teoría de Sahlqvist y a la semántica de polaridad y demuestra que los correspondientes de primer orden de estas desigualdades son inclusiones de relaciones binarias en ambas semánticas.