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.
Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves
BERARDI, Stefano
2007-01-01
Abstract
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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
