[FOM] Predicativity in CZF: Correction

[Nik Weaver]

Bill Tait wrote:

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

Oh, I see what you meant.  Yes, you're quite right.  If we're using
intuitionistic logic (which is appropriate in this discussion) we
need to slightly rephrase the notion of well-ordering.  Say that <
is a well-ordering of A if

(forall S subset A)(Prog(S) --> S = A),

where Prog(S) abbreviates

(forall x in A)[ (forall y < x)(y in S) --> x in S ]

("S is progressive").

That's classically equivalent to the usual definition of well-ordering
(a fun exercise) and eliminates the double-negative issue that you
rightly raise.

It doesn't affect my point because predicativists still have
the identical problem that I discussed previously, namely, the
fact that A is well-ordered does not predicatively entail that
it supports induction for arbitrary predicates.  In other words
we cannot infer

Prog(phi) --> (forall x in A)(phi(x))

where Prog(phi) abbreviates

(forall x in A)[ (forall y < x)phi(y) --> phi(x) ]

from the fact that A is well-ordered.  Making this inference
requires the ability to form the set S = {x in A: phi(x)}.

Does that help?  I considered mentioning this in my earlier
message but decided not to for the sake of brevity.  So, thank
you for giving me the chance to clarify this.

Nik