Silver machine

In set theory, Silver machines are devices used for bypassing the use of fine structure in proofs of statements holding in L. They were invented by set theorist Jack Silver as a means of proving global square holds in the constructible universe.


An ordinal   is *definable from a class of ordinals X if and only if there is a formula   and   such that   is the unique ordinal for which   where for all   we define   to be the name for   within  .

A structure   is eligible if and only if:

  1.  .
  2. < is the ordering on On restricted to X.
  3.   is a partial function from   to X, for some integer k(i).

If   is an eligible structure then   is defined to be as before but with all occurrences of X replaced with  .

Let   be two eligible structures which have the same function k. Then we say   if   and   we have:


Silver machineEdit

A Silver machine is an eligible structure of the form   which satisfies the following conditions:

Condensation principle. If   then there is an   such that  .

Finiteness principle. For each   there is a finite set   such that for any set   we have


Skolem property. If   is *definable from the set  , then  ; moreover there is an ordinal  , uniformly   definable from  , such that  .


  • Keith J Devlin (1984). "Chapter IX". Constructibility. ISBN 0-387-13258-9.