Vendredi 5 Juillet
Heure: 
00:59  14:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Forcing in classical realizability: the case study of Herbrand trees 
Description: 
Lionel Rieg Krivine presented in 2010 a methodology to combine Cohen's forcing with the theory of classical realizability and showed that the forcing condition can be seen as a reference that is not subject to backtracks. The underlying classical program transformation was then analyzed by Miquel (2011) in a fully typed setting in classical higherorder arithmetic (PAw+).As a case study of this methodology, I present a method to extract a Herbrand tree from a classical realizer of an existential formula, following the idea of the proof of Herbrand theorem.&nbsp; Unlike the traditional proof based on Konig's lemma (using a fixed enumeration of atomic formulas), our method is based on the introduction of a particular Cohen real.&nbsp; It is formalized as a proof in PAw+, making explicit the construction of generic sets in this framework in the particular case where the set of forcing conditions is arithmetical.&nbsp; We then analyze the algorithmic content of this proof. 

