Provability as modality

• Grant number: 18/22896-0
• Support Opportunities: Scholarships in Brazil - Scientific Initiation
• Start date: February 01, 2019
• End date: December 31, 2019
• Field of knowledge: Humanities - Philosophy - Logic
• Principal Investigator: Giorgio Venturi
• Grantee: Felipe de Souza Albarelli
• Host Institution: Centro de Lógica, Epistemologia e História da Ciência (CLE). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brazil

Abstract

A formal system is a set of axioms and rules of inference that entails the derivation of theorems. Formal systems may be used to assert claims about many things and mathematical structures, like real numbers, geometric figures, and inferences. Some formal systems may even assert claims about formal systems since the latter is also mathematical structures or objects. A particular and surprising instance occurs when a formal system is able to assert claims about itself. For example, a system may not only be capable of proving P, but also be capable of proving that the system itself is able to prove P. The notorious Gödel's Incompleteness Theorems rise from this fact: these theorems impose limitations to what any formal system may be able to prove about itself. Gödel's Theorems and the logical tools that were used to prove them reveal fundamental facts about what is, in fact, a logical proof, since they impose limits to what may be proved (i.e., demonstrable) in a formal system. The formal theory that studies what formal systems are capable of proving is called 'provability logic'. Gödel's demonstration is an instance of provability logic. The operators that commonly appear in this logic are Ç and û, that hold the properties of being consistent and provable(i.e., demonstrable). These operators are dealt with by means of modal logic, as the likes of Kripke's models. This project has as its objective to study provability logic, as well its variations, in order to reach a deeper understanding of the notions of 'proof', 'consistency' and 'completeness' in a formal system, which are main concepts in the foundations of mathematics and in the philosophy of mathematics.