Spring Lectures in Mathematical Logic

Speaker:	Prof. Grigori MINTS, Stanford University, USA
Place:	Room B 216, Institute of Cybernetics, Akadeemia tee 21, Tallinn, Estonia
Time:	Friday, May 25, 2001, 14:00

EPSILON SUBSTITUTION: PAST AND FUTURE

Abstract

Epsilon substitution method introduced by Hilbert provides numerical realizations of existential sentences. It attracted interest of J. von Neumann, H. Weyl, W. Ackermann and other logicians. After original setbacks and successes in number-theoretic setting before 1941 further progress was made in 1990-s for mathematical analysis (second order arithmetic). We describe original formulation in the framework of Hilbert's program, subsequent change of emphasis to verifiable computer programs, results obtained for predicative subsystems of analysis and the most recent progress for impredicative part.

About the Speaker

Grigori Mints was working at the Institute of Cybernetics in the years 1985 - 1991. Jointly with Enn Tyugu he has developed a theoretical basis for an automated programs synthesis system PRIZ, a direct successor of which is the modern system NUT. The main mathematical idea behind these systems is a combination of proof-search in intuitionistic calculi with a fact that intuitionistic proof of a sentence automatically gives rise to a program specified by that sentence, together with its correctness proof.

G. Mints is also well-known for many more contributions to Proof Theory. Among the topics of his continuing interest is Hilbert's epsilon calculus and epsilon substitution method.

Dr. Sergei Tupailo
Institute of Cybernetics at TTU
Akadeemia tee 21, 12618 Tallinn, Estonia
email: sergei@cs.ioc.ee