| 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.
|