Cyclic Proofs, System T, and the Power of Contraction
summary
The paper studies a cyclic proof system C built over regular-expression types (inspired by linear logic and non-wellfounded proofs) and interprets C-proofs as strongly-typed goto programs. It proves that C denotes computable total functions and compares its expressive power with Gödel’s system T: in general C and T define the same functions on naturals, while the affine fragment of C (no contraction) corresponds exactly to the primitive recursive functions with a direct uniform encoding of C into T. The authors also obtain upper bounds by formalising weak normalization of a small-step reduction semantics in subsystems of second-order arithmetic (ACA0 and RCA0).
AI-written summary · about