At the turn of the 20th century there was a revolution in logic. New technologies, associated with the names of Frege and Russell, radically changed philosophy, because formal logic lends incredible precision to the asking and answering of old questions. A discipline called foundations of mathematics emerged, casting new light on the nature and meaning of rationality and mathematical truth. In foundational research, philosophical issues and mathematical results develop in tandem, each informing the other. Epochal results came out of early investigations, such as the modern theory of computing as developed by Gödel, Turing and Church.
The goal of the initial foundational project, as articulated by Hilbert (reviving an idea of Leibniz’s), was a method for reliably deciding whether or not a given sentence is true. All approaches to foundations of the last hundred years, from Russell’s to Hilbert’s to Brouwer’s, are beholden to formal consistency. Beset on one side by serious paradoxes, like Russell’s contradiction, and on the other by Gödel’s incompleteness theorems, it is now known that a consistent foundation is impossible to obtain.
Starting in the 1970s, developments in logic produced a novel kind of tool, paraconsistent logic. These logics accommodate inconsistency in a sensible fashion. From the start, many logicians saw the relevance and possible applications of these logics to foundational matters. Techniques have now developed to a level of sophistication where it is possible to renew a serious investigation of foundations. The driving thought here is that one need not founder on the paradoxes that halted older foundational projects. One simply recasts, accepts and even studies some contradictions, controlling any pernicious effects with a paraconsistent logic.
Our project is to construct, for the first time, a fully articulated foundation for mathematics. This will involve the construction of paraconsistent versions of the major pillars of foundational studies:
• Foundations are tested on arithmetic, the basic tool for counting and quantity. The functions that operate over the numbers are the province of recursion theory, which ties into computation.
• The bridge between language and mathematical structures is provided by model theory, which has become an indispensable tool for philosophers and logicians alike. Consistent model theory is not able to take in the full range of what mathematicians express in language. A model theory built on paraconsistent principles will be radically more powerful and illuminating, a major achievement.
• Conducting foundational studies of proof and truth in their natural setting contributes to our understanding of knowledge and beliefs, by providing a simple and credible account of learning.
What will emerge is a wholly new perspective on the nature of mathematical thought and truth, striking results in inconsistent mathematics itself, and a reliable platform for more general theories that no strictly consistent foundation can support.
Formally, we define and describe the objects of mathematics, such as numbers and functions; we prove that there are such objects and that they have the right properties; and we do this in such a way as to allow for some inevitable inconsistencies, using paraconsistency to protect the basic integrity of the theory. Philosophically, we work from that foundation to understand truth, proof and belief in terms of what they are—rational but paradoxical ways that humans navigate through our world.
