Game semantics for first-order logic

TL;DR

This paper refines game semantics with mu-pointers for first-order classical logic, providing completeness results and connecting to lambda-mu-calculus, Krivine's realizability, and type isomorphisms.

Contribution

It introduces mu-pointers into game semantics for first-order logic and extends the framework to classical logic with completeness, linking to lambda-mu-calculus and realizability.

Findings

Refined game semantics with mu-pointers for first-order logic

Extended semantics to classical logic with completeness

Explored relations with lambda-mu-calculus and type isomorphisms

Abstract

We refine HO/N game semantics with an additional notion of pointer (mu-pointers) and extend it to first-order classical logic with completeness results. We use a Church style extension of Parigot's lambda-mu-calculus to represent proofs of first-order classical logic. We present some relations with Krivine's classical realizability and applications to type isomorphisms.