Laver function

In set theory, a Laver function (or Laver Diamond, named after its inventor, Richard Laver) is a function connected with supercompact cardinals.

Definition

If κ is a supercompact cardinal, a Laver function is a function f:κ→V_κ such that for every set x and every cardinal λ≥|TC(x)|+κ there is a supercompact measure U on [λ]^{<κ such that if j_U is the associated elementary embedding then j_U(f)(κ)=x. (Here V_κ denotes the κ-th level of the cumulative hierarchy, TC(x) is the transitive closure of x)}

Applications

The original application of Laver functions was the following theorem of Laver. If κ is supercompact, there is a κ-c.c. forcing notion (P,≤) such after forcing with (P,≤) the following holds: κ is supercompact and remains supercompact after forcing with any κ-directed closed forcing.

There are many other applications, for example the proof of the consistency of the Proper Forcing Axiom.

Reference

• R. Laver: Making the supercompactness of κ indestructible under κ-directed closed forcing, Israel Journal of Mathematics, 29(1978), 385-388.