Nino Guallart

En este artículo, presentamos un sistema de lógica modal que permite representar relaciones entre conjuntos o clases de individuos definidos por una propiedad específica. Introducimos dos operadores modales, [a] y, que se utilizan respectivamente para expresar "para todo A" y "existe un A". Tanto la sintaxis como la semántica del sistema tienen dos niveles que evitan el anidamiento del operador modal. La semántica se basa en una variante de la semántica de Kripke, en donde los operadores modales se indexan sobre fórmulas de lógica proposicional (“pre-fórmulas” en el trabajo). Además, presentamos un conjunto de axiomas y reglas que rigen el sistema, y demostramos que el sistema es correcto y completo con relación a los modelos de Kripke. En la sección final del artículo, discutimos posibles trabajos futuros. Consideramos la posibilidad de combinar nuestro operador modal con otras modalidades, como necesidad o conocimiento. Además, como ejemplo de la utilidad de nuestro operador modal, analizamos brevemente la fórmula de Barcan adaptada de manera conveniente dentro del marco de nuestro sistema. En resumen, proponemos la combinación de nuestro operador modal con otros como una forma más simple y compacta, aunque con un menor poder expresivo, para abordar la lógica modal cuantificada.

In this article, we present a modal logic system that allows representing relationships between sets or classes of individuals defined by a specific property. We introduce two modal operators, [a] and <a>, which are used respectively to express "for all A" and "there exists an A". Both the syntax and semantics of the system have two levels that avoid the nesting of the modal operator. The semantics is based on a variant of Kripke semantics, where the modal operators are indexed over propositional logic formulas ("pre-formulas" in the paper). Furthermore, we present a set of axioms and rules that govern the system and we prove that the logic is correct and complete with respect to Kripke models. In the final section of the article, we discuss potential future work. We consider the possibility of combining our operator with other modalities, such as necessity or knowledge. Additionally, as an example of the utility of our modal operator, we briefly analyze a conveniently adapted Barcan formula within the framework of our system. In summary, we propose combining our modal operator with other ones as a simpler, more compact, albeit less expressive way to address quantified modal logic.

Pure type systems arise as a generalisation of simply typed lambda calculus. The contemporary development of mathematics has renewed the interest in type theories, as they are not just the object of mere historical research, but have an active role in the development of computational science and core mathematics. It is worth exploring some of them in depth, particularly predicative Martin-Löf’s intuitionistic type theory and impredicative Coquand’s calculus of constructions. The logical and philosophical differences and similarities between them will be studied, showing the relationship between these type theories and other fields of logic.