Realizability for Peano arithmetic with winning conditions in HON games

Valentin Blot

doi:10.1016/j.apal.2016.10.006

Realizability for Peano arithmetic with winning conditions in HON games

Valentin Blot

Department of Computer Science

Research output: Contribution to journal › Article › peer-review

2 Citations (SciVal)

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 Π₂ ⁰-formulas.

Original language	English
Pages (from-to)	254-277
Number of pages	24
Journal	Annals of Pure and Applied Logic
Volume	168
Issue number	2
Early online date	13 Oct 2016
DOIs	https://doi.org/10.1016/j.apal.2016.10.006
Publication status	Published - 1 Feb 2017

Keywords

Classical realizability
Hyland Ong game semantics
Peano arithmetic

Access to Document

10.1016/j.apal.2016.10.006Licence: CC BY

Cite this

@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 = feb,

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 B.V.",

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

U2 - 10.1016/j.apal.2016.10.006

DO - 10.1016/j.apal.2016.10.006

M3 - Article

AN - SCOPUS:84999862751

SN - 0168-0072

VL - 168

SP - 254

EP - 277

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 2

ER -

Realizability for Peano arithmetic with winning conditions in HON games

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Semantic Types for Verified Program Behaviour

Semantic Structures for Higher-Order Information Flow

Cite this

Realizability for Peano arithmetic with winning conditions in HON games

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Projects

Semantic Types for Verified Program Behaviour

Semantic Structures for Higher-Order Information Flow

Cite this