Thematic Afternoon on CONSTRUCTIVISM
including the first Arend Heyting Lecture

Date: Friday, December 14, 2001
Place: De Rode Hoed, Keizersgracht 102, 1015 CV AMSTERDAM, tel. 020 638 5606

ABOUT THE AREND HEYTING LECTURE

The Arend Heyting Foundation came into being as the result of the last will of ms J.F. Heyting-van Anrooij, who died in september 1998. The aims of the Foundation are to support mathematical logic, and more specifically to organize every three years the Arend Heyting Lecture. Ms. heyting stipulated in he last will that the first Arend Heyting lecture should be devoted to workconnected with Heytings own work on intuitionism.

If you wish to attend, please notify Marjan Veldhuisen: marjanv@science.uva.nl

PROVISIONAL PROGRAMME (version 6-11-2001)

13.30-13.45 Reception
13.45-14.00 Introduction by the chairman of the Arend Heyting Foundation
14.00-15.00 F. Richman, Constructive algebra (1st Arend Heyting Lecture)
15.10-15.50 J. van Oosten, Modified realizability
15.50-16.30 Drinks & Snacks
16.30-17.30 A. Simpson, After the Interval

ABSTRACTS OF THE TALKS

F.Richman, Constructive Algebra (1st AREND HEYTING Lecture)
In "Untersuchungen über intuitionistische Algebra", Heyting reduces the question of whether a nonzero polynomial with coefficients in a field divides another polynomial, to whether a finite number of field elements are zero. This may be thought of as a generalization of the division algorithm for monic polynomials. I will use this theorem as a point of departure to talk about some topics in constructive algebra including discrete versus nondiscrete, the definition of a field, modules over local rings, and what constitutes a good theorem.

A. Simpson, After the Interval
In this talk I will address the question: "what is the correct  constructive notion of real number?" Standard accounts are based on arithmetisation - one starts off with the natural numbers and constructs the real numbers from them. I shall discuss an alternative approach, which is joint work with Martin Escardo. Rather than constructing the real numbers, we assumeinstead the existence of an interval of real numbers as an  independent object that is to be identified via its characterising geometric properties. Interestingly, this approach gives rise to a
new constructive notion of real number - at least it appears to. I shall discuss in how this new notion of real number compares with
the familiar notions of Cauchy and Dedekind real. Several open  questions remain, not least: is the new notion of real number
genuinely different from the Cauchy reals?

J. van Oosten, Modified realizability
Modified realizability is a recursive interpretation of intuitionistic formal arithmetic (HA) into itself. In various forms, Modified Realizability has been applied: to obtain consistency and independence results, but also for the construction of models for type theories (e.g., Martin-Loef Type Theory).
    We try to investigate the question: what does HA say about this interpretation? To this end, we employ some simple tools as the Friedman translation and a notion of internal forcing. A straightforward approach turns out to run into an obstacle however; we shall exhibit this.

ABOUT THE SPEAKERS

Fred  Richman  graduated at Princeton University magna cum laude in 1958, receiving the Covington Mathematics Prize. He obtained his PhD in 1963 at the University of Chicago under Irving Kaplansky. In 1971 he became a full professor at New Mexico Stae University. In 1980 his University gave him the Westhafer Award for Excellence in Research, a university-wide award given every two years.  Since 1990 he is a professor of the Dept. of Mathematics, Florida Atlantic University. He received National Science Foundation grants for research in abelian group theory continuously from 1966 to 1985, and from 1988 to 1990.
He has published extensively on algebra, and has been a leading researcher in the field of  Constructive Mathematics in teh spirit of Errett Bishop, especially algebra.

Alex Simpson has a BA in mathematics from the University of Oxford (1987), an MSc in artificial intelligence from the University of Edinburgh (1988), and a PhD in computer science also from Edinburgh (1994). He has since been employed as EPSRC postdoctoral research fellow (1994-5),  then as a lecturer (1996-present) at the Division of Informatics, University of Edinburgh, where he is a member of the Laboratory for  Foundations of Computer Science. Since October 2001, he has held an  EPSRC advanced research fellowship. His research interests are in the mathematical theory of computation, its logical ramifications,  and also in the general application of logic in computer science.

Jaap van Oosten studied first Dutch, then switched to Mathematics at the University of Amsterdam. He obtained his Ph.D in 1991 on a thesis Exercises in Realizability  under A.S. Troelstra. At present he is a lecturer in the Mathematics Dept., specialty Mathematical Logic  at  Utrecht University. he has published a number of papers on mathematical logic, especially on realizability.