|Time:|| 12 - 1:20 p.m.
|Speaker:|| Henry Towsner
Graduate Student in Mathematical Sciences
Carnegie Mellon University
A Realizability Interpretation for Classical Analysis
I present a realizability interpretation of classical
analysis, that is, a method of assigning to proofs in second order
arithmetic an object (in this case functionals of the polymorphic
lambda calculus) in such a way that the object assigned to a formula
\exists x A(x) (where A is recursive) is a number n so that A(n)
holds. In addition, the object assigned to a formula \forall x\exists
y A(x,y) (where A is recursive) will be a type one functional f such
that f(n)=m iff m is the least y satisfying A(n,y).
|Organizer's note:|| Please bring your lunch.