[FOM] 308:Large large cardinals

[Robert M. Solovay]

In a recent posting, Joe Shipman asks:

How do you express

"the existence of a nontrivial elementary embedding j:V into M, where
V(lambda)
containedin M."

as a statement or scheme in ZFC, that refers only to sets and not
classes?

**********************************************************************

 	A good reference for this is Theorem 1.3 of the paper by Rich 
Laver "Implications between strong large cardinal axioms" (Annals of Pure 
and Applied Logic v. 90 (1997) 79-90.) [The cited theorem appears on page 
83.]

 	Laver gives six equivalents of the statement JS asks about. Five 
of them are assertions which are sentences of ZFC,

 	The general context is that j is an elementary embedding of 
V_lambda into itself which is not the identity; lambda is a limit ordinal 
[necessarily of cofinality omega].

 	Let kappa_0 be the critical point of j and for n > 0 define 
kappa_n inductively to be j(kappa_{n-1}). Define a measure mu_n on 
P(kappa_n) by letting mu(A) = 1 (for A subseteq P(kappa_n)) iff j"kappa_n 
\in j(A). If n >= m then there is a natural map of P(kappa_n) onto 
P(kappa_m) (X --> X \cap kappa_m). It is easy to check that this map 
projects mu_n onto mu_m.

 	We say that the tower of measures <mu_i :i in omega> is complete 
if whenever <A_n : n in omega> is a sequence of sets such that mu_n(A_n) = 
1 for all n in omega then there is a set X \subseteq lambda such that X 
\cap kappa_n is in A_n for all n in omega.

 	Then the axiom Shipman mentions is equivalent to:

There is a j:V_lambda --> V_lambda (non-trivial, elementary and with 
lambda of cof omega) such that the associated tower of measures is 
complete.

(This is (ii) on Laver's list.)

 	We can describe how the elementary embedding of the axiom arises 
from the tower thus.

We have a direct limit:

V --> Ult(V, mu_0) --> Ult(V, mu_1) ...

 	The direct limit is well-founded iff the tower is complete. The 
obvious map of V into the direct limit is the elementary embedding of the 
axiom in question.

 	--Bob Solovay