Realizability for Peano arithmetic with winning conditions in HON games (Q345704)

Hyland-Ong-Nickau games are used to provide semantics for programming languages. In HON games, plays are interaction traces between a program (player \(P\)), and an environment (opponent \(O\)); a program is interpreted by a strategy for \(P\) which represents the interactions it can have with the environment. In the paper under review, the author presents a classical realizability semantics based on HON games, using winning conditions on desequentialized plays. The realizability relation builds on an interpretation of the \(\lambda\mu\)-calculus in a coproduct completion of the Cartesian-closed category of single-threaded strategies. It is shown that the realizability relation provides sound semantics for classical first-order logic and, further employing a relativization predicate, for Peano arithmetic.