×

Semantics for intuitionistic arithmetic based on Tarski games with retractable moves. (English) Zbl 1215.03069

Ronchi della Rocca, Simona (ed.), Typed lambda calculi and applications. 8th international conference, TLCA 2007, Paris, France, June 26–28, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73227-3/pbk). Lecture Notes in Computer Science 4583, 23-38 (2007).
Summary: We define an effective, sound and complete game semantics for \({\text{HA}_{\text{inf}}}\), Intuitionistic Arithmetic with \(\omega \)-rule. Our semantics is equivalent to the original semantics proposed by Lorentzen, but it is based on the more recent notions of “backtracking” and of isomorphism between proofs and strategies. We prove that winning strategies in our game semantics are tree-isomorphic to the set of proofs of some variant of \({\text{HA}_{\text{inf}}}\), and that they are a sound and complete interpretation of \({\text{HA}_{\text{inf}}}\).
For the entire collection see [Zbl 1120.03002].

MSC:

03F30 First-order arithmetic and fragments
PDFBibTeX XMLCite
Full Text: DOI