Michele Basaldella, An interactive semantics for classical arithmethic



In this talk, we present a semantics of derivations for an infinitary logic introduced by Novikoff and later refined by Coquand and Herbelin. The language of this logic consists of infinitary propositional formulas, and the proof-system for this language is given by a sequent calculus with infinitary rules of inferences. First-order classical arithmetic can be naturally embedded in this logic. The semantics of derivations we develop in this paper is strongly inspired by Girard’s ludics. The main result of this paper is a soundness-and-completeness theorem for derivations in the infinitary logic with respect to this kind of semantics.