[FOM] Predicativity in CZF

[Nik Weaver]

Dan Mehkeri wrote:

> Maybe instead of trying to construct infinite sets by a
> transfinite number of stages, one can think of the set of
> natural numbers as simply given, and all sets as built up
> in a finite number of stages by applying set constructors
> (none of which, of course, is the power set). Full induction 
> would be available over the natural number set and over the
> finite number of stages.

Then you have a problem with strong collection since a binary
relation can become total in the limit.  The fact that CZF has
proof-theoretic strength equal to the Howard-Bachmann ordinal
should tell you that you can't get a model in such a simple way.

Theories with this degree of strength (constructive set theory,
Kripke-Platek set theory, generalized inductive definitions)
are often claimed to be predicative but none of these claims
stands up to scrutiny, in my opinion.  There's always an issue
with predicative well-ordering.

I suspect the Howard-Bachmann ordinal actually is predicative,
but I don't think this has been demonstrated yet.  I doubt
there's going to be any simple, elegant formal system like
those I just mentioned that establishes this; to get up that
high predicatively you're going to have to roll up your sleeves
and bootstrap your way up by hand.  This is going to be hard.

Nik