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.
An ordinal α is *definable from a class of ordinals X if and only if there is a formula ϕ ( μ 0 , μ 1 , … , μ n ) and ∃ β 1 , … , β n , γ ∈ X such that α is the unique ordinal for which ⊨ L γ ϕ ( α ∘ , β 1 ∘ , … , β n ∘ ) where for all α we define α ∘ to be the name for α within L γ .
A structure ⟨ X , < , ( h i ) i < ω ⟩ is eligible if and only if:
- X ⊆ O n .
- < is the ordering on On restricted to X.
- ∀ i , h i is a partial function from X k ( i ) to X, for some integer k(i).
If N = ⟨ X , < , ( h i ) i < ω ⟩ is an eligible structure then N λ is defined to be as before but with all occurrences of X replaced with X ∩ λ .
Let N 1 , N 2 be two eligible structures which have the same function k. Then we say N 1 ◃ N 2 if ∀ i ∈ ω and ∀ x 1 , … , x k ( i ) ∈ X 1 we have:
h i 1 ( x 1 , … , x k ( i ) ) ≅ h i 2 ( x 1 , … , x k ( i ) )
A Silver machine is an eligible structure of the form M = ⟨ O n , < , ( h i ) i < ω ⟩ which satisfies the following conditions:
Condensation principle. If N ◃ M λ then there is an α such that N ≅ M α .
Finiteness principle. For each λ there is a finite set H ⊆ λ such that for any set A ⊆ λ + 1 we have
M λ + 1 [ A ] ⊆ M λ [ ( A ∩ λ ) ∪ H ] ∪ { λ } Skolem property. If α is *definable from the set X ⊆ O n , then α ∈ M [ X ] ; moreover there is an ordinal λ < [ s u p ( X ) ∪ α ] + , uniformly Σ 1 definable from X ∪ { α } , such that α ∈ M λ [ X ] .
