2026-08-17T16:12:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4624 2024-03-06T10:35:09Z ddc:004 open_access

A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle Aschieri, Federico Zorzi, Margherita Markov's Principle Intuitionistic Realizability Heyting Arithmetic Game Semantics We propose a very simple modification of Kreisel's modified realizability in order to computationally realize Markov's Principle in the context of Heyting Arithmetic. Intuitively, realizers correspond to arbitrary strategies in Hintikka-Tarski games, while in Kreisel's realizability they can only represent winning strategies. Our definition, however, does not employ directly game semantical concepts and remains in the style of functional interpretations. As term calculus, we employ a purely functional language, which is Goedel's System T enriched with some syntactic sugar. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Federico Aschieri and Margherita Zorzi 2014 Is Part Of LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2013.24 urn:nbn:de:0030-drops-46245 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.24 eng https://creativecommons.org/licenses/by/3.0/legalcode