Learning, Realizability and Games in Classical Arithmetic

Details Learning, Realizability and Games in Classical Arithmetic Learning, Realizability and Games in Classical Arithmetic

2010-12-22

arxiv.org/abs/1012.4992v5

Mathematics

Logic

Phd Thesis

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Learning, Realizability and Games in Classical Arithmetic 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 Learning, Realizability and Games in Classical Arithmetic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Learning, Realizability and Games in Classical Arithmetic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-582353