Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM_1

摘要

We interpret classical proofs as constructive proofs (with constructive rules for V, E) over a suitable structure N for the language of natural numbers and maps of Godel's system T. We introduce a new Realization semantics we call "Interactive learning-based Realizability", for Heyting Arithmetic plus EM_1 (Excluded middle axiom restricted to Σ_1~0 formulas). Individuals of N evolve with time, and realizers may "interact" with them, by influencing their evolution. We build our semantics over Avigad's fixed point result [1], but the same semantics may be defined over different constructive interpretations of classical arithmetic (in [7], continuations are used). Our notion of realizability extends Kleene's realizability and differs from it only in the atomic case: we interpret atomic realizers as "learning agents".