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

lmcs:1061 - Logical Methods in Computer Science, September 7, 2010, Volume 6, Issue 3 - https://doi.org/10.2168/LMCS-6(3:19)2010
Interactive Learning-Based Realizability for Heyting Arithmetic with EM1Article

Authors: Federico Aschieri ; Stefano Berardi

    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ödel'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''.


    Volume: Volume 6, Issue 3
    Published on: September 7, 2010
    Imported on: November 15, 2009
    Keywords: Computer Science - Logic in Computer Science,F.4.1

    13 Documents citing this article

    Consultation statistics

    This page has been seen 1236 times.
    This article's PDF has been downloaded 287 times.