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.