[FOM] Predicativity in CZF

[Nik Weaver]

Bill Tait wrote:

> In neither the elementary nor the non-elementary case is the analysis
> of inductive definitions from below ("stages") or from above
> (intersection of hereditary sets) available for the constructivist:
> They have to be taken sui generis---based on "intuition", I guess.

Bill, thank you for the message.  You seem to feel that
the difficulties in predicatively justifying generalized
inductive definitions are already present in the case of
the natural numbers.

I don't think that's true of the specific difficulty I
raised, namely, that a predicativist cannot use the fact
that an inductive class has been generated in well-ordered
stages to infer the minimality of that class.

For example, it is predicatively evident that the constructive
second number class is well-ordered, but not that it supports
full induction.  That's why proving minimality is a problem.
Whereas predicativists who accept the natural numbers would
say that it is just as evident that they support full
induction as it is that they are well-ordered.

If you want to argue that omega is evidently well-ordered
but does not evidently support full induction, then minimality
becomes a problem in this case too.  But only then.

(Also --- I'm not sure what you meant by your comment that
"In this case, S=A".)

Nik