Interactive Learning-Based Realizability for Heyting Arithmetic with EM1

TL;DR

This paper introduces an interactive learning-based realizability semantics for Heyting Arithmetic with the restricted law of excluded middle, enabling a constructive interpretation of classical proofs through evolving individuals and interaction.

Contribution

It develops a novel semantics that combines finite approximation and interaction, extending intuitionistic realizability to classical arithmetic with EM1.

Findings

Semantic framework interprets classical proofs constructively

Realizers are modeled as learning agents influencing evolving individuals

Framework can be adapted to different constructive interpretations

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\"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''.