[FOM] Predicativity in CZF: Correction

Nik Weaver nweaver at math.wustl.edu
Wed Jun 18 12:56:35 EDT 2008

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.


More information about the FOM mailing list