Modal Ecumenism through RNmatrices: Theory, Implementation, and Verification

• Grant number: 23/16021-9
• Support Opportunities: Scholarships abroad - Research Internship - Doctorate
• Start date: June 20, 2024
• End date: June 19, 2025
• Field of knowledge: Humanities - Philosophy - Logic
• Principal Investigator: Marcelo Esteban Coniglio
• Grantee: Renato Reis Leme
• Supervisor: Carlos Olarte
• Host Institution: Instituto de Filosofia e Ciências Humanas (IFCH). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brazil
• Institution abroad: Laboratoire D'Informatique De Paris Nord, France
• Associated to the scholarship: 21/01025-3 - Genericity in the context of theorem proving: a cloud based proof assistant for flow-based languages, BP.DR

Abstract

Ecumenical modal logic offers a philosophically grounded alternative to the search for harmony between classical and intuitionistic modal logic. RNmatrices, in turn, are non-deterministic algebraic structures that have shown promise for characterizing logics that do not admit traditional finite matrix semantics, as is the case of ecumenical logic. The main objective of this project is to obtain new semantics for ecumenical modal logic through RNmatrices. To achieve this, we propose to develop the work on three fronts: theory, implementation, and verification. In the end, we hope to have obtained, as by-products, new proof systems implemented in software for propositional and first-order ecumenical modal logic.