|
|
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 higher-order 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.  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.  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.  We then analyze the algorithmic content of this proof. |
|
|