[FOM] Least class that ...

[giovanni sambin]

>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?
>
>Richard Haney

There is no need of "axiom of infinity" or of impredicative 
definitions. What you are aiming at here is just an inductive (or 
generalized inductive) definition. So a set is defined by its 
introduction rules (the inductive clauses) and the eliminations rule, 
telling that you can prove things by induction on those clauses.

This is the idea underlying Martin-Loef's type theory, which is both 
intuitionistic and predicative (in a reasonable sense).

Giovanni Sambin