[FOM] Predicativity in CZF: Correction

[William Tait]

On Jun 16, 2008 I mistakenly wrote:

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

I have just reread what Nic Weaver wrote and my response and realized  
that I had mis-read his definition of S. But it remains true that this  
is not the way to understand inductive definitions constructively.   
For the argument shows only that S is not-not-empty, which does not  
imply constructively that it is empty.

I remain happy with the remainder of what I wrote.

Bill Tait