From unary to binary numeral system

Question

I define a unary numeral system (for natural numbers greater than $0$) with digit $1$ (single unit) and unary operator $+_1$ (increment, left associative operator). Thus, as examples, the numbering 1 to 6 is:

\begin{align*} 1 \\ 1 +_1 \\ 1 +_1 +_1 \\ 1 +_1 +_1 +_1 \\ 1 +_1 +_1 +_1 +_1 \\ 1 +_1 +_1 +_1 +_1 +_1 \end{align*}

Now I want to pass to a binary numbering system. I define unary operator $\times_2$, left associative and with the meaning of "duplicate". As examples, numbering 1 to 6 is:

\begin{align*} 1 \\ 1 \times_2 \\ 1 \times_2 ~ +_1 \\ 1 \times_2 \times_2 \\ 1 \times_2 \times_2 +_1 \\ 1 \times_2 +_1 \times_2 \end{align*}

[ Note operators applies to the left value, left associative, being $1 \times_2 +_1 \times_2 = ( ( 1 \times_2 ) +_1 ) \times_2$ ]

Definition of operator $\times_2$ is given by:

a) $ 1 +_1 = 1 \times_2 $

b) $a \times_2 +_1 +_1 = a +_1 \times_2 $ for any $a$

Questions:

• Is axiom b) mandatory ? can be it simplified ?

• Is this binary numeral system well defined or something more should be stated or defined in another way ( could be a more simple one ) ?

The only restriction is define and use only unary functions(operators).

Answer 1

Your revised axiom system allows you to prove all true equalities between (variable-free) terms in your language.

Namely, it proves that $1$ followed by any sequence of operators is equal to $1$ followed by some number of $+_1$s (and since it obviously doesn't prove any false statement, this must be the right number of $+_1$s): If there are any $\times_2$, look at the leftmost $\times_2$. If there's a $+_1$ to the left of it use axiom (b) to reduce the number of $+_1$s before it by one; if there's just a $1$ to the left of it, use axiom (a) to eliminate it. Then proceed by induction to eliminate the remaining $\times_2$s.

Furthermore, you can define a "binary representation" to mean a term that does not contain two $+_1$s in succession. We can then prove by induction on the total number of $+_1$s in the term that every term must equal a "binary representation".

You cannot prove from your axioms alone that every element has at most one binary representation; after all the axioms are satisfied in a model with only one element where $+_1$ and $\times_2$ are both the identity.

You can prove as a metatheorem that no two different binary representations can be proved to be equal, but the straightforward way to do that involves semantics: already knowing how the usual naturals work at the metalevel, show that $(\mathbb N_+,x\mapsto x+1,x\mapsto x+x)$ is a model and argue that the ordinary binary representation of a number is unique.

Answer 2

Writing $n+1$ for $n+_1$ and $f(n)$ for $n\times_2$, you're simply inductively defining a function on $\mathbb N$ by using a recurrence relation. Your axiom (b) simply says $f(n+1)=f(n)+1+1$. Of course it's mandatory - axiom (a) just says $f(1)=1+1$. You can't define a sequence by just defining its first term.

Axiom (b) is certainly about as simple as it's going to get - you're directly defining $f(n+1)$ in terms of $f(n)$.