[FOM] Predicativity in CZF
nweaver at math.wustl.edu
Wed Jun 18 02:30:22 EDT 2008
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".)
More information about the FOM