Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves

We define an effective, sound and complete game semantics for HA_omega, 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_omega, and that they are a sound and complete interpretation of HA_omega.