Ernest Schimmerling

### Mathematical logic seminar - November 6, 2003

 Time: 12 - 1:20 p.m. Room: CFA 110 Speaker: Henry Towsner Graduate Student in Mathematical Sciences Carnegie Mellon University Title: A Realizability Interpretation for Classical Analysis Abstract: 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.