Peano Arithmetic, games and descent recursion

TL;DR

This paper provides a new implementation of Coquand's game semantics for Peano Arithmetic, using descent recursion to describe winning strategies and offering insights into provably recursive functions.

Contribution

It introduces a descent recursive approach to Coquand's game semantics, enabling direct descriptions of winning strategies and new proofs of properties of provably recursive functions.

Findings

Descent recursive functions can describe winning strategies in game semantics.

A direct implementation of cut elimination proof via descent recursion.

New proofs of properties of provably recursive functions.

Abstract

We analyze Coquand's game-theoretic interpretation of Peano Arithmetic through the lens of elementary descent recursion. In Coquand's game semantics, winning strategies correspond to infinitary cut-free proofs and cut elimination corresponds to debates between these winning strategies. The proof of cut elimination, i.e., the proof that such debates eventually terminate, is by transfinite induction on certain interaction sequences of ordinals. In this paper, we provide a direct implementation of Coquand's proof, one that allows us to describe winning strategies by descent recursive functions. As a byproduct, we obtain yet another proof of well-known results about provably recursive functions and functionals.