Mauricio Guillermo, Specifying arithmetical formulae in classical realizability
Schedule
- Feb. 14, 2012, 15:30 - 16:15
Abstract
We present the specification problem, which consists in the characterization of the universal realizers of a given formula in terms of its computational behaviour --this work is strongly related to the results appearing in [1].
After recalling the theoretical framework of Classical Realizability and giving some simple examples on specification, we present two game-theoretic characterizations of universal realizers of arithmetical formulae.
First, we deal with the case where the language of realizers does not contain instructions incompatible with substitutive constants (in the sense of [1]). For this particular case, we generalize the result proven in [2] for an arbitrary number of alternations of quantifiers. This generalization is part of the work of E. Miquey during his internship at Montevideo--see [3]--.
Second, we present the general case, whitout any assumptions about the instructions allowed in the language of classical realizers. This case, as in [1], must be trated with a more sophisticated game and the proof of the specification leans strongly on the Threads Method introduced in [2] and improved in [1].
References
[1]"Specifying Peirce's Law in Classical Realizability". M. Guillermo & A. Miquel. To appear in MSCS.
[2]"Realizability games in arithmetical formulae". M Guillermo. PhD Thesis 2008.
[3] "Realizing Arithmetical Formulae". E. Miquey. Internship 2011.
We present the specification problem, which consists in the characterization of the universal realizers of a given formula in terms of its computational behaviour --this work is strongly related to the results appearing in [1].
After recalling the theoretical framework of Classical Realizability and giving some simple examples on specification, we present two game-theoretic characterizations of universal realizers of arithmetical formulae.
First, we deal with the case where the language of realizers does not contain instructions incompatible with substitutive constants (in the sense of [1]). For this particular case, we generalize the result proven in [2] for an arbitrary number of alternations of quantifiers. This generalization is part of the work of E. Miquey during his internship at Montevideo--see [3]--.
Second, we present the general case, whitout any assumptions about the instructions allowed in the language of classical realizers. This case, as in [1], must be trated with a more sophisticated game and the proof of the specification leans strongly on the Threads Method introduced in [2] and improved in [1].
References
[1]"Specifying Peirce's Law in Classical Realizability". M. Guillermo & A. Miquel. To appear in MSCS.
[2]"Realizability games in arithmetical formulae". M Guillermo. PhD Thesis 2008.
[3] "Realizing Arithmetical Formulae". E. Miquey. Internship 2011.