An arithmetical proof of the strong normalization for the $\lambda$-calculus with recursive equations on types

TL;DR

This paper provides an arithmetical proof that the lambda calculus with recursive type equations is strongly normalizing, demonstrating that the proof's logical strength is within Peano arithmetic.

Contribution

It introduces an arithmetical proof of strong normalization for lambda calculus with recursive types, extending previous proofs without equations and establishing its formalization within Peano arithmetic.

Findings

Proof extends to lambda calculus with recursive equations

Strength of the proof system is within Peano arithmetic

Demonstrates formalizability of the proof in Peano arithmetic

Abstract

We give an arithmetical proof of the strong normalization of the $\lambda$-calculus (and also of the $\lambda\mu$-calculus) where the type system is the one of simple types with recursive equations on types. The proof using candidates of reducibility is an easy extension of the one without equations but this proof cannot be formalized in Peano arithmetic. The strength of the system needed for such a proof was not known. Our proof shows that it is not more than Peano arithmetic.