Laver function


In set theory, a Laver function is a function connected with supercompact cardinals.

Definition

If κ is a supercompact cardinal, a Laver function is a function ƒ:κ → Vκ such that for every set x and every cardinal λ ≥ |TC| + κ there is a supercompact measure U on <κ such that if j U is the associated elementary embedding then j U = x.

Applications

The original application of Laver functions was the following theorem of Laver.
If κ is supercompact, there is a κ-c.c. forcing notion such after forcing with 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.