Emanuele Frittaion (University of Leeds)

Peano arithmetic, games, and descent recursion

I will discuss a game semantics for classical (first-order) arithmetic due to Coquand. The real content of this semantics is a proof of cut elimination for infinitary propositional logic. As the title suggests, I will say something about descent recursive functions and how it all comes together.