Abstract
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 Π20-formulas. © 2013 Springer-Verlag.
Cite
CITATION STYLE
Blot, V. (2013). Realizability for Peano arithmetic with winning conditions in HON games. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7941 LNCS, pp. 77–92). https://doi.org/10.1007/978-3-642-38946-7_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
