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.

Preliminaries

An ordinal \alpha is *definable from a class of ordinals X if and only if there is a formula and ordinals such that \alpha is the unique ordinal for which where for all \alpha we define to be the name for \alpha within L_\gamma. A structure is eligible if and only if: If is an eligible structure then N_\lambda is defined to be as before but with all occurrences of X replaced with. Let N^1, N^2 be two eligible structures which have the same function k. Then we say if and we have:

Silver machine

A Silver machine is an eligible structure of the form which satisfies the following conditions: Condensation principle. If then there is an \alpha such that. Finiteness principle. For each \lambda there is a finite set such that for any set we have Skolem property. If \alpha is *definable from the set, then ; moreover there is an ordinal , uniformly \Sigma_1 definable from , such that.