Realizability for Peano arithmetic with winning conditions in HON games

Valentin Blot

Research output: Contribution to journalArticlepeer-review

1 Citation (SciVal)


We build a realizability model for Peano arithmetic based on winning conditions for HON games. Our winning conditions are sets of desequentialized interactions which we call positions. We define a notion of winning strategies on arenas equipped with winning conditions. We prove that the interpretation of a classical proof of a formula is a winning strategy on the arena with winning condition corresponding to the formula. Finally we apply this to Peano arithmetic with relativized quantifications and give the example of witness extraction for Π2 0-formulas.

Original languageEnglish
Pages (from-to)254-277
Number of pages24
JournalAnnals of Pure and Applied Logic
Issue number2
Early online date13 Oct 2016
Publication statusPublished - 1 Feb 2017


  • Classical realizability
  • Hyland Ong game semantics
  • Peano arithmetic


Dive into the research topics of 'Realizability for Peano arithmetic with winning conditions in HON games'. Together they form a unique fingerprint.

Cite this