  In this dissertation we provide mathematical evidence that the concept of
learning can be used to give a new and intuitive computational semantics of
classical proofs in various fragments of Predicative Arithmetic.
  First, we extend Kreisel modified realizability to a classical fragment of
first order Arithmetic, Heyting Arithmetic plus EM1 (Excluded middle axiom
restricted to Sigma^0_1 formulas). We introduce a new realizability semantics
we call "Interactive Learning-Based Realizability". Our realizers are
self-correcting programs, which learn from their errors and evolve through
time.
  Secondly, we extend the class of learning based realizers to a classical
version PCFclass of PCF and, then, compare the resulting notion of
realizability with Coquand game semantics and prove a full soundness and
completeness result. In particular, we show there is a one-to-one
correspondence between realizers and recursive winning strategies in the
1-Backtracking version of Tarski games.
  Third, we provide a complete and fully detailed constructive analysis of
learning as it arises in learning based realizability for HA+EM1, Avigad's
update procedures and epsilon substitution method for Peano Arithmetic PA. We
present new constructive techniques to bound the length of learning processes
and we apply them to reprove - by means of our theory - the classic result of
Godel that provably total functions of PA can be represented in Godel's system
T.
  Last, we give an axiomatization of the kind of learning that is needed to
computationally interpret Predicative classical second order Arithmetic. Our
work is an extension of Avigad's and generalizes the concept of update
procedure to the transfinite case. Transfinite update procedures have to learn
values of transfinite sequences of non computable functions in order to extract
witnesses from classical proofs.

Logic