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 ${\displaystyle \alpha }$ is *definable from a class of ordinals X if and only if there is a formula ${\displaystyle \phi (\mu _{0},\mu _{1},\ldots ,\mu _{n})}$ and ${\displaystyle \exists \beta _{1},\ldots ,\beta _{n},\gamma \in X}$ such that ${\displaystyle \alpha }$ is the unique ordinal for which ${\displaystyle \models _{L_{\gamma }}\phi (\alpha ^{\circ },\beta _{1}^{\circ },\ldots ,\beta _{n}^{\circ })}$ where for all ${\displaystyle \alpha }$ we define ${\displaystyle \alpha ^{\circ }}$ to be the name for ${\displaystyle \alpha }$ within ${\displaystyle L_{\gamma }}$.

A structure ${\displaystyle \langle X,<,(h_{i})_{i<\omega }\rangle }$ is eligible if and only if:

1. ${\displaystyle X\subseteq On}$.
2. < is the ordering on On restricted to X.
3. ${\displaystyle \forall i,h_{i}}$ is a partial function from ${\displaystyle X^{k(i)}}$ to X, for some integer k(i).

If ${\displaystyle N=\langle X,<,(h_{i})_{i<\omega }\rangle }$ is an eligible structure then ${\displaystyle N_{\lambda }}$ is defined to be as before but with all occurrences of X replaced with ${\displaystyle X\cap \lambda }$.

Let ${\displaystyle N^{1},N^{2}}$ be two eligible structures which have the same function k. Then we say ${\displaystyle N^{1}\triangleleft N^{2}}$ if ${\displaystyle \forall i\in \omega }$ and ${\displaystyle \forall x_{1},\ldots ,x_{k(i)}\in X^{1}}$ we have:

${\displaystyle h_{i}^{1}(x_{1},\ldots ,x_{k(i)})\cong h_{i}^{2}(x_{1},\ldots ,x_{k(i)})}$

Silver machine

A Silver machine is an eligible structure of the form ${\displaystyle M=\langle On,<,(h_{i})_{i<\omega }\rangle }$ which satisfies the following conditions:

Condensation principle. If ${\displaystyle N\triangleleft M_{\lambda }}$ then there is an ${\displaystyle \alpha }$ such that ${\displaystyle N\cong M_{\alpha }}$.

Finiteness principle. For each ${\displaystyle \lambda }$ there is a finite set ${\displaystyle H\subseteq \lambda }$ such that for any set ${\displaystyle A\subseteq \lambda +1}$ we have

${\displaystyle M_{\lambda +1}[A]\subseteq M_{\lambda }[(A\cap \lambda )\cup H]\cup \{\lambda \}}$

Skolem property. If ${\displaystyle \alpha }$ is *definable from the set ${\displaystyle X\subseteq On}$, then ${\displaystyle \alpha \in M[X]}$; moreover there is an ordinal ${\displaystyle \lambda <[sup(X)\cup \alpha ]^{+}}$, uniformly ${\displaystyle \Sigma _{1}}$ definable from ${\displaystyle X\cup \{\alpha \}}$, such that ${\displaystyle \alpha \in M_{\lambda }[X]}$.

References

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