Taming Jörmungandr: The Logical Foundations of Circularity
Short description
The project is devoted to developing new techniques for the formal analysis of cyclic phenomena in mathematical, philosophical and computational contexts. Although a variety of formalisms will be employed, the concept of cyclic and ill-founded proofs will play an important role. Cyclic proofs are formal arguments/deductions following the local constraints of a given calculus but where possibly infinite deduction trees are allowed provided they exhibit uniformity and satisfy a decidable correctness criterion. Informal examples of cyclic proofs are the irrationality of √2 by the method of infinite descent and Fermat’s ‘Last Theorem’ for the fourth power.
Cyclic proofs offer a novel perspective to our understanding of provability not present in traditional notions of proof. They represent the dynamic aspect of provability: verifications of non-terminating processes and winning strategies in infinite games. Logico-linguistic concepts characterised by self-reference, including temporality and truth, can be associated cyclic forms of proof, providing a formal foundation for their analysis. Computer algorithms can be designed to search for cycles in reasoning, furnishing algorithms for automated proof-search and the certification of safety critical systems.
This research project aims to develop a unified framework for the study of circularity in theory and applications with particular focus on three agendas:
Uniform methods for representing and analysing calculi of cyclic and ill-founded derivations, including general arguments of correctness, notions of normal form and translations to/from finitary proofs.
Deepening our understanding of truth and ontology in mathematics, particularly in relation to notions of provability, justification and verification.
Formal characterisations of similarity and equivalence underpinning modern advancements in mathematics, philosophy and computer science.