[FOM] predicativity

[giovanni sambin]

>The point is that impredicative
>(circular) definitions only make sense against a background of a
>well-defined preexisting universe of sets; if one does not believe
>there is such a thing, it becomes very hard to see why impredicative
>definitions should be allowed.

I fully agree on this. As well as on the fact that more energy should 
be given to the investigation of predicative mathematics.

>At the risk of being repetitious, my papers on conceptualism can be
>found at
>
>http://www.math.wustl.edu/~nweaver/conceptualism.html

I agree with most of the claims in your first paper (it took me some 
time to read it, I have just finished; it will take much longer to 
read the other two...).

It seems that you are unaware of the intuitionistic and predicative 
approach to foundations, as in Per Martin-L"of's type theory (started 
in early 70s), and of the mathematics built on it, a notable example 
being formal topology (started in the mid 80s). You can find some 
more information on both in my web-site: www.math.unipd.it/~sambin

Some specific comments on your claims:

1. I have nothing against your claim that predicativity does not stop 
at Gamma_0; as far as I understand, also Per Martin-L"of would say so.

2. I personally do not like arguments "by size": what is wrong with 
Cantorian universe is in my opinion that it presupposes existence of 
all sets; being "too big" is a consequence of this (your paper, page 
5).

3. I agree with your arguments against "flocks" and "average 
taxpayers" as metaphysical entities; they apply in my opinion to all 
abstract concepts, hence to all of mathematical concepts.

4. Your sentence "the predicativist literature tends to presume 
classical logic" (page 9) is what made me presume that you don't know 
about Martin-L"of's type theory.

5. The distinction you make between "sets in the strong sense - sets 
in the weak sense (page 10), later called sets - classes (page 11) 
apparently coincides with the distinction between sets (or data 
types) and categories (or classes, logical types, collections) which 
is fundamental in Martin-L"of's theory.

6. I agree with your comment that "one can make a case that this 
[using intuitionistic logic] is the more elegant approach". That is 
why formal topology was developed.

7. The question about the meaning of "forall X there exists Y" which 
you touch on page 16 is a crucial question in the approach via type 
theory. The usual explanation in type theory is that you must have a 
function justifying it (hence validity of the axiom of choice). See 
the lecture by Martin-L"of on the axiom of choice given at TYPES 
2004, and also the paper by Maietti and myself in my webpage.

Let me conclude with a general remark. I am very much in favour of 
any new, well-argued proposal for the foundations of mathematics. It 
will be nice to have more information about your conception. I should 
add, however, that I prefer to think that mathematics is not 
something fixed which has to be given a foundation, but rather that 
the choice for a foundation goes together with the development of 
some specific mathematics. So the aim is, for instance, not only 
better information on classical results, but also pieces of 
mathematics which classically had not appeared. Again, you can find 
more info on this in my webpage.

Giovanni Sambin

Professor of Mathematical Logic
Dipartimento di Matematica P. e A., Universita' di Padova (Italy)
sambin at math.unipd.it
http://www.math.unipd.it/~sambin