[FOM] predicativity
giovanni sambin
sambin at math.unipd.it
Thu Sep 22 12:22:09 EDT 2005
>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
More information about the FOM
mailing list