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

Fingerprint

Peano Arithmetic
Realizability
Game
Quantification
Interaction
Strategy

Keywords

  • Classical realizability
  • Hyland Ong game semantics
  • Peano arithmetic

Cite this

Realizability for Peano arithmetic with winning conditions in HON games. / Blot, Valentin.

In: Annals of Pure and Applied Logic, Vol. 168, No. 2, 01.02.2017, p. 254-277.

Research output: Contribution to journalArticle

@article{c80714c5e3754d72af52f6f8e53aa97f,
title = "Realizability for Peano arithmetic with winning conditions in HON games",
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.",
keywords = "Classical realizability, Hyland Ong game semantics, Peano arithmetic",
author = "Valentin Blot",
year = "2017",
month = "2",
day = "1",
doi = "10.1016/j.apal.2016.10.006",
language = "English",
volume = "168",
pages = "254--277",
journal = "Annals of Pure and Applied Logic",
issn = "0168-0072",
publisher = "Elsevier",
number = "2",

}

TY - JOUR

T1 - Realizability for Peano arithmetic with winning conditions in HON games

AU - Blot, Valentin

PY - 2017/2/1

Y1 - 2017/2/1

N2 - 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.

AB - 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.

KW - Classical realizability

KW - Hyland Ong game semantics

KW - Peano arithmetic

UR - http://www.scopus.com/inward/record.url?scp=84999862751&partnerID=8YFLogxK

UR - http://dx.doi.org/10.1016/j.apal.2016.10.006

UR - http://dx.doi.org/10.1016/j.apal.2016.10.006

U2 - 10.1016/j.apal.2016.10.006

DO - 10.1016/j.apal.2016.10.006

M3 - Article

VL - 168

SP - 254

EP - 277

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

SN - 0168-0072

IS - 2

ER -