A sequent calculus for the three-valued and intuitionistic logic I1

• Grant number: 19/15963-5
• Support Opportunities: Scholarships in Brazil - Scientific Initiation
• Start date: December 01, 2019
• End date: January 31, 2021
• Field of knowledge: Humanities - Philosophy - Logic
• Principal Investigator: Luiz Henrique da Cruz Silvestrini
• Grantee: Elias Oliveira Vieira dos Santos
• Host Institution: Faculdade de Ciências (FC). Universidade Estadual Paulista (UNESP). Campus de Bauru. Bauru , SP, Brazil

Abstract

The calculus I1 was introduced in 1995 by Sette and Carnielli. This system has an intuitionistic character, in the same sense as the logical system developed by Arend Heyting (1898-1980), which emerged as the underlying logic of Intuitionistic Mathematics, or constructive, by Luitzen Egbertus Jan Brouwer (1881-1966). Furthermore, the calculus I1 is a three-valued logic that, contrary to classical logic, does not admit only two truth values, but three, these are T, F* and F. The values T and F denote, respectively, truth and falsity, whereas F* can be interpreted as "falsity by lack of positive evidence". Santos and Silvestrini (2018) introduced the logic I1 in a tableaux system, denoted by TI1; which presented closing clauses and rules for the construction of such a system and discussing its benefits in relation to the axiomatic method. The aim of this scientific initiation project is to develop an alternative deductive method to the axiomatic for intuitionistic logic I1, then, we intend to develop a system of sequent calculi for such logic and discuss the benefits of this method of deduction in relation to the axiomatic method, comparing the logic I1 in systems, namely, axiomatic, analytic tableaux and sequent calculus, arguing about the benefits of such alternative deductive methods and your applications.