[FOM] Predicativity in CZF: Correction
williamtait at mac.com
Wed Jun 18 10:49:48 EDT 2008
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.
More information about the FOM