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

[Nik Weaver]

Hendrick Bloom wrote (quoting me):

> > there are several classically equivalent versions of the concept
> > of well-ordering which are not predicatively equivalent).
>
> 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


First: yes, there is a subtle difference between the version I used
(nonexistence of proper progressive subsets) and strong induction.  To
establish induction for the formula A(n) we would need to consider the
set {n: A(n)}, observe that this is a progressive subset of omega, and
then conclude that A(n) holds for all n.  But forming the set {n: A(n)}
requires a comprehension axiom.  Unless A(n) has some special form
(e.g., is arithmetical) this step would generally be predicatively
illegitimate.


Three predicatively inequivalent versions of well-ordering are:

(1)  Induction for sets, i.e., there is no proper progressive subset.

(2)  Strong induction in some predicatively acceptable language.
(Also predicatively meaningful, but generally stronger than (1).)

(3)  Schematic induction: the statement

[P(0) and (forall n)(P(n) --> P(n+1))] --> (forall n)P(n)

where P is a "predicate variable", together with a deduction rule
which allows substitution of any legal formula for P.  (Not even
predicatively meaningful because of the circularity involved in the
fact that formulas substitutible for P may themselves contain P.)


A failure to appreciate the predicative distinction between classically
equivalent formulations of well-ordering pervades the literature on
predicativism.  For example, the whole idea of "autonomous progressions",
where one bootstraps up to larger ordinals by admiting infinitary proofs
of length alpha once alpha has been shown to be an ordinal notation, rests
on this mistake.  I go into this in some detail in my paper "Predicativity
beyond Gamma_0".  Two formal systems that have been alleged to model
predicative reasoning, Ref*(PA(P)) (Feferman) and U(NFA) (Feferman and
Strahm), incorporate schematic induction on omega and are predicatively
illegitimate for that reason (among others).

The main thing that people seem to have gotten out of the Gamma_0 paper
so far is the idea that I'm predicatively accessing ordinals larger than
Gamma_0 (that's the point of the title).  However, a major contribution
of the paper is the fact that I get *up to* Gamma_0 using predicative
methods.  This has been claimed many times before --- going back forty
years --- but, as I show in my paper, *all* previous attempts at some
point involve impredicatively passing between inequivalent well-ordering
statements.

As for other versions of well-ordering, quoting from footnote 15 of
my Gamma_0 paper:

"In intuitionistic logic with arithmetical comprehension, the numerical
omniscience schema, and `A or not A' for all atomic A, for any a in
omega and any ordering on omega the statement (1) (forall X)TI(X,a) is
equivalent to (2) the assertion that {b: b < a} has no proper progressive
subsets and also to (3) the assertion that for all X, if there exists
b < a in X then there is a least such b.  Assuming dependent choice for
arithmetical formulas, the preceding are also equivalent to (4) the
assertion that every decreasing sequence in {b: b < a} is eventually
constant and (5) the assertion that there is no strictly decreasing
sequence in {b: b < a}."

Here TI(X,a) is the assertion that if X is a progressive subset of omega
then X contains all elements less than a.

I omit the proofs of these statements, but they are easy and I am
happy to provide sketches if anyone wants.

Nik Weaver
Math Dept.
Washington University
St. Louis, MO 63130 USA
nweaver at math.wustl.edu