Silver machine explained

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

\alpha

is *definable from a class of ordinals X if and only if there is a formula

\phi(\mu0,\mu1,\ldots,\mun)

and ordinals

\beta1,\ldots,\betan,\gamma\inX

such that

\alpha

is the unique ordinal for which
\models
L\gamma
\circ,
\phi(\alpha
1

\ldots,

\circ
\beta
n)
where for all

\alpha

we define

\alpha\circ

to be the name for

\alpha

within

L\gamma

.

A structure

\langleX,<,(hi)i<\omega\rangle

is eligible if and only if:

X\subseteqOn

.
  1. < is the ordering on On restricted to X.

\foralli,hi

is a partial function from

Xk(i)

to X, for some integer k(i).

If

N=\langleX,<,(hi)i<\omega\rangle

is an eligible structure then

Nλ

is defined to be as before but with all occurrences of X replaced with

X\capλ

.

Let

N1,N2

be two eligible structures which have the same function k. Then we say

N1\triangleleftN2

if

\foralli\in\omega

and

\forallx1,\ldots,xk(i)\inX1

we have:
1(x
h
1,

\ldots,xk(i))\cong

2(x
h
1,

\ldots,xk(i))

Silver machine

A Silver machine is an eligible structure of the form

M=\langleOn,<,(hi)i<\omega\rangle

which satisfies the following conditions:

Condensation principle. If

N\triangleleftMλ

then there is an

\alpha

such that

N\congM\alpha

.

Finiteness principle. For each

λ

there is a finite set

H\subseteqλ

such that for any set

A\subseteqλ+1

we have

Mλ+1[A]\subseteqMλ[(A\capλ)\cupH]\cup\{λ\}

Skolem property. If

\alpha

is *definable from the set

X\subseteqOn

, then

\alpha\inM[X]

; moreover there is an ordinal

λ<[sup(X)\cup\alpha]+

, uniformly

\Sigma1

definable from

X\cup\{\alpha\}

, such that

\alpha\inMλ[X]

.

References