[FOM] predicativity

[Jeremy Avigad]

Nick Weaver wrote:

> Perhaps
> everyone already has a favorite foundational stance and is not
> interested in looking at work that supports an opposing view?  If
> so, this would make my readership very small, as I represent a view
> that I gather is almost universally rejected.  (Jeremy Avigad says
> that "it is an awkward fact that there seems to be no strong case
> that predicativity is a notion worthy of our attention".)

It's always nice to be quoted! The remark is taken from an APA/ASL talk 
I gave in Seattle in 2002. I have long been meaning to turn the notes 
from this talk into a paper; but in the meanwhile, so as not to be 
construed an "anti-predicativist," I would like to provide some context.

On the Feferman-Schu"tte notion of predicativity, one is allowed to use 
quantification over N in defining subsets of N, but not quantification 
over P(N). In the talk, I noted that, as an ontological stance, this is 
not a position that many subscribe to these days. Most philosophers and 
mathematicians seem happy to take set theory as a foundation for 
mathematics; those who have qualms about the infinite are prone to 
reject arithmetic set comprehension, which allows quantification over N; 
and for those who subscribe to forms of constructivism or intuitionism, 
the central issues are orthogonal to these.

The upshot is that for most mathematicians and philosophers, on 
ontological grounds, there is little a priori reason to be interested in 
classical predicative theories that go beyond finitism and yet restrict 
set theory significantly. One can point out that such theories are 
strong enough to carry out a good deal of mathematics --- modulo some 
reworking --- but are not as strong, and hence not as dubious, as full 
set theory. But this is a somewhat weak defense, and has not won many 
converts.

I then argued that, in fact, predicative theories do hold a broader 
appeal. Roughly, predicative theories characterize a style of doing 
mathematics in which infinitary objects are built up from a countable 
basis, in stages. A predicative methodology then encompasses a 
collection of methods of working with such constructions that are useful 
and important. I suggested Hensel's construction of the p-adics and 
Ostrowski's lovely classification of the completions of the rationals as 
examples of developments that reflect a predicative orientation.

In short, the point of the talk was to argue that predicative theories 
*are* worthy of attention, independent of one's ontological views, in 
that they help characterize important features of certain mathematical 
developments. But more work is needed to make this last claim more 
precise. Not everything there is to say about mathematics boils down to 
which axioms one believes in; we, as logicians and philosophers, need to 
take other aspects of mathematical practice more seriously.

Jeremy

P.S. One can also claim that reconstruing parts of classical mathematics 
in predicative terms has mathematical benefits as well. For example, 
such a construal may make it possible to use proof-theoretic methods and 
tools to extract additional information from ordinary mathematical 
arguments, a` la proof mining. But here, too, there is a case that needs 
to be made.