Aschieri, Federico and Berardi, Stefano - Interactive Learning-Based Realizability for Heyting Arithmetic with EM1

lmcs:1061 - Logical Methods in Computer Science, September 7, 2010, Volume 6, Issue 3
Interactive Learning-Based Realizability for Heyting Arithmetic with EM1

Authors: Aschieri, Federico and Berardi, Stefano

We apply to the semantics of Arithmetic the idea of ``finite approximation'' used to provide computational interpretations of Herbrand's Theorem, and we interpret classical proofs as constructive proofs (with constructive rules for $\vee, \exists$) over a suitable structure $\StructureN$ for the language of natural numbers and maps of G\"odel's system $\SystemT$. We introduce a new Realizability semantics we call ``Interactive learning-based Realizability'', for Heyting Arithmetic plus $\EM_1$ (Excluded middle axiom restricted to $\Sigma^0_1$ formulas). Individuals of $\StructureN$ evolve with time, and realizers may ``interact'' with them, by influencing their evolution. We build our semantics over Avigad's fixed point result, but the same semantics may be defined over different constructive interpretations of classical arithmetic (Berardi and de' Liguoro use continuations). Our notion of realizability extends intuitionistic realizability and differs from it only in the atomic case: we interpret atomic realizers as ``learning agents''.


Source : oai:arXiv.org:1007.1785
DOI : 10.2168/LMCS-6(3:19)2010
Volume: Volume 6, Issue 3
Published on: September 7, 2010
Submitted on: November 15, 2009
Keywords: Computer Science - Logic in Computer Science,F.4.1


Share

Consultation statistics

This page has been seen 33 times.
This article's PDF has been downloaded 11 times.