Atlas Mathematical Conference Abstracts || Conferences | Abstracts | for Organizers | About AMCA

Second St.Petersburg Days of Logic and Computability
August 24-26, 2003
Petersburg Department of Steklov Institute of Mathematics
St. Petersburg, Russia

Organizers
Sergei ADIAN (Russia), Sergei ARTEMOV (Russia/USA), Nikolai KOSSOVSKI (Russia), Maurice MARGENSTERN (France), Grigori MINTS (USA), Yuri MATIYASEVICH (Russia), the chairman, Nikolai NAGORNY (Russia), Vladimir OREVKOV (Russia), Anatol SLISSENKO (France)

View Abstracts
Conference Homepage

A Realizability Interpretation of Classical Analysis
by
Henry Towsner
Stanford University

We present a realizability interpretation for classical analysis-an association of a term to every proof so that the terms assigned to existential formulas represent witnesses to the truth of that formula. For classical proofs of \Pi2 sentences for allx existsy A(x, y), this provides a recursive type 1 function which computes the function given by f(x)=y iff y is the least number such that A(x, y).

Date received: May 1, 2003

Copyright © 2003 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Mathematical Conference Abstracts. Document # cajy-36.