[FOM] Predicativity in CZF
Nik Weaver
nweaver at math.wustl.edu
Sun Jun 22 14:23:05 EDT 2008
I wrote:
> Actually in predicativism we have a hierarchy of
> well-ordering notions characterized by their supporting
> induction for different classes of predicates. This seems
> not to be widely understood.
And Michael Rathjen replied:
> I completely agree. This is well-known to proof-theorists,
> but as you say probably not widely known elsewhere.
I'm sure you are right, but proof theorists have not been
sensitive to this point in analyses of predicativism. I
already mentioned that the purported predicative justification
of generalized inductive definitions hinges on a failure to
recognize just this distinction. The classical Feferman-Schutte
analysis involves the same fallacy when we pass from "the
notation \gamma_n is well-ordered" to "the theory S_{\gamma_n}
is valid" (where (\gamma_n) is the canonical sequence of
notations increasing to \Gamma_0). In order for this inference
to be legitimate we would have to have induction for the
predicate "S_a is valid", which can't even be expressed in
the language of second order arithmetic.
> On the other hand if one drops Set Induction from the axioms
> of CZF the resulting theory CZF^- is much weaker.
Right! I wasn't thinking about this when I wrote my earlier
message about strong collection and subset collection. But
now that you mention it, set induction is also impredicative
--- with, again, predicative well-ordering being the issue.
The justification for set induction (again, please correct me
if I'm wrong) is that sets are thought of as being built up in
well-ordered stages. But that would only be enough to support
set induction for delta_0 predicates.
Nik
More information about the FOM
mailing list