[FOM] Predicativity in CZF

[William Tait]

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  
there.

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.

Best,

Bill