License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2013.597
URN: urn:nbn:de:0030-drops-42212
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4221/
Go to the corresponding LIPIcs Volume Portal

Rieg, Lionel

Extracting Herbrand trees in classical realizability using forcing

pdf-format:
41.pdf (0.6 MB)

Abstract

Krivine presented in [Krivine, 2011] 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 [Miquel, 2011] in a fully typed setting in classical higher-order arithmetic (PA-omega^+).
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 completeness 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-omega^+, 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.

BibTeX - Entry

@InProceedings{rieg:LIPIcs:2013:4221,
  author =	{Lionel Rieg},
  title =	{{Extracting Herbrand trees in classical realizability using forcing}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{597--614},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Simona Ronchi Della Rocca},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4221},
  URN =		{urn:nbn:de:0030-drops-42212},
  doi =		{10.4230/LIPIcs.CSL.2013.597},
  annote =	{Keywords: classical realizability, forcing, Curry-Howard correspondence, Herbrand trees}
}

Keywords: classical realizability, forcing, Curry-Howard correspondence, Herbrand trees
Collection: Computer Science Logic 2013 (CSL 2013)
Issue Date: 2013
Date of publication: 02.09.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI