Laver function

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

If κ is a supercompact cardinal, a Laver function is a function ƒ:κ → 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(ƒ)(κ) = x.

(Here Vκ denotes the κ-th level of the cumulative hierarchy, TC(x) is the transitive closure of x) The original application of Laver functions was the following theorem of Laver.

There are many other applications, for example the proof of the consistency of the proper forcing axiom.

This set theory-related article is a stub.