[FOM] Intuitionism, predicativism, and ill-defined domains

[Jaap van Oosten]

Hendrik Boom:

> 
> I'd very much like to see a short list of these inequivalent versions
> of well-ordering.  I gather three of them are
> 
>   -- every subset has a least element
>   -- strong induction works (is this the same as the one you used
>      just now?  Or is there a subtle distinction?)
>   -- every descending sequence terminates
> 
> Which one is generally considered to be the paroper
> constructive/predicative/intuitionistic one?  Or do
> constructivists, predicativists, and intuitionists
> not agree on this?

Call them 1), 2), 3). They are not even equivalent in ZF, since the 
implication 3)==>1) needs dependent choices.
>From the intuitionistic point of view, 1) implies classical logic, and
3) is a property which is so weak as to be almost useless. Therefore,
2) is generally used in intuitionistic formulations of well-foundedness
(for example, in intuitionistic axiomatizations of set theory).

Jaap van Oosten