On the logical strength of confluence and normalisation for cyclic proofs

authors: Anupam Das
year: 2021
url: https://drops.dagstuhl.de/storage/00lipics/lipics-vol195-fscd2021/LIPIcs.FSCD.2021.29/LIPIcs.FSCD.2021.29.pdf
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
abstract: In this work we address the logical strength of confluence and normalisation for non-wellfounded typing derivations, in the tradition of “cyclic proof theory”. We present a circular version CT of Gödel's system T, with the aim of comparing the relative expressivity of the theories CT and T. We approach this problem by formalising rewriting-theoretic results such as confluence and normalisation for the underlying “coterm” rewriting system of CT within fragments of second-order arithmetic. We establish confluence of CT within the theory RCA₀, a conservative extension of primitive recursive arithmetic and IΣ1. This allows us to recast type structures of hereditarily recursive operations as “coterm” models of T. We show that these also form models of CT, by formalising a totality argument for circular typing derivations within suitable fragments of second-order arithmetic. Relying on well-known proof mining results, we thus obtain an interpretation of CT into T; in fact, more precisely, we interpret level-n-CT into level-(n+1)-T, an optimum result in terms of abstraction complexity. A direct consequence of these model-theoretic results is weak normalisation for CT. As further results, we also show strong normalisation for CT and continuity of functionals computed by its type 2 coterms.