Realizability Games in Arithmetical Formulae.
Mauricio Guillermo · 2008
This work is devoted to Krivine's Realizability, focusing over computational aspects of realizers. Each formula has associated a game. Each proof of a formula gives a term implementing a winning strategy for the game associated to the proven formula. A proof is, by soundness, a combinator capable to take winning strategies of the premises and furnish a winning strategy for the conclusion. Are treated the following topics: A. The specification problem, which consists in characterize all realizers of a given formula in computational terms. Many examples are given. B. We study a proof as a combinator of winning strategies: Consider an implication $A\to B$ where $A$ and $B$ are $\Sigma^0_2$ formulae. Consider $C$ the prenex normal form of the implication $A\to B$. We study a proof of $A, C\to B$ as a combinator of winning strategies. In order to do this work, some techniques where developed to trace the execution of processes, in particular the so called threads method.