| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 5778163 | Annals of Pure and Applied Logic | 2017 | 24 Pages |
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 Î 20-formulas.
Keywords
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Valentin Blot,