2進法で数を表すことは、計算機における計算の基礎です。形式的には、2進法は0と1の2つの文字からなる列を数に対応させる関数です。
ところで、2進法で任意の自然数を表現できることは自明ではありません。加えて、各自然数について2進法での表現が一意になるという点も自明ではありません。(ここでは位取り記数法での有限の01列に限って考え、無限列は考えません。)
こういった2進法の前提となる事実は、どの自然数もいくつかの相異なる2の冪乗の和で表せることから導かれます。すなわち、任意の自然数\(n\)について、次を満たす非負整数の有限集合\(K_n\)が一意に存在します: \[n = \sum_{k \in K_n} 2^k.\]
まず次の補題が成り立つことに注意します(帰納法で簡単に証明できます): 任意の非負整数\(i\)について\[2^i = 1 + \sum_{j = 0}^{i-1} 2^j.\]
帰納法により\(K_n\)の存在が証明できます。\(n = 1\)の場合は\(K_n = \{0\}\)です。\(n = m + 1\)の場合、帰納法の仮定より\(m\)に対して\(m = \sum_{k \in K_m} 2^k\)となる\(K_m\)が存在します。\(K_m\)に含まれない最小の非負整数\(k_0\)を取ると、補題から\(K_n = \{k_0\} \cup \{k \in K_m \mid k_0 < k\}\)と求められます。
一方、\(K_n\)の一意性は次の命題から導かれます。非負整数の有限集合\(K, K'\)について、\(K \neq K'\)なら\(\sum_{k \in K} 2^k \neq \sum_{k' \in K'} 2^{k'}.\)実際、\(L := K \setminus K'\)、\(L' := K' \setminus K\)とおくと、空でない\(L \cup L'\)中の最大の要素\(l^{*}\)は、一般性を失わずに\(L\)に属すると仮定できます。このとき\(L'\)の各要素は\(l^{*}\)より小さいので、補題から\(\sum_{l \in L} 2^l \geq 2^{l^{*}} > \sum_{l' \in L'} 2^{l'}\)となって題意が示されます。