Interactive Learning-Based Realizability for Heyting Arithmetic with EM1

Abstract

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 }_1^0$ 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''.

References in corpus (1)

• Interactive Realizers and Monads

Cited by in corpus (8)

• The joy of implications, aka pure Horn functions: mainly a survey
• Knowledge Spaces and the Completeness of Learning Strategies
• Interactive Learning Based Realizability and 1-Backtracking Games
• Spector bar recursion over finite partial functions
• Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic
• A Monadic Framework for Interactive Realizability
• Interpreting a Classical Geometric Proof with Interactive Realizability
• A Witness Extraction Technique by Proof Normalization Based on Interactive Realizability