Realizability for Peano arithmetic with winning conditions in HON games

Valentin Blot

Research output: Contribution to journalArticle

Abstract

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
Volume168
Issue number2
Early online date13 Oct 2016
DOIs
Publication statusPublished - 1 Feb 2017

Keywords

  • Classical realizability
  • Hyland Ong game semantics
  • Peano arithmetic

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

  • Projects

  • Cite this