Can ZF Classical Mathematics be Understood from a Constructive Standpoint?

Peter Aczel

Hilbert’s Program (HP) was intended to lead to a positive answer to something like this question when ‘constructive’ is replaced by ‘finitist’. When HP was first conceived there was not yet a clear distinction between the two standpoints. Today we understand the finitist standpoint to be a restricted one, where the abstractions of a constructive standpoint are not available. It is now generally agreed that Godel’s incompleteness results showed that the original HP is not achievable. Instead variants of HP have been formulated and a great variety of results have been obtained, particularly by proof theorists, reducing fragments of classical mathematics to systems which are arguably acceptable from the constructive standpoint or even to systems that are finitistically acceptable. Proof theoretic technics have been refined to such an extent in more recent years, particularly through the work of Michael Rathjen, that one might now hope that some of the tools might eventually be applicable even to full second order arithmetic (PA_{2}). But, because of the extreme complexity of this work and doubts about the constructive character of the systems that PA_{2} might be reduced to, one can wonder if this line of work will really lead to a constructive ‘understanding’ of classical mathematics. Here I will follow another direction.

Of course the problem is the full impredicativity of PA_{2} and stronger systems such as ZF. In my talk I will discuss the status of full impredicativity in the context of my prefered approach to the foundations of constructive mathematics, Martin-Lof’s Constructive Type Theory (CTT). I will review my earlier work on the type theoretic interpretation of the constructive set theory, CZF, and some extensions, and I will discuss ways of strengthening CTT so as to get systems strong enough to interprete ZF. The first crudest approach is to simply add the law of excluded middle to the Curry-Howard treatment of logic in CTT. A more subtle second approach is to add a version of Russell’s Axiom of Reducibility to CTT and use Friedman’s ‘double-negation’ reduction of ZF to IZF. Yet another possible approach is to add axioms for an impredicative type Prop, as in the Huet-Coquand Calculus of Constructions. But it remains an open problem whether this last possible extension is strong enough to interprete IZF and so ZF.

I will conclude by arguing that the second approach gives a more coherent approach to understanding ZF than the standard ‘classical iterative conception’. Although the approach is not completely constructive I believe that it may be the appropriate approach to a constructive ‘understanding’ of classical mathematics.

Address: Department of Computer Science, University of Manchester, Manchester M13 9PL, UK

E-mail: petera@cs.man.ac.uk