Computer Science – Logic in Computer Science
Scientific paper
2010-07-11
LMCS 6 (3:19) 2010
Computer Science
Logic in Computer Science
Scientific paper
10.2168/LMCS-6(3:19)2010
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''.
Aschieri Federico
Berardi Stefano
No associations
LandOfFree
Interactive Learning-Based Realizability for Heyting Arithmetic with EM1 does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Interactive Learning-Based Realizability for Heyting Arithmetic with EM1, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Interactive Learning-Based Realizability for Heyting Arithmetic with EM1 will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-563506