[FOM] Intuitionism, predicativism, and ill-defined domains
Jaap van Oosten
jvoosten at math.uu.nl
Mon Oct 31 05:42:47 EST 2005
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
More information about the FOM
mailing list