# A Peano system with an infinite initial segment

Let $$T$$ be a binary tree with the lexicographic order. And $$f:T→T$$ be the successor operation. We denote the empty sequence in $$T$$ by $$i$$. Also Suppose that:

For all $$X⊂T$$ if these two conditions hold:

1. $$i∈X$$
2. For all $$t$$, it holds that $$(t∈X →f(t)∈X)$$

Then $$X=T$$.

In $$\text{RCA}_0$$, I want to show that if $$T$$ has an infinite initial segment, then $$(T,i,f)$$ cannot be isomorphic to $$(ℕ,0,S)$$; which means there is no bijection such $$G:T→ℕ$$ satisfying these conditions:

1. $$G(i)=0$$
2. For all $$t∈T$$, it holds that $$G(f(t))=S(G(t))$$

How can I show this?

Let $$Y$$ be an infinite initial segment in $$T$$ and by contradiction, suppose that there exists a desirable function $$G$$. Then, $$\text{card}(G(Y))$$ has to be equal to $$\text{Card}(Y)$$. But in the other hand, $$G(Y)$$ is an initial segment of $$ℕ$$ which has to be finite. Contradiction.

But the problem is, I couldn't prove that $$G(Y)$$ is an initial segment of $$ℕ$$.

Maybe you want to say that such $$(T,i,f)$$ with an infinite initial segment doesn't even exist! Yes if we assume weak konig lemma, you are right. But in this context, we are assuming that weak konig lemma doesn't hold, then such $$(T,i,f)$$ with an infinite initial segment exists, by this argument:

If we assume that weak konig lemma doesn't hold, then there is an infinite binary tree $$T'$$ with no infinite path. We define $$T=T'∪S$$ which

$$S=\{t=\langle 1,1,...,1 \rangle : \text{lh}(t)=n \;\text{and}\; n∈ℕ\}$$

$$T$$ is a tree. consider the lexicographic order on $$T$$, and let $$f:T→T$$ be the successor operation, and let i be the empty sequence in $$T$$. Then $$(T,i,f)$$ is a Peano system (in particular, induction assumption holds) with an infinite initial segment. In fact, $$T'$$ is an infinite initial segment of $$T$$.

Now I want to show that $$(T,i,f)$$ is not isomorphic to $$(ℕ,0,S)$$.

The definition of initial segment that I have in mind:

$$Y$$ is an initial segment of $$T$$ iff there exists $$s∈T$$ such that $$Y={t∈T : t.

The lexicographic order that I have in mind:

Given two different binary sequence "s" and "t". We compare $$t(0)$$ and $$s(0)$$. If $$t(0), then $$t. If $$s(0) then $$s. If $$s(0)=t(0)$$, then we compare $$s(1)$$ and $$t(1)$$ and so on. If $$\text{lh}(t)<\text{lh}(s)$$ and for all $$i<\text{lh}(t)$$, $$t(i)=s(i)$$, then $$t. For example: $$000<01$$, $$01<1$$, $$1101<11010$$ etc.