[FOM] Least class that ...

[Harvey Friedman]

On 1/30/06 10:19 PM, "Richard Haney" <rfhaney at yahoo.com> wrote:

> A. S. Troelstra & D. van Dalen in * Constructionism in Mathematics: An
> Introduction *, Vol. 1, seem to make frequent use of the idea of the
> least class containing some basic elements and closed under some sort
> of (say, generalized iteration of) operations.  This sort of notion
> seems to be used routinely in many other contexts as well in
> mathematics.  A typical definition I've seen for "the least class that
> ..." is the set-theoretic intersection of all classes containing the
> basic elements and closed under the operations.
> 
> This sort of definition seems to assume some "axiom of infinity" of
> sorts (especially when unbounded constructions are involved) and to
> also be impredicative.
> 
> Does anyone know of a generally useful, alternative type of definition
> (for "the least class that ..." or an alternative concept) that will
> satisfy finitists and predicativists as well?  Is such an idea of "the
> least class that ..." really needed in metamathematics?
> 

Yes, this is a well known situation, where in the usual cases, there is an
alternative type of definition well known to be equivalent.

A typical case is as follows. Let N* be the set of all finite sequences of
nonnegative integers. Let f1,...,fk be functions of several variables from
N* into N*. Let c1,...,cr be elements of N*.

We often want to form the least subset S of N* such that

i. c1,...,cn are in S.
ii. S is closed under the functions f1,...,fk.

To literally form this set without further discussion involves a very
substantial instance of comprehension. In particular, it would involve,
without further explanation, Pi11-CA0. This is highly impredicative under
the usual Feferman/Schutte analysis.

However, the set in question has an alternative definition. This is

the set of all x in N* such that there exists a finite sequence y1,...,yr
from N* such that every yi is either among c1,...,cn or is the value of at
least one of the fi at arguments from y1,...,y_i-1.

The existence of this latter set, for all c's and f's, is equivalent, over
RCA0, to ACA0. Furthermore, it is provable in RCA0 that this latter set, if
it exists, is in fact the least subset S of N* such that i,ii above hold.

In particular, this alternative will satisfy predicativists for sure (in
this context). For finitists or constructivists, this is another matter.
Either definition, even for very concrete f's, may lead to a nonrecursive
set. However, very commonly, the f's have the further property that they
increase lengths, or increase suitable norms, so that one can show the sets
exist and are equal, in RCA0, and also satisfy finitists and
constructivists.

Harvey Friedman