A circular version of G\"odel's T and its abstraction complexity

TL;DR

This paper explores a circular variant of G"odel's system T, demonstrating that circular derivations can type primitive recursive functionals more succinctly and establishing a logical correspondence between the circular and standard systems.

Contribution

It introduces a circular version of G"odel's T, analyzes its type complexity, and establishes a formal correspondence with the traditional system, advancing understanding of circular proof systems.

Findings

Circular derivations type primitive recursive functionals more succinctly.

A logical correspondence between circular and standard G"odel's T systems is established.

Results on normalization, confluence, and models for circular derivations are obtained.

Abstract

Circular and non-wellfounded proofs have become an increasingly popular tool for metalogical treatments of systems with forms of induction and/or recursion. In this work we investigate the expressivity of a variant CT of G\"odel's system T where programs are circularly typed, rather than including an explicit recursion combinator. In particular, we examine the abstraction complexity (i.e. type level) of C, and show that the G\"odel primitive recursive functionals may be typed more succinctly with circular derivations, using types precisely one level lower than in T. In fact we give a logical correspondence between the two settings, interpreting the quantifier-free type 1 theory of level n+1 T into that of level n C and vice-versa. We also obtain some further results and perspectives on circular 'derivations', namely strong normalisation and confluence, models based on hereditary computable functionals, continuity at type 2, and a translation to terms of $\T$ computing the same functional, at all types.