2026-07-23T10:34:49Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3220 2024-03-06T10:33:57Z ddc:004 open_access

Transfinite Update Procedures for Predicative Systems of Analysis Aschieri, Federico update procedure epsilon substitution method predicative classical analysis bar recursion 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Federico Aschieri 2011 Is Part Of LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2011.20 urn:nbn:de:0030-drops-32200 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.20 eng https://creativecommons.org/licenses/by-nd/3.0/legalcode