How can we argue that any binary number plus $1$ is a binary number?

Question

I am working with the definition of a binary number $n$ to be $$ n=c_k \cdot 2^k+c_{k-1} \cdot 2^{k-1}+\cdots+c_1 \cdot 2^1+c_0 \cdot 2^0 $$ where $k \in \mathbb{N}$ and $c_i \in\{0,1\}$ for all $i \leq k$.

I am working on a strong inductive proof that every natural number has a binary representation which uses the argument that a binary number $+1$ is a binary number. I have tried to justify this by saying that when we add $2^0$ to $n$, it will keep combining with terms until eventually a coefficient of a power of $2$ is $0$, and this number "settles in" to the sum defined to be a binary number (as if there is a $1 \cdot 2^0$ in the sum given in the definition, adding $2^0$ will get $2^1$, which in turn could combine with a $2^1 $ to produce a $2^2$, etc.). However, this argument is very informal and I am not sure if it is valid due to not being able to formalize it. How could we argue that a binary number $+1$ is a binary number?`

Answer 1

If you really intend to prove things in a very formal way, you can prove that for $n = c_k 2^k + \cdots + c_0 2^0$, if you take $$i := \min \{ j | c_j = 0 \}$$ you have if $i \neq k$ $$n+1 = c_k 2^k + \cdots + c_i 2^i$$ And if $i = k$: $$n+1 = c_{k+1} 2^{k+1} $$

But it is not really mandatory if you get how adding $1$ works.

Answer 2

If you really want to use strong induction rather than simple induction, you don't need to worry about $+1$. Instead, assume that every positive integer $< n$ is a binary number $c_k 2^k + \ldots + c_0$ with $c_k = 1$. Let $k$ be the greatest integer such that $n \ge 2^k$ (use another induction to show that such $k$ exists). If $n = 2^k$, then that is a binary number with $c_i = 0$ for $i < k$ and $c_k = 1$. Otherwise, $m = n - 2^k$ is a positive integer $< n$ so by the induction hypothesis it is a binary number $c^j 2^j + \ldots + c_0$ with $c_j = 1$. Since $n < 2^{k+1} $, $m = n - 2^k < 2^k$, and $j < k$. Then $n = 2^k + c_j 2^j + \ldots + c_0$ is a binary number.