Silver machine

---

title: "Silver machine" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["constructible-universe"] description: "Type of mathematical object" topic_path: "general/constructible-universe" source: "https://en.wikipedia.org/wiki/Silver_machine" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0

::summary Type of mathematical object ::

::callout[type=note] the kind of mathematical object ::

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 \phi(\mu_0,\mu_1, \ldots ,\mu_n) and ordinals \beta_1, \ldots , \beta_n,\gamma \in X such that \alpha is the unique ordinal for which \models_{L_\gamma} \phi(\alpha^\circ,\beta_1^\circ, \ldots , \beta^\circ_n) where for all \alpha we define \alpha^\circ to be the name for \alpha within L_\gamma.

A structure \langle X, is eligible if and only if:

1. X \subseteq On.
3. \forall i, h_i is a partial function from X^{k(i)} to X, for some integer k(i).

If N=\langle X, is an eligible structure then N_\lambda is defined to be as before but with all occurrences of X replaced with X \cap \lambda.

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

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 M=\langle On, which satisfies the following conditions:

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

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

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

Skolem property. If \alpha is *definable from the set X \subseteq On, then \alpha \in M[X]; moreover there is an ordinal \lambda , uniformly \Sigma_1 definable from X \cup {\alpha}, such that \alpha \in M_\lambda[X].

References

::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::