Cyclic Proofs for Theories of Truth

Abstract

Formal theories of truth aim to help us understand the notion of truth and its role in logic and mathematics. The field has come forth from Tarski’s effort to give a formal truth definition, and has since seen significant developments. One of the guiding theories on mathematical truth is Kripke’s semantic theory which partially models the truth predicate as a minimal fixed point. Kripke’s theory has motivated several axiomatic theories that capture this truth notion. Among them the most popular seems to be the theory Kripke- Feferman (KF). Investigations into the proof theory of KF have been ongoing and inform our understanding of the relation between truth and provability in mathematical logic. In this thesis we contribute to these investigations through the lens of cyclic proofs, a type of formal proof that allows for finite proof-theoretic representations of possibly infinite derivations through cyclic reasoning. This type of proof has received much attention in recent years due to its practical applicability, and has been analyzed in the context of several logical theories, but has not yet been applied to theories of truth. Therefore we bring together the streams of research by developing a cyclic proof system for the theory KF. We also demonstrate we are able to further expand this system into cyclic systems for μKF (a version of KF where truth and falsity are taken to be minimal fixed points), and νKF (which takes truth and falsity to be maximal fixed points). We show that all three systems are sound with respect to their semantic construction and that we can simulate inductive reasoning through cyclic rules in these systems.