[FOM] Least class that ...
sambin at math.unipd.it
Wed Feb 1 13:57:47 EST 2006
>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?
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).
More information about the FOM