BerardideLiguoro:CSL08 (In proceedings)

Author(s)  Stefano Berardi and Ugo de' Liguoro 
Title  « A Calculus of Realizers for EM1 Arithmetic » 
In  Proceedings of CSL '08 
Series  Lecture Notes in Computer Science 
Volume  5213 
Page(s)  215229 
Year  2008 
Publisher  SpringerVerlag 
Abstract 
We propose a realizability interpretation of a system for quantifier free arithmetic which is equivalent to the fragment of classical arithmetic without nested quantifiers, which we call EM1arithmetic. We interpret classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the ``environment'' and with each other. With respect to known constructive interpretations of classical arithmetic, the present one differs under many respects: for instance, the interpretation is compositional in a strict sense; in particular the interpretation of (the analogous of) the cut rule is the plain composition of functionals. As an additional remark, any two quantifierfree formulas provably equivalent in classical arithmetic have the same realizer. 
Download the complete article:
@inproceedings{BerardideLiguoro:CSL08,
volume = {5213},
author = {Stefano Berardi and de' Liguoro, Ugo},
series = {Lecture Notes in Computer Science},
booktitle = {Proceedings of CSL '08},
tag = {{CSL'8}},
localfile = {http://www.di.unito.it/~deligu/pub/RealWFA.pdf},
title = {{A Calculus of Realizers for EM1 Arithmetic}},
abstract = {We propose a realizability interpretation of a system for
quantifier free arithmetic which is equivalent to the fragment of
classical arithmetic without nested quantifiers, which we call
EM1arithmetic. We interpret classical proofs as interactive
learning strategies, namely as processes going through several
stages of knowledge and learning by interacting with the
``environment'' and with each other. With respect to known
constructive interpretations of classical arithmetic, the present
one differs under many respects: for instance, the interpretation
is compositional in a strict sense; in particular the
interpretation of (the analogous of) the cut rule is the plain
composition of functionals. As an additional remark, any two
quantifierfree formulas provably equivalent in classical
arithmetic have the same realizer.},
publisher = {SpringerVerlag},
year = {2008},
pages = {215229},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)