Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
verfasst von : Federico Aschieri, Stefano Berardi
Erschienen in: Typed Lambda Calculi and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We interpret classical proofs as constructive proofs (with constructive rules for ∨ , ∃) over a suitable structure
${\mathcal N}$
for the language of natural numbers and maps of Gödel’s system
${\mathcal{T}}$
. We introduce a new Realization semantics we call “Interactive learning-based Realizability”, for Heyting Arithmetic plus
EM
1
(Excluded middle axiom restricted to
$\Sigma^0_1$
formulas). Individuals of
${\mathcal 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”.