[FOM] Least class that ...

[José Félix Costa]

Richard Haney:

«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?»

The concept you search for is that of an inductive closure. See, e.g. (where
it is quite well explained), in

Jean H. Gallier
Logic for Computer Science, Foundations of Automatic Theorem Proving
Willey (1987)

§2.3 ( pag 17 - ) Inductive Definitions

It provides what you want, inductive set X_+ and co-inductive set X^+ and
main results such like proposition 2.3.1.

Inductive class X_+ is bottom-up constructive (pag 19). The definition you
gave in your mail is top-down.

Of course you have also treatises on the subject of definition, like
Curry's.

+++++++++++++++++++++++++++++++++++++++++++++++
J. Felix Costa
Departamento de Matematica
Instituto Superior Tecnico
Av. Rovisco Pais, 1049-001 Lisboa, PORTUGAL
tel:      351 - 21 - 841 71 45
fax:     351 - 21 - 841 75 98
e-mail:   fgc at math.ist.utl.pt
www:    http://fgc.math.ist.utl.pt/jfc.htm
+++++++++++++++++++++++++++++++++++++++++++++++