Abstract
We define an effective, sound and complete game semantics for HAinf, Intuitionistic Arithmetic with ω-rule. Our semantics is equivalent to the original semantics proposed by Lorentzen [6], but it is based on the more recent notions of "backtracking" ([5], [2]) and of isomorphism between proofs and strategies ([8]). We prove that winning strategies in our game semantics are tree-isomorphic to the set of proofs of some variant of HA inf, and that they are a sound and complete interpretation of HA inf. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Berardi, S. (2007). Semantics for intuitionistic arithmetic based on tarski games with retractable moves. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4583 LNCS, pp. 23–38). Springer Verlag. https://doi.org/10.1007/978-3-540-73228-0_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
