[FOM] predicativity

[Nik Weaver]

Giovanni Sambin wrote:

> 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

Thank you for the reference; I enjoyed browsing your website.  I do
not know as much about Martin-L"of's theory as I should.  However,
I am under the impression that in this context the term "predicative"
is used in a somewhat loose sense which allows generalized inductive
definitions.  (If I am mistaken in thinking this, please correct me.)
At one point I did believe that generalized inductive definitions are
predicatively legitimate provided intuitionistic logic is used, but
on thinking through this question more carefully I concluded that
even in this case there is still a slightly subtle circularity.  I
explain this in section 2.5 of my Gamma_0 paper.

Nik