Réunion ANR Récré, 15 novembre 2012
Réunion du projet ANR Récré ouverte à tous les participants des rencontres CHoCoLa.
Lieu
La rencontre aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, dans l'amphi B. Pour venir, voir les instructions sur le site du LIP ou sur un plan, par exemple chez Google Maps. À l'entrée, se présenter à la réception, qui aura la liste des inscrits.
Programme
- 10:30 – 12:00
-
Jean-Louis Krivine (Paris 7)
- 14:00 – 15:00
-
Lionel Rieg (ENS Lyon)
We give here a new proof of Herbrand's theorem in PAω : we use a forcing transformation to add a Cohen real to PAω. This new real allows us to avoid using the fan theorem and requiring an order on atomic formulas. We then take a look at the program extracted from this new proof using Krivine's translation of forcing into classical realizability. Because of the clever uses (i.e. only in the forcing universe) of classical logic in the proof, the extracted program does not backtrack the tree it builds, contrary to a classical proof without forcing.
- 15:30 – 16:30
-
Alexander Kreuzer (ENS Lyon)
We investigate the strength of the existence of a non-principal ultrafilters over fragments of higher order arithmetic.
Let (U) be the statement that a non-principal ultrafilter on N exists and let ACA_0^w be the higher order extension of ACA_0 (arithmetical comprehension).
We show that ACA_0^w+(U) is \Pi^1_2-conservative over ACA_0^w and thus that ACA_0^w+(U) is conservative over PA.
Moreover, we provide a program extraction method and show that from a proof of a strictly Pi^1_2 statement \forall f \exists g A_qf(f,g) in ACA_0^w+(U)$ a realizing term in Gödel's system T can be extracted. This means that one can extract a term t, such that \forall f A_qf(f,t(f)).
