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.