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

Aschieri, Federico

Transfinite Update Procedures for Predicative Systems of Analysis

pdf-format:
7.pdf (0.5 MB)

Abstract

We present a simple-to-state, abstract computational problem, whose solution implies the 1-consistency of various systems of predicative Analysis and offers a way of extracting witnesses from classical proofs. In order to state the problem, we formulate the concept of transfinite update procedure, which extends Avigad's notion of update procedure to the transfinite and can be seen as an axiomatization of learning as it implicitly appears in various computational interpretations of predicative Analysis. We give iterative and bar recursive solutions to the problem.

BibTeX - Entry

@InProceedings{aschieri:LIPIcs:2011:3220,
  author =	{Federico Aschieri},
  title =	{{Transfinite Update Procedures for Predicative Systems of Analysis}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{20--34},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Marc Bezem},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3220},
  URN =		{urn:nbn:de:0030-drops-32200},
  doi =		{10.4230/LIPIcs.CSL.2011.20},
  annote =	{Keywords: update procedure, epsilon substitution method, predicative classical analysis, bar recursion}
}

Keywords: update procedure, epsilon substitution method, predicative classical analysis, bar recursion
Collection: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
Issue Date: 2011
Date of publication: 31.08.2011

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