[FOM] Predicativity in CZF
williamtait at mac.com
Mon Jun 16 13:46:06 EDT 2008
On Jun 15, 2008, at 12:32 PM, Nik Weaver wrote:
> But look what happens. Let's say we want to inductively
> define a class A satisfying some closure conditions. We
> tell the predicativist to build A up in a series of
> well-ordered stages. Then he has to prove that A is
> minimal, i.e., it is contained in any other class B that
> satisfies the same closure conditions.
> Well, since A is built up in well-ordered stages we'll
> prove this by induction. Let S be the set of stages at
> which elements of A appear that do not belong to B. If
> S is nonempty then it has a least element and we can now
> get a contradiction from the fact that B satisfies the
> closure conditions which define A. But wait a minute.
> Was S a predicatively legitimate set?
Nik, This cannot be quite the right way to think about inductive
definitions constructively. The simplest example (it was Brouwer's) of
a non-elementary inductively defined set for a constructivist IS the
constructive second number class A=O. In this case, S=A.
The definition of O is impredicative in the usual sense because the
condition from which we can infer e \in O, already contains "O". Of
course this already happens with elementary inductive definitions---
say that of the first number class, N; but with the exception of a few
scholars such as P. Bernays, E. Nelson, and C. Parsons, we excuse it
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.
More information about the FOM