Extracting Herbrand trees in classical realizability using forcing

Abstract : Krivine presented in [Kri10] 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 [Miq11] in a fully typed setting in classical higher-order arithmetic (PAω⁺). As a case study of this methodology, we present a method to extract a Herbrand tree from a classical realizer of inconsistency, following the ideas underlying the compactness theorem and the proof of Herbrand's theorem. Unlike the traditional proof based on König'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 PAω⁺, 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.
Type de document :
Communication dans un congrès
Simona Ronchi Della Rocca. Computer Science Logic 2013, Sep 2013, Turin, Italy. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 23, pp.15, 2013, LIPIcs. 〈10.4230/LIPIcs.CSL.2013.i〉
Liste complète des métadonnées

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00814278
Contributeur : Lionel Rieg <>
Soumis le : mercredi 11 décembre 2013 - 21:34:14
Dernière modification le : mardi 24 avril 2018 - 13:52:48
Document(s) archivé(s) le : vendredi 14 mars 2014 - 10:51:40

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Lionel Rieg. Extracting Herbrand trees in classical realizability using forcing. Simona Ronchi Della Rocca. Computer Science Logic 2013, Sep 2013, Turin, Italy. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 23, pp.15, 2013, LIPIcs. 〈10.4230/LIPIcs.CSL.2013.i〉. 〈ensl-00814278v2〉

Partager

Métriques

Consultations de la notice

202

Téléchargements de fichiers

78