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.
α
is *definable from a class of ordinals X if and only if there is a formula
β
β
α
is the unique ordinal for which
γ
α
α
α
α
γ
is an eligible structure then
λ
is defined to be as before but with all occurrences of X replaced with
be two eligible structures which have the same function k. Then we say
A Silver machine is an eligible structure of the form
which satisfies the following conditions: Condensation principle.
α
α
Finiteness principle.
there is a finite set
we have Skolem property.
α
is *definable from the set
α ∈
) ∪ α
∪ { α }
α ∈