{{short description|Type of mathematical object}} {{About|the kind of mathematical object|the Hawkwind song|Silver Machine|the Vapors song|Silver Machines}} {{Multiple issues| {{notability|date=June 2020}} {{technical|date=June 2020}} }}
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 <math>\alpha</math> is ''*definable'' from a class of ordinals X if and only if there is a formula <math>\phi(\mu_0,\mu_1, \ldots ,\mu_n)</math> and ordinals <math>\beta_1, \ldots , \beta_n,\gamma \in X </math> such that <math>\alpha</math> is the unique ordinal for which <math>\models_{L_\gamma} \phi(\alpha^\circ,\beta_1^\circ, \ldots , \beta^\circ_n)</math> where for all <math>\alpha</math> we define <math>\alpha^\circ</math> to be the name for <math>\alpha</math> within <math>L_\gamma</math>.
A structure <math>\langle X, < , (h_i)_{i<\omega} \rangle</math> is ''eligible'' if and only if:
# <math>X \subseteq On</math>. # < is the ordering on On restricted to X. # <math>\forall i, h_i</math> is a partial function from <math>X^{k(i)}</math> to X, for some integer k(i).
If <math>N=\langle X, < , (h_i)_{i<\omega} \rangle</math> is an eligible structure then <math>N_\lambda</math> is defined to be as before but with all occurrences of X replaced with <math>X \cap \lambda</math>.
Let <math>N^1, N^2</math> be two eligible structures which have the same function k. Then we say <math>N^1 \triangleleft N^2</math> if <math>\forall i \in \omega</math> and <math>\forall x_1, \ldots , x_{k(i)} \in X^1</math> we have:
<math>h_i^1(x_1, \ldots , x_{k(i)}) \cong h_i^2(x_1, \ldots , x_{k(i)})</math>
==Silver machine== A Silver machine is an eligible structure of the form <math>M=\langle On, < , (h_i)_{i<\omega} \rangle</math> which satisfies the following conditions:
''Condensation principle.'' If <math>N \triangleleft M_\lambda</math> then there is an <math>\alpha</math> such that <math>N \cong M_\alpha</math>.
''Finiteness principle.'' For each <math>\lambda</math> there is a finite set <math>H \subseteq \lambda</math> such that for any set <math>A \subseteq \lambda +1</math> we have
: <math>M_{\lambda+1}[A] \subseteq M_\lambda[(A \cap \lambda) \cup H] \cup \{\lambda\}</math>
''Skolem property.'' If <math>\alpha</math> is *definable from the set <math>X \subseteq On</math>, then <math>\alpha \in M[X]</math>; moreover there is an ordinal <math>\lambda < [sup(X) \cup \alpha]^+</math>, uniformly <math>\Sigma_1</math> definable from <math>X \cup \{\alpha\}</math>, such that <math>\alpha \in M_\lambda[X]</math>.
==References== *{{cite book | title=Constructibility | chapter=Chapter IX | author=Keith J Devlin | author-link=Keith Devlin | isbn= 0-387-13258-9 | year = 1984}}
Category:Constructible universe