In set theory, a code for a hereditarily countable set

x ∈ H ℵ 1 {\displaystyle x\in H_{\aleph _{1}}\,}

is a set

E ⊂ ω × ω {\displaystyle E\subset \omega \times \omega }

such that there is an isomorphism between ( ω , E ) {\displaystyle (\omega ,E)} and ( X , ∈ ) {\displaystyle (X,\in )} where X {\displaystyle X} is the transitive closure of { x } {\displaystyle \{x\}}. If X {\displaystyle X} is finite (with cardinality n {\displaystyle n}), then use n × n {\displaystyle n\times n} instead of ω × ω {\displaystyle \omega \times \omega } and ( n , E ) {\displaystyle (n,E)} instead of ( ω , E ) {\displaystyle (\omega ,E)}.

According to the axiom of extensionality, the identity of a set is determined by its elements. And since those elements are also sets, their identities are determined by their elements, etc.. So if one knows the element relation restricted to X {\displaystyle X}, then one knows what x {\displaystyle x} is. (We use the transitive closure of { x } {\displaystyle \{x\}} rather than of x {\displaystyle x} itself to avoid confusing the elements of x {\displaystyle x} with elements of its elements or whatever.) A code includes that information identifying x {\displaystyle x} and also information about the particular injection from X {\displaystyle X} into ω {\displaystyle \omega } which was used to create E {\displaystyle E}. The extra information about the injection is non-essential, so there are many codes for the same set which are equally useful.

So codes are a way of mapping H ℵ 1 {\displaystyle H_{\aleph _{1}}} into the powerset of ω × ω {\displaystyle \omega \times \omega }. Using a pairing function on ω {\displaystyle \omega } such as ( n , k ) ↦ ( n 2 + 2 n k + k 2 + n + 3 k ) / 2 {\displaystyle (n,k)\mapsto (n^{2}+2nk+k^{2}+n+3k)/2}, we can map the powerset of ω × ω {\displaystyle \omega \times \omega } into the powerset of ω {\displaystyle \omega }. And we can map the powerset of ω {\displaystyle \omega } into the Cantor set, a subset of the real numbers. So statements about H ℵ 1 {\displaystyle H_{\aleph _{1}}} can be converted into statements about the reals. Therefore, H ℵ 1 ⊂ L ( R ) {\displaystyle H_{\aleph _{1}}\subset L(R)}, where L(R) is the smallest transitive inner model of ZF containing all the ordinals and all the reals.

Codes are useful in constructing mice.