Silver machine

From Infogalactic: the planetary knowledge core
Jump to: navigation, search

<templatestyles src="Module:Hatnote/styles.css"></templatestyles>

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 \exists \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, < , (h_i)_{i<\omega} \rangle is eligible if and only if:

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

If N=\langle X, < , (h_i)_{i<\omega} \rangle 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, < , (h_i)_{i<\omega} \rangle 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 < [sup(X) \cup \alpha]^+, uniformly \Sigma_1 definable from X \cup \{\alpha\}, such that \alpha \in M_\lambda[X].

References

  • Lua error in package.lua at line 80: module 'strict' not found. - Please note that errors have been found in some results in this book concerning Kripke Platek set theory.