Treffer: Realizability for Peano Arithmetic with Winning Conditions in HON Games

Title:
Realizability for Peano Arithmetic with Winning Conditions in HON Games
Authors:
Blot, Valentin
Contributors:
Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon), Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Research Institute for Mathematical Sciences, Kyoto University
Source:
Typed Lambda Calculi and Applications. :77-92
Publisher Information:
CCSD; Springer Berlin Heidelberg, 2013.
Publication Year:
2013
Collection:
collection:ENS-LYON
collection:CNRS
collection:UNIV-LYON1
collection:LIP
collection:UDL
collection:UNIV-LYON
Subject Terms:
Hyland Ong game semantics, Peano arithmetic, Classical realizability, ACM: F.: Theory of Computation, F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES, F.4.1: Mathematical Logic, [INFO.INFO-LO]Computer Science [cs], Logic in Computer Science [cs.LO]
Subject Geographic:
Eindhoven, Netherlands
Original Identifier:
HAL: hal-00793324
Document Type:
Konferenz conferenceObject<br />Conference papers
Language:
English
Relation:
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-38946-7_8
DOI:
10.1007/978-3-642-38946-7_8
Access URL:
https://hal.science/hal-00793324
https://hal.science/hal-00793324v4/document
https://hal.science/hal-00793324v4/file/paper.pdf
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edshal.hal.00793324v4
Database:
HAL

Weitere Informationen

We build a realizability model for Peano arithmetic based on winning conditions for HON games. First 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 Π 0 2 -formulas.