# Collatz conjecture becomes theorem

Grażyna Mirkowska
UKSW University of Warsaw
Institute of Informatics  Andrzej Salwicki
Dombrova Research
Łomianki, Poland
salwicki at mimuw.edu.pl

(October 18, 2023)

###### Abstract

The Collatz hypothesis is a theorem of the algorithmic theory of natural
numbers. We prove the (algorithmic) formula that expresses the halting
property of Collatz algorithm.
The observation that Collatz’s theorem cannot be proved in any elementary
number theory completes the main result.

Key words: algorithm of Collatz, halting property, Collatz tree, calculus of
programs.

MSC-class: 03D02 (Primary) 68Q02 (Secondary)
ACM-class: F.3.1; D.2.4

###### Contents

  1. 1 Introduction
  2. 2 Collatz tree
  3. 3 Four algorithms, relatives of $Cl$ algorithm
    1. 3.1 Hotel Collatz
  4. 4 On finite and infinite computations of Collatz algorithm
    1. 4.1 Finite computations
    2. 4.2 Infinite computations
    3. 4.3 Collatz theorem
    4. 4.4 A counterexample
  5. 5 Final remarks
    1. 5.1 Historical remarks
  6. 6 Suplements
    1. 6.1 A structure with counterexamples
    2. 6.2 Presburger arithmetic
    3. 6.3 An introduction to calculus of programs $\mathcal{AL}$
    4. 6.4 An introduction to algorithmic theory of natural numbers $\mathcal{ATN}$
    5. 6.5 Proof of lemma 4
    6. 6.6 Proof of invariant of algorithm $Gr3$

##  1 Introduction

The $3x+1$ problem remained open for over 80 years. It has been noticed in
1937 by Lothar Collatz. The problem became quite popular due to its wording,
for it is short and easy to comprehend.
Collatz remarked that for any given natural number $n>0$ , the sequence
$\\{n_{i}\\}$ defined by the following recurrence

$\left.\begin{array}[]{l}n_{0}=n\\\ n_{i+1}=\begin{cases}n_{i}\div 2&\mbox{
when $n_{i}$ is even}\\\ 3\cdot n_{i}+1&\mbox{ when $n_{i}$ is
odd}\end{cases}\quad\mbox{ for }\ i\geq 0\end{array}\right\\}$

seem always reach the value 1.
He formulated the following conjecture

$\text{for all }n\ \text{exists }i\ \text{such that }n_{i}=1$

One can give another formulation of the hypothesis of Collatz 111Let
$f(n,0)\stackrel{{\scriptstyle df}}{{=}}n$ , and
$f(n,i+1)\stackrel{{\scriptstyle df}}{{=}}\begin{cases}f(n,i)/2&\text{if
$f(n,i)$ is even}\\\ 3\cdot f(n,i)+1&\text{if $f(n,i)$ is odd}\end{cases}$.
Now, conjecture reads $\forall_{n}\,\exists_{i}\,f(n,i)=1$..
The number of papers devoted to the problem surpasses 200, c.f. [Lag10] . It
is worthwhile to consult social media: wikipedia, youtube etc, there you can
find some surprising ideas to prove the Collatz hypothesis as well as a
technical analysis of the problem.
Computers are used and are still crunching numbers in the search of an
eventual counterexample to the Collatz conjecture. The reports on progress
appear each year. We claim that the counterexample approach is pointless, i.e.
the computers can be turned off. Namely, we shall prove that the program that
searches a counterexample will never stop.
Our goal will be achieved if we prove that for each number $n$ the computation
of the following $Cl$ algorithm is finite.

$\left\\{\begin{array}[]{l}\textbf{while}\ n\neq 1\ \textbf{do}\\\
\quad\textbf{if}\ even(n)\ \textbf{then}\ n:=n\div 2\ \textbf{else}\ n:=3n+1\
\textbf{fi}\\\ \textbf{od}\end{array}\right\\}$ (Cl)

One needs

  * •

a formula $\Theta_{Cl}$ such that it expresses the termination property of
program $Cl$,

  * •

a verifiable proof $\Pi$ of the formula and

  * •

a definition of relation $\mathcal{C}$ of deducibility.

Ah, we need also a specification of the domain in which the algorithm is to be
executed, i.e. the axioms $\mathcal{A}x$ of the algebraic structure of natural
numbers.
Question 1. How to express the termination property of a program $K$ as a
formula $\Theta_{K}$ (i.e. a Boolean expression)?
Note, there is no a universal algorithm that expresses the halting property of
a given program $K$ by an appropriate first-order logical formula
$\Theta_{K}$. First, let us recall the theorem on incompleteness of
arithmetics, cf. Kurt Gödel . According to Gödel, the property to be a natural
number is not expressible by any set of first-order formulas. The reader may
wish to note, that halting property of the algoritm

$q:=0;\textbf{while}\ q\neq n\ \textbf{do}\ q:=q+1\ \textbf{od}$

is valid in a data structure iff $n$ is a standard (i.e. reachable) natural
number. Therefore the halting property allow to define the set of natural
numbers. In this situation it seems natural to pass from first-order language
to another more expressive language. There are three candidates: 1°a second-
order language admitting variables and quantifiers over sets, 2°the language
of infinte disjunctions and conjunctions $\mathcal{L}_{\omega_{1}\omega}$ and
3°language of algorithmic logic. Problem with second order logic is in lack of
adequate definition of consequence operation. True, we can limit our
considerations to the case of finite sets (aka, weak second order logic).
Still we do not know a complete set of axioms and inference rules for the weak
second-order logic. Applying second-order logic to program analysis results in
a heavy overhead. Because first you have to translate the semantic property of
the program into a property of a certain sequence or set. prove this property
and make a backward translation. The question of whether this approach is
acceptable to software engineers seems to be appropriate.
The language of infinite disjunctions and conjunctions is not an acceptable
tool for software engeeners.
We shall use the language and the consequence operation offered by algorithmic
logic i.e. calculus of programs. We enlarge the set of well formed
expressions: beside terms and formulas of first order language we accept
algorithms and we modify the definition of logical formulas. The simplest
algorithmic formulas are of the form:
$\langle\textit{algorithm}\rangle\langle\textit{formula}\rangle$.
As an example of an algorithmic formula consider the expression

$\forall_{n}\\{q:=0;\textbf{while}\ q\neq n\ \textbf{do}\ q:=q+1\
\textbf{od}\\}\,(n=q)$

The latter formula is valid iff every element $n$ can be reached from 0 by
adding 1.
Now our goal is to prove the following formula

$\forall_{n\in N}\,\left\\{\begin{array}[]{l}\mathbf{while}\ n\neq 1\
\mathbf{do}\\\ \quad\mathbf{if}\ even(n)\ \textbf{then}\ n:=\frac{n}{2}\\\
\quad\mathbf{else}\ n:=3n+1\ \mathbf{fi}\\\
\mathbf{od}\end{array}\right\\}(n=1)$ ($\Theta$)

from the axioms of algorithmic theory of natural numbers $\mathcal{ATN}$, c.f.
subsection 6.4. For the formula ($\Theta$) expresses the termination property
of program $Cl$.
Question 2. How to prove such algorithmic formula?
Note, all structures that assure the validity of axioms of the $\mathcal{ATN}$
theory are isomorphic (this is the categoricity meta-theorem). Therefore, the
termination formula, can be either proved (with the inference rules and axioms
of calculus of programs $\mathcal{AL}$, or validated in this unique model of
axioms of $\mathcal{ATN}$.
Let us make a simple observation. The computation of Collatz algorithm if
succesful goes through intermediate values. The following diagram (Dg)
illustrates a computation where all odd numbers were exposed as stacked
fractions.

$n\rightarrow\dfrac{n}{2^{k_{0}}}\rightarrow\dfrac{3*(\dfrac{n}{2^{k_{0}}})+1}{2^{k_{1}}}\rightarrow\dfrac{3*\dfrac{3*\dfrac{n}{2^{k_{0}}}+1}{2^{k_{1}}}+1}{2^{k_{2}}}\dots\rightarrow\frac{3\cdot\frac{3\cdot\frac{3\cdot\frac{3\cdot\frac{\biggl{.}3\cdot\frac{n}{2^{k_{0}}}\biggr{.}+1}{2^{k_{1}}}+1}{2^{k_{2}}}+1}{\bigl{(}\
\dots\ \bigr{)}}+1}{2^{k_{x-1}}}+1}{2^{k_{x}}}=1$ (Dg)

where
$k_{0}=expo(n,2),k_{1}=expo(3\cdot\frac{n}{2^{k_{0}}}+1,2),k_{2}=expo(3*\frac{(3\cdot\frac{n}{2^{k_{0}}}+1)}{2^{k_{1}}}+1,2),\dots$
222Note, the function $expo$ returns the largest exponent of 2 in the prime
factorization of number $x$ .
$expo(x,2)\stackrel{{\scriptstyle df}}{{=}}\\{l:=0;y:=x;\textbf{while}\
even(y)\ \textbf{do}\ l:=l+1;\,y:=y/2\ \textbf{od}\\}(\mathrm{result}=l)$ i.e.
$l=expo(x,2)$ . We introduce the notation $expo$ instead $exp$ for our friends
programmers who interpret the notation $exp$ as exponentiation. . In our
earlier paper [MS21] we studied the halting formula of the Collatz algorithm.
We remarked that the computation of Collatz algorithm is finite iff there
exist three natural numbers $x,y,z$ such that:
a) the equation $n\cdot 3^{x}+y=2^{z}$ is satisfied and
b) the computation of another algorithm $IC$, cf. page 17, is finite, the
algorithm computes on triples$\langle x,y,z\rangle$.
It is worthwhile to mention that the subsequent triples are decreasing during
computation.
The proof we wrote there [MS21] is overly complicated.
Here we show that the 4-argument relation

$\\{n,x,y,z\\}:\\{IC\\}(true).$

is elementary recursive, since it may be expressed by an arihmetic expression
with operator $\sum$.
The present paper shows arguments simpler and easier to follow.

##  2 Collatz tree

###### Definition 1

Collatz tree $\mathcal{DC}$ is a subset $D\subset N$ of the set $N$ of natural
numbers and the function $f$ defined on the set $D\setminus\\{0,1\\}$.

$\mathcal{DC}=\langle D,f\rangle$

where $D\subset N,1\in D,f\colon D\setminus\\{0,1\\}\rightarrow D$.
Function $f$ is determined as follows

$f(n)=\begin{cases}n\div 2&\mbox{when }n\mod 2=0\\\ 3n+1&\mbox{when }n\mod
2=1\land n\neq 1\end{cases}$

, the set $D$ is the least set containing the number 1 and closed with respect
to the function $f$,

$D=\\{n\in N:\exists_{i\in N}\ f^{i}(n)=1\ \\}\ .$

As it is easy to see, this definition is highly entangled and the decision
whether the set $D$ contains every natural number is equivalent to the Collatz
problem.

###### Remark 2

Set $D$ has the following properties :

$\displaystyle x\in D\implies(x+x)\in D$ (1) $\displaystyle\bigl{(}x\in
D\implies(\exists_{y}x=y+y\implies y\in D)\bigr{)}$ (2)
$\displaystyle\bigl{(}x\in D\implies(\exists_{y}x=y+y+1\implies(x+x+x+1)\in
D)\bigr{)}$ (3) $\displaystyle\bigl{(}x\in
D\implies(\exists_{e}\exists_{z}e=z+z+1\land x=e+e+e+1\implies e\in
D)\bigr{)}$ (4)

Implications (1) and (4) show left and right son of element $x$.

###### Conjecture 3

The Collatz tree contains all the reachable natural numbers.

$16$$32$
641282565121024204840968192163843276854611365273054603416821364272854569092274549081518517034068013602720544045390611322645290475150$21$4284168336672134426885376$5$$10$
$20$408016032064012802560512085321342685253106212424848141357014023132652104208416832691381734681361122$3$612244896192384768

Figure 1:  A fragment of Collatz tree, levels 4-15. It does not include levels
0-3, they consist of elements 1 — 2 — 4 — 8 — .

##  3 Four algorithms, relatives of $Cl$ algorithm

In this section we present an algorithm $Gr$ equivalent to the algorithm $Cl$
and three algorithms $Gr1,Gr2,Gr3$ that are successive extensions of the $Gr$
algorithm.

###### Lemma 4

The following algorithm $Gr$ is equivalent to Collatz algorithm $Cl$.

$Gr$:  while even(n) do n:= n $\div$ 2 od ; while n $\neq$1 do n:= 3*n+1;
while even(n) do n:= n $\div$ 2 od od ;
Proof. The equivalence of the algorithms $Cl$ and $Gr$ is intuitive. Compare
the recurrence of Collatz (1) and the following recurrence (3 ) that is
calculated by the algorithm $Gr$.

$\left.\begin{array}[]{rcl}k_{0}=expo(n,2)&\land&m_{0}=\frac{n}{2^{k_{0}}}\\\
k_{i+1}=expo(3m_{i}+1,2)&\
\land&m_{i+1}=\frac{3m_{i}+1}{2^{k_{i+1}}}\qquad\text{for}\ i\geq
0\end{array}\right\\}$

One can say the algorithm $Gr$ is obtained by the elimination of if
instruction from the $Cl$ algorithm. However, construction of a formal proof
is a non-obvious task. A sketch of a proof is given in subsection 6.5 We are
encouraging the reader to fill the details.
Next, we present the algorithm $Gr1$, an extension of algorithm $Gr$.
$Gr1$:  var  n,$l,i$ :integer ; $k,m$ :arrayof  integer; $\Gamma_{1}$:
$i:=0;\,l:=0;$ while even(n) do n:= n $\div$ 2; $l:=l+1$ od ;
$k_{i}:=l;\,m_{i}:=$n: while n $\neq$1 do $\Delta_{1}$:  { $m_{i}$=n
$\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\\}}\quad$n:=
3*n+1; $l:=0$; while even(n) do n:= n $\div 2;\ l:=l+1$od ; $k_{i+1}:=l;\
m_{i+1}:=$n;
$\\{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}m_{i+1}=\frac{3\cdot
m_{i}+1}{2^{K_{i}}}\land
k_{i+1}=exp(3*m_{i}+1,2)\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\\}}\quad\,i:=i+1$
od

###### Lemma 5

Algorithm $Gr1$ has the following properties:
(i) Algorithms $Gr$ and $Gr1$ are equivalent with respect to the halting
property.
(ii) The sequences $\\{m_{i}\\}$ and $\\{k_{i}\\}$ calculated by the algorithm
$Gr1$ satisfy the recurrence 3.

Proof. Both statements are very intuitive. Algorithm $Gr1$ is an extension of
algorithm $Gr$. The inserted instructions do not interfere with the halting
property of algorithm $Gr1$. Second part of the lemma follows easily from the
remark that $k_{0}=exp(\mathrm{n},2)$ and $m_{0}=\frac{n}{2^{k_{0}}}$ and that
for all $i>0$ we have $k_{i+1}=exp(3*m_{i}+1,2)$ and $m_{i+1}=\frac{3\cdot
m_{i}+1}{2^{k_{i+1}}}$.
Each odd number $m$ in Collatz tree, $m\in D$, initializes a new branch. Let
us give a color number $x+1$ to each new branch emanating from a branch with
color number $x$. Note, for every natural number$p$ the set of branches of the
color $p$ is infinite. Let $W_{x}$ denote the set of natural numbers that
obtained the color $x$.
Besides the levels of Collatz tree, one can distinguish the structure of
strata in the tree.

First, we define a congruence relation $\sim$ between numbers: given two odd
numbers $a$ and $b$ the relation $a\sim b$ holds iff $b=4a+1$, We take
symmetric and transitive closure of the relation $\sim$.
Further, if $a\sim b$ and two odd numbers $c,d$ are such $a=3c+1$ and $b=3d+1$
then $c\sim d$.

###### Definition 6

Definition of strata.  Strata $W_{0}$ consists of powers of two.

$W_{0}\ \stackrel{{\scriptstyle df}}{{=}}\ \\{n\in N\colon n=2^{expo(n,2)}\\}$

Any number $n\notin W_{0}$ belongs to some set $W_{x},x\neq 0$.

$W_{x+1}\stackrel{{\scriptstyle df}}{{=}}\ \bigl{\\{}n\in
N\colon\exists_{\,m\in W_{x}}\,(\
3\cdot\frac{n}{2^{expo(n,2)}}+1=m\,)\bigr{\\}}$

A couple of observations will be used in the sequel.

###### Remark 7

Among properties of sets $W_{i}$ we find

  1. 1.

Each set $W_{i}$ is infinite. If it contains a number $n$ then the number
$2n\in W_{i}$.

  2. 2.

The set $W_{0}$ contains one odd number 1. All other sets contain infinitely
many odd numbers. For if $a=2j+1$ and $a\in W_{i}$ then $4a+1\in W_{i}$.

  3. 3.

We define the function $f\colon N\rightarrow N$ as follow:
$f(n)=\begin{cases}n\div 2&\text{when}\ n\ \text{is even}\\\ 3n+1&\text{when}\
n\ \text{is odd}\ n\neq 1\\\ undefined&\text{when}\ n=1\\\ \end{cases}$

  4. 4.

Let $x>0$ be a natural number. Let the sequence $\left\\{o_{j}\right\\}_{i\in
N}$ contain all odd numbers that are in the set $W_{x}$. Let
$S_{o_{j}}=\left\\{2^{i}\cdot o_{j}\right\\}$ be the set. Every set $W_{x}$
may be partitioned as follow $W_{x}=\bigcup\limits_{j=0}^{\infty}\,S_{o_{j}}$.
If $j\neq j^{\prime}$ then $S_{o_{j}}\cap S_{o_{j^{\prime}}}=\emptyset$

  5. 5.

For every $i,j\in Nat$ if $i\neq j$ then $W_{i}\cap W_{j}=\emptyset$.

  6. 6.

For every $n,j\in Nat$ if $n\in W_{j}\land j>1\land n\mod 2=1$ then $3n+1\in
W_{j-1}$.

  7. 7.

The sequence of sets $\left\\{\bigcup\limits_{i=0}^{j}\,W_{i}\right\\}_{j\in
N}$ is monotone, increasing.

$16$$32$
641282565121024204840968192163843276854611365273054603416821364272854569092274549081518517034068013602720544045390611322645290475150$21$4284168336672134426885376$5$$10$
$20$408016032064012802560512085321342685253106212424848141357014023132652104208416832691381734681361122$3$612244896192384768

Figure 2: Strata $W_{0}--W_{4}$ of Collatz tree

Let $s$ be a variable not occurring in algorithm $Gr1$. The following lemma
states the partial correctnes of the algorithm $Gr1$ w.r.t. precondition $s=n$
and postcondition $s\in W_{i}$.

###### Lemma 8

Algorithm $Gr1$ computes the number $i$ of storey $W_{i}$ of number $n$,

$\\{Gr1\\}(true)\implies\bigl{(}(s=n)\implies\\{Gr1\\}(s\in W_{i})\bigr{)}$

Next, we present another algorithm $Gr2$ and a lemma.
$Gr2$:  var  n ,$l,i,x,y,z$ :integer ; k,m :arrayof  integer; $\Gamma_{2}$:
$i:=0;\ l:=0;$ while even(n) do n:= n $\div$ 2; $l:=l+1$ od ; $z,\,k_{i}:=l$;
$m_{i}$:=n; $y:=0$; while $m_{i}\neq$1 do $\Delta_{2}$:  n:= 3*n+1;
$i:=i+1;\,l:=0$ ; while even(n) do n:= n $\div$ 2; $l:=l+1$ od ; $k_{i}:=l$;
$m_{i}$:=n; $z:=z+k_{i};\,y:=3*y+2^{z};\,x:=i$ od

###### Lemma 9

Algorithm $Gr2$ has the following properties:
(i) Both algorithms $Gr1$ and $Gr2$ are equivalent with respect to the halting
property.
(ii) Formula $\varphi:\ \boxed{n\cdot 3^{i}+y=m_{i}\cdot 2^{z}}$ is an
invariant of the program $Gr2$ i.e. the formulas (5) and (6)

$\\{\Gamma_{2}\\}\,(n\cdot 3^{i}+y=m_{i}\cdot 2^{z})$ (5) $(n\cdot
3^{i}+y=m_{i}\cdot 2^{z})\implies\\{\Delta_{2}\\}(n\cdot 3^{i}+y=m_{i}\cdot
2^{z})$ (6)

are theorems of the algorithmic theory of numbers $\mathcal{ATN}$.

Proof. Proofs of these formulas are easy, it suffices to apply the axiom of
assignment instruction $Ax_{18}$,

$\langle 0,0,4\rangle_{16}$$\langle 0,0,5\rangle_{32}$ $\langle
0,0,6\rangle_{64}$$\langle 0,0,7\rangle_{128}$$\langle 0,0,8\rangle$$\langle
0,0,9\rangle$$\langle 0,0,10\rangle$$\langle 0,0,11\rangle$$\langle
0,0,12\rangle$$\langle 0,0,13\rangle$$\langle
0,0,14\rangle$327685461136527305460$\langle
1,1,10\rangle_{341}$682136427285456 909227454908151$\langle
1,1,8\rangle_{85}$170$\langle
1,4,10\rangle_{340}$68013602720544045390611322645290475150$\langle
1,1,6\rangle_{21}$4284168$\langle 1,16,10\rangle_{336}$672134426885376$\langle
1,1,4\rangle_{5}$$\langle 1,2,5\rangle_{10}$ $\langle
1,4,6\rangle_{20}$$\langle 1,8,7\rangle_{40}$$\langle
1,16,8\rangle_{80}$$\langle 1,32,9\rangle_{160}$$\langle
1,64,10\rangle_{320}$640128025605120853213426852$\langle
2,35,9\rangle_{53}$106212424848141357014023$\langle
2,11,7\rangle_{13}$$\langle 2,22,8\rangle_{26}$$\langle
2,44,9\rangle_{52}$10420841683269138$\langle 3,53,9\rangle$$\langle
3,106,10\rangle_{34}$68136$\langle 4,133,10\rangle_{11}$22$\langle
2,5,5\rangle_{3}$$\langle 2,10,6\rangle_{6}$$\langle
2,20,7\rangle_{12}$$\langle 2,40,8\rangle_{24}$$\langle
2,80,9\rangle_{48}$96192384768

Figure 3:  Tree of triples (levels 4 – 15)

Subsequent algorithm $Gr3$ exposes the history of the calculations of $x,y,z$.
$Gr3$:  var n,$i,$aux :integer ; k,m,X,Y,Z : arrayof  integer; $\Gamma_{3}$:
$i:=0;\,k_{i}:=exp(\mathrm{n},2);\,m_{i}:=\frac{\mathrm{n},}{2^{k_{i}}};\,Z_{i}:=k_{0};\,Y_{i},X_{i}:=0;$
while $n\cdot 3^{i}+Y_{i}\neq 2^{Z_{i}}$ do $\Delta_{3}$:  aux:=3*$m_{i}$+1;
$i:=i+1$ ; $k_{i}:=exp($aux$,2);\ m_{i}:=$aux$/2^{k_{i}}$;
$Y_{i}:=3Y_{i-1}+2^{Z_{i-1}};\ Z_{i}:=Z_{i-1}+k_{i};\ X_{i}:=i$; od
See some properties of the algorithm $Gr3$.

###### Lemma 10

Both algorithms $Gr2$ and $Gr3$ are equivalent with respect to the halting
property.
For every element $n$ after each $i$-th iteration of algoritm $Gr3$, the
following formulas are satisfied

$\begin{array}[]{lll}\hline\cr\varphi:\ n\cdot 3^{i}+Y_{i}=m_{i}\cdot
2^{Z_{i}}&&X_{i}=i\\\
Z_{i}=\sum\limits_{j=0}^{i}\,k_{j}&&Y_{i}=\sum\limits_{j=0}^{i-1}\biggl{(}3^{i-1-j}\cdot
2^{Z_{j}}\biggr{)}\\\ \hline\cr\end{array}$

where the sequences $\\{m_{i}\\}$and $\\{k_{i}\\}$ are determined by the
recurrence (3).
in other words, the following formula is valid in the structure $\mathfrak{N}$

$\mathfrak{N}\models\Gamma_{3}\bigcap\,\\{\mathbf{if}\ m_{i}\neq 1\
\mathbf{then}\ \Delta_{3}\ \mathbf{fi}\\}\,\varphi$

###### Remark 11

Hence, for every element $n$ algorithm $Gr3$ calculates an increasing,
monotone sequence of triples $\langle i\,(=X_{i}),Y_{i},Z_{i}\rangle$.

###### Remark 12

We can say informally that the algorithm $Gr3$ performs as follow
$i:=0$; while $n\notin W_{i}$ do $i:=i+1$ od

Note, $\left\\{Gr_{3}\right\\}(n\in W_{i})$

###  3.1 Hotel Collatz

Hotel contains rooms of any natural number. Let $n=2^{i}\cdot(2j+1)$ . It
means that the room number $n$ is located in tower number $j$ on the floor
number $i$ . Each tower is equipped with an elevator (shown as a green line).
Moreover, each tower is connected to another by a staircaise that connects
numbers $k=2j+1$ and $3k+1$. This is shown as a red arrow
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overrightarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\langle
k,3k+1\rangle}$.

12838464089611521408166419202176243226882944320034563712396842244480473649925248550457606016627265286784704072967552780880648320857688329088934496009856101121036810624108801113611392116481190412160124161267212928131841344013696139521420814464147201497664192320448576704832960108812161344147216001728185619842112224023682496262427522880300831363264339235203648377639044032416042884416454446724800492850565184531254405568569658245952608062086336646465926720684869767104723273607488329616022428835241648054460867273680086492899210561120118412481312137614401504156816321696176018241888195220162080214422082272233624002464252825922656272027842848291229763040310431683232329633603424348835523616368037441648801121441762082402723043363684004324644965285605926246566887207527848168488809129449761008104010721104113611681200123212641296132813601392142414561488152015521584161616481680171217441776180818401872824405672881041201361521681842002162322482642802963123283443603763924084244404564724885045205365525685846006166326486646806967127287447607767928088248408568728889049209364122028364452606876849210010811612413214014815616417218018819620421222022823624425226026827628429230030831632433234034835636437238038839640441242042843644445246046826101418222630343842465054586266707478828690949810210611011411812212613013413814214615015415816216617017417818218619019419820220621021421822222623023413579111315171921232527293133353739414345474951535557596163656769717375777981838587899193959799101103105107109111113115117

Figure 4: Hotel Collatz

######  Definition 13 (Hotel Collatz)

The graph $HC=\langle V,E\rangle$ is defined as follows
$V=N$ i.e. the set of vertices is the set of standard, reachable, natural
numbers
$E=\\{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\overrightarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\langle
k,p\rangle}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}:\exists_{p}\,k=p+p\\}\cup\\{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\overrightarrow{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\langle
k,3k+1\rangle}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}:\exists_{p}k=p+p+1\\}$
are edges of the graph

Note. Don’t forget, our drawing is only a small fragment of the infinite HC
structure. The picture shows a small part of red arrows. We drew only those
red arrows that fit entirely on a page.
---

###### Conjecture 14

The hotel Collatz is an infinite, connected, acyclic graph, i.e. it is a tree.
Number 1 is the root of the tree.

Making use of the definition 6 one can formulate the following

###### Conjecture 15

The set $\overline{W}\stackrel{{\scriptstyle df}}{{=}}\bigcup\limits_{x\in
N}\,W_{x}$ is a partition of the set $N$ of nodes of Hotel Collatz.

##  4 On finite and infinite computations of Collatz algorithm

Question Can some computation contain both reachable and unreachable elements?
No. The subset of reachable elements is closed with respect of division by 2
and multiplication by 3. The same observation applies to the set of
unreachable elements.
We know, cf. subsection 6.1 that computations of nonreachable elements are
infinite.

###  4.1 Finite computations

Let $\mathfrak{M}=\langle M;0,1,+,=\rangle$ be any algebraic structure that is
a model of elementary theory of addition of natural numbers, c.f. subsection
6.2.
Denotation. Let $\theta(x,y)$ be a formula. The expression $(\mu
x)\theta(x,y)$ denotes the least element $x(y)$ such that the value of the
formula is truth.
Example. $(\mu x)(x+x>y)$.

The following lemma gathers the facts established earlier.

###### Lemma 16

Let $n$ be an arbitrary element of the structure $\mathfrak{M}$. The following
conditions are equivalent

  1. (i)

The sequence $n_{0}=n$ and $n_{i+1}=\begin{cases}n_{i}\div 2&\text{when }\
n_{i}\mod 2=0\\\ 3n_{i}+1&\text{when }\ n_{i}\mod 2=1\end{cases}$ determined
by
the recurrence (1) contains an element $n_{j}=1$

  2. (ii)

The computation of the algorithm $Cl$ is finite.

  3. (iii)

The sequence $m_{0}=\frac{n}{2^{k_{0}}}$ and
$m_{i+1}=\frac{3m_{i}+1}{2^{k_{i}}}$ determined by the recurrence (3)
stabilizes, i.e. there exist $l$ such that $m_{k}=1$ for all $k>l$

  4. (iv)

The computation of the algorithm $Gr$ is finite.

  5. (v)

The computation of the algorithm $Gr1$ is finite and the subsequent values of
the variables $M_{i}$ and $K_{i}$ satisfy the recurrence (3) .

  6. (vi)

The computation of the algorithm $Gr2$ is finite and the subsequent values of
the variables $m_{i}$ and $k_{i}$ satisfy the recurrence (3). The formula
$n\cdot 3^{x}+y=m_{i}\cdot 2^{z}$ holds after each iteration of while
instruction, i.e. it is the invariant of the program $\Delta_{2}$. The final
valuation of variables $x,y,z$ and $n$ satisfies the equation $n\cdot
3^{x}+y=2^{z}$.

  7. (vii)

The computation of the algorithm $Gr3$ is finite.
The subsequent values of the variables $m_{i}$ and $k_{i}$ satisfy the
recurrence (3) .
The subsequent values of the variables $X_{i},Y_{i},Z_{i}$ form a monotone,
increasing sequence of triples.
The formula $n\cdot 3^{X_{i}}+Y_{i}=m_{i}\cdot 2^{Z_{i}}$ is satisfied after
each $i$-th iteration of the program $Gr3$, i.e. the value of the following
exression $\\{\Gamma_{3};\,\Delta_{3}^{i}\\}(X_{i}+Z_{i})$ is the total number
of operations excuted. The value of the variable $Y_{i}$ encodes the history
of the computation till the $i$-th iteration of $\Delta_{3}$

Suppose that for a given element $n$ the computationof algorithm $Gr2$ is
finite.
Let $\bar{x}=(\mu x)\Biggl{(}n\cdot
3^{x}+\Biggl{[}\sum\limits_{j=0}^{x-1}\bigl{(}3^{x-1-j}\cdot
2^{\sum\limits_{l=0}^{j}\,k_{l}}\bigr{)}\Biggr{]}=2^{\sum\limits_{j=0}^{x}\,k_{j}}\Biggr{)}$.
Put $\bar{y}=\sum\limits_{j=0}^{\bar{x}-1}\bigl{(}3^{\bar{x}-1-j}\cdot
2^{\sum\limits_{l=0}^{j}\,k_{l}}\bigr{)}$ and
$\bar{z}=\sum\limits_{j=0}^{\bar{x}}\,k_{j}$.
We present the algorithm $IC^{\prime}$, which is a slightly modified version
of the algorithm $IC$ devised in [MS21] .

$IC^{\prime}:\left\\{\begin{array}[]{l}\textbf{var}\
\mathrm{x,y,z},k:integer,Err:Boolean;\\\ Err:=false;\\\ \mathbf{while}\
\mathrm{x+y+z}\neq 0\ \ \mathbf{do}\\\ \
Tr:\begin{array}[]{|l|}\hline\cr\mathbf{if}\
\bigl{(}odd(\mathrm{y})\land((\mathrm{x}=0)\ \lor\
(\mathrm{y}<3^{\mathrm{x}-1}))\bigr{)}\\\ \ \ \ \mathbf{then}\ Err:=true;\
\mathbf{exit}\\\ \mathbf{fi};\\\ \ \mathrm{x}:=\mathrm{x}-1;\
\mathrm{y}:=\mathrm{y}-3^{\mathrm{x}};\ k:=expo(\mathrm{y},2);\\\
\mathrm{y}:=\dfrac{\mathrm{y}}{2^{k}};\,\mathrm{z}:=\mathrm{z}-k;\\\
\hline\cr\end{array}\\\ \mathbf{od}\end{array}\,\right\\}$ (IC’)

We observe the following fact

###### Lemma 17

For every element $n$

$(n=b)\land\\{Gr2\\}\Biggl{(}\bigl{(}(x=\bar{x}\land y=\bar{y}\land
z=\bar{z})\land(b\cdot
3^{\bar{x}}+\bar{y}=2^{\bar{z}})\bigr{)}\Rightarrow\\{IC^{\prime}\\}(x=y=z=0)\Biggr{)}$

and

$(x=\bar{x}\land y=\bar{y}\land z=\bar{z})\land(b\cdot
3^{\bar{x}}+\bar{y}=2^{\bar{z}})\bigr{)}\land\\\
\biggl{(}\\{IC^{\prime}\\}(x=y=z=0)\implies(n=b)\implies\\{Gr2\\}(x=\bar{x}\land
y=\bar{y}\land z=\bar{z})\biggr{)}$

The contents of this lemma are best explained by the commutativity of the
diagram below.

${\boxed{\bigl{(}\frac{n}{b}\bigr{)}\,\bigl{(}\frac{x}{0}\frac{y}{0}\frac{z}{0}\bigr{)}}}$${\boxed{\bigl{(}(\frac{x}{\bar{x}}\frac{y}{\bar{y}}\frac{z}{\bar{z}})(\frac{n}{1})}\land(b\cdot
3^{\bar{x}}+\bar{y}=2^{\bar{z}})\bigr{)}}$$\scriptstyle{Gr2(n)}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}IC(x\,y\,z)}$

Proof. The proof makes use of two facts:
1) $even(n)\equiv even(\sum\limits_{j=0}^{x-1}\bigl{(}3^{x-1-j}\cdot
2^{\sum\limits_{l=0}^{j}\,k_{l}}\bigr{)})$
2) $\sum\limits_{j=0}^{x-1}\bigl{(}3^{x-1-j}\cdot
2^{\sum\limits_{l=0}^{j}\,k_{l}}\bigr{)}=2^{k_{0}}\cdot(3^{x-1}+2^{k_{1}}\cdot(3^{x-2}+2^{k_{2}}\cdot(\dots+2^{k_{x}}\cdot
3^{0})))$
One can prove this lemma by induction w.r.t. number of encountered odd
numbers.
The thesis of the lemma is very intuitive. Look at the Collatz hotel Fig. 4.
The lemma states that for every room number $n$ the two conditions are
equivalent (1) there is a path from room number $n$ to the exit, which is
located near room number 1, (2) there is a path from entry to the hotel near
room number 1 to the room number $n$. It is clear that such a path must be
complete, no jumps are allowed.

###### Lemma 18

For every element $n$ the following conditions are equivalent

  * (i)

computation of Collatz algorithm $Cl$ is finite,

  * (ii)

there exists the least element $x$ such that the following equality holds

$n\cdot 3^{x}+\Biggl{(}\sum\limits_{j=0}^{x-1}3^{x-1-j}\cdot
2^{\,\sum\limits_{l=0}^{j}\,k_{l}}\Biggr{)}=2^{\,\sum\limits_{j=0}^{x}\,k_{j}}.$
(Mx)

where the sequence $\\{k_{i}\\}$ is determined by the element $n$ in
accordance to the recurrence (3).

Proof. The implication (i) $\Rightarrow$ (ii) follows from lemma 16(vii).
Consider the inverse implication (ii) $\Rightarrow$ (i). If (ii) holds, then
the computation of program $Gr_{3}$ reaches 1 after $x$-th iteration of
internal instruction $\Delta_{3}$. The value of $m_{x}$ is then 1. The
computation performs $x$ nultiplications and $z=\sum\limits_{j=0}^{x}k_{j}$
divisions.
The value of $y=\Biggl{(}\sum\limits_{j=0}^{x-1}\bigl{(}3^{x-1-j}\cdot
2^{\,\sum\limits_{l=0}^{j}\,k_{l}}\bigr{)}\Biggr{)}$ codes the history of the
computation.
Which means: $x_{0}$ is the number of multiplication by 3,
$z=\sum\limits_{j=0}^{x}\,k_{j}$ is the total number of divisions by 2 and for
every $0\leq j\leq x-1$ the number $k_{j}$ is the number of divisions by 2
excuted in between the $j$-th and $j+1$-th execution of multiplication by 3.
The algorithm $Cl$ executes $x+z$ iterations. The lemma 18 gives the halting
formula i.e. a satisfactory and necessary condition for the computation of the
Collatz program to be finite.
We shall summarize the considerations on finite computations in the following
commutative diagram.

${n}$${m_{1}}$${m_{2}}$${m_{3}}$${\cdots\ \
m_{x-1}}$${m_{x}=1}$${0,0,0}$${0,0,k_{0}}$${1,Y_{1},Z_{1}}$${2,Y_{2},Z_{2}}$${\cdots\
\
x-1,Y_{x-1},Z_{x-1}}$${x,Y_{x},Z_{x}}$${x,Y_{x},Z_{x}}$${x_{0},\bar{Y}_{x_{0}},\bar{Z}_{x_{0}}}$${x_{1},\bar{Y}_{x_{1}},\bar{Z}_{x_{1}}}$${x_{2},\bar{Y}_{x_{2}},\bar{Z}_{x_{2}}}$${\cdots\
\ \ \
1,\bar{Y}_{1},\bar{Z}_{1}}$${0,0,0}$${1}$${m_{x-1}}$${m_{x-2}}$${m_{x-3}}$${\cdots
m_{1}}$${n}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}/2^{k_{0}}}$$\scriptstyle{Gr3}$$\scriptstyle{Gr1}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3m_{1}+1}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}/2^{k_{1}}}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3m_{2}+1}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}/2^{k_{2}}}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3m_{3}+1}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}/2^{k_{3}}}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}3m_{x-1}+1}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}/2^{k_{x-1}}}$$\scriptstyle{\Gamma_{3}}$$\scriptstyle{Gr3}$$\scriptstyle{\Delta_{3}}$$\scriptstyle{\Delta_{3}}$$\scriptstyle{\Delta_{3}}$$\scriptstyle{\Delta_{3}}$$\scriptstyle{\definecolor[named]{.}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}Tr}$$\scriptstyle{IC^{\prime}}$$\scriptstyle{\definecolor[named]{.}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}Tr}$$\scriptstyle{\definecolor[named]{.}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}Tr}$$\scriptstyle{\definecolor[named]{.}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}Tr}$$\scriptstyle{\definecolor[named]{.}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}Tr}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\times
2^{k_{x-1}}}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\div
3}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\cdot\times
2^{k_{x-2}})-1}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\div
3}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\cdot\times
2^{k_{x-3}})-1}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\div
3}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\cdot\times
2^{k_{x-2}})-1}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\div
3}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\cdot\times
2^{k_{0}})-1}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\div
3}$ Figure 5: Case of finite computation illustrated
Upper row, (with red arrows) represents computation of $Gr1$,
elements $k_{i}$ and $m_{i}$ are calculated in accordance with the recurrence
(rec2)
rows 1 and 2 show computation of $Gr3$, the subsequent triples are
$X_{i+1}=i+1,Y_{i+1}=3Y_{i}+2^{Z}_{i},Z_{i+1}=Z_{i}+k_{i}$
third row (blue arrows) shows computation of algorithm $IC$ on triples,
$\bar{Y}_{x}=Y_{x}$ and $\bar{Z}_{x}=Z_{x}$ and for $i=x,\dots,1$ we have
$\bar{Z}_{i-1}=\bar{Z}_{i}-k_{i}$ and
$\bar{Y}_{i-1}=(\bar{Y}_{i}/2^{k_{i}})-3^{i-1}$

###  4.2 Infinite computations

Do infinite computations exist?
There are two answers yes and no.
Yes Imagine your computer system is (maliciously) handled by a hacker. This
can be done by preparing its hardware or software (e.g. someone modifies the
class Int in Java). To hide the damage from the user, the hacker may come with
a correct proof that all axioms of natural numbers (e.g. of Presburger’s
system) are valid. Yet, for many $n$ execution of the Collatz algorithm will
not terminate. See subsections 4.4 and 6.1. No If argument of Collatz
procedure is a standard (i.e. reachable) natural number then the computation
is finite.
We are going to prove the following

###### Lemma 19

If for certain number $n$ computation of Collatz algorithm is infinite then
$n$ is not a reachable, natural number.

We remark that the semantical property: for a given element $n$ the
computation of Collatz algorithm may be continued at will , i.e. it is an
infinite computation, is expressed by the following formula

$\left\\{\Gamma_{3}\right\\}\bigcap\left\\{\Delta_{3}\right\\}(n_{i}\neq 1)$ (
$\Pi$)

where denotations $\Gamma_{3}$ and $\Delta_{3}$ were introduced on page 3, see
program $Gr_{3}$.

For it says: after every iteration of subprogram $\Delta_{3}$ of the program
$Gr_{3}$ the value of the variable $n$ is not equal 1.
The following formula

$\left\\{i:=0;\right\\}\bigcap\left\\{i:+i+1\right\\}(n\cdot
3^{i}+\sum\limits_{j=0}^{i-1}3^{i-1-j}\cdot 2^{Z_{j}}\neq 2^{Z_{i}})$ ( $\Xi$)

where denotation $Z_{j}$ was introduced on page 3

does express the semantical property: for every reachable, natural number $i$
the inequality $(n\cdot 3^{i}+\sum\limits_{j=0}^{i-1}3^{i-1-j}\cdot
2^{Z_{j}}\neq 2^{Z_{i}})$ holds.
Hence our goal is to prove the implication $(\Pi\implies\Xi)$.
We begin with simple observation that every formula of the following set
$Z_{a}$ is a tautology

$Z_{a}\stackrel{{\scriptstyle df}}{{=}}\left\\{\
(\left\\{\Gamma_{3}\right\\}\left\\{\Delta_{3}\right\\}^{r}(n_{i}\neq
1)\implies\left\\{\Gamma_{3}\right\\}\left\\{\Delta_{3}\right\\}^{r}(n_{i}\neq
1))\ \right\\}_{r\in N}$

here $\underline{\mathbf{}r}=\underbrace{1+1+1+\cdots+1}_{r\ times}$ is any
reachable, natural number.
For every natural number $r$ the following equivalence is a theorem of
algorithmic theory of numbers $\mathcal{ATN}$

$\big{(}\
\left\\{\Gamma_{3}\right\\}\left\\{\Delta_{3}\right\\}^{r}(n_{i}=1)\Leftrightarrow\left\\{\Gamma_{3}\right\\}\left\\{\Delta_{3}\right\\}^{r}(n\cdot
3^{i}+\sum\limits_{j=0}^{i-1}3^{i-1-j}\cdot 2^{Z_{j}}=2^{Z_{i}})\ \big{)}\ $

Hence the following set $Z_{b}$ consists of theorems of theory $\mathcal{ATN}$

$Z_{b}\stackrel{{\scriptstyle df}}{{=}}\left\\{\
(\left\\{\Gamma_{3}\right\\}\left\\{\Delta_{3}\right\\}^{r}(n_{i}\neq
1)\Rightarrow\left\\{\Gamma_{3}\right\\}\left\\{\Delta_{3}\right\\}^{r}(n\cdot
3^{i}+\sum\limits_{j=0}^{i-1}3^{i-1-j}\cdot 2^{Z_{j}}\neq 2^{Z_{i}}))\
\right\\}_{r\in N}$

Look at programs $\left\\{\Gamma_{3}\right\\}$ and
$\left\\{\Delta_{3}\right\\}$, on page 3. Note that first program contains
instruction $i:=0$ and the second program contains the instruction $i:=i+1$,
other instructions can be dropped. Hence the set $Z_{c}$ of formulas

$\displaystyle Z_{c}\stackrel{{\scriptstyle df}}{{=}}$ $\displaystyle\left\\{\
\left\\{\Gamma_{3}\right\\}\left\\{\Delta_{3}\right\\}^{r}(n_{i}\neq
1)\Rightarrow\left\\{i:=0\right\\}\left\\{i:=i+1\right\\}^{r}(n\cdot
3^{i}+\sum\limits_{j=0}^{i-1}3^{i-1-j}\cdot 2^{Z_{j}}\neq
2^{Z_{i}})\right\\}_{r\in N}$

contains only theorems of theory $\mathcal{ATN}$. Now by induction with
respect to $r$ we can prove that every formula of the set $Z_{d}$ is a theorem
of theory $\mathcal{ATN}$. I.e. we introduce the universal iteration
quantifier $\bigcap$ in the precedent of every implication of the set $Z_{c}$
of theorems of theory $\mathcal{ATN}$.

$\displaystyle Z_{d}\stackrel{{\scriptstyle df}}{{=}}$
$\displaystyle\left\\{\left\\{\Gamma\right\\}\bigcap\left\\{\Delta\right\\}(n_{i}\neq
1)\Rightarrow\left\\{i:=0\right\\}\left\\{i:=i+1\right\\}^{r}(n\cdot
3^{i}+\sum\limits_{j=0}^{i-1}3^{i-1-j}\cdot 2^{Z_{j}}\neq
2^{Z_{i}})\right\\}_{r\in N}$

the symbols $\Gamma$ and $\Delta$ were stripped off the indices 3 for
typographic reason.

In the proof we used axiom $Ax_{23}$ of calculus of programs, de Morgan’s laws
(case of infinite operations in a Boolean algebra) and propositional calculus,
c.f. page 6.3.
Now, we are ready to use the inference rule $R_{5}$, see page 6.3 and to
obtain the desired theorem of algorithmic theory $\mathcal{ATN}$

$\mathcal{ATN}\vdash\underbrace{\left\\{\Gamma_{3}\right\\}\bigcap\left\\{\Delta_{3}\right\\}(n_{i}\neq
1)}_{\Pi}\Rightarrow\underbrace{\left\\{i:=0\right\\}\bigcap\left\\{i:=i+1\right\\}(n\cdot
3^{i}+\sum\limits_{j=0}^{i-1}3^{i-1-j}\cdot 2^{Z_{j}}\neq 2^{Z_{i}})}_{\Xi}$
(7)

which reads:
if for a given number $n$ the computation of Collatz algorithm is infinite
then the number $n$ is an unreachable element of non-standard model of
Presburger arithmetic.
Why it is so?

  * •

The equation $n\cdot 3^{i}+\sum\limits_{j=0}^{i-1}3^{i-1-j}\cdot 2^{Z_{j}}\neq
2^{Z_{i}}$ is an implicit definition of a function that to a given number $n$
assigns a corresponding number $i$, consult the lemma 36,

  * •

Note, the elements $n$ and $i$ are either both reachable or both unreachable
numbers.

This ends the proof of the lemma.

—————————

###  4.3 Collatz theorem

Till now we proved that Collatz conjecture is _valid_ in the structure
$\mathfrak{N}$ of standard (reachable) natural numbers.

###### Lemma 20

Let $n$ be any standard element of the structure $\mathfrak{N}$. The
computation of Collatz algorithm $Cl$ that begins with $n$ is finite.

Proof. The proof follows immediately from the lemmas 18 and 19.

###### Corollary 21

Conjectures 3, 14 and 15 formulated above are valid statements.

Now, making use of the completeness theorem of calculus of programs we argue
that the terminatiom formula of the Collatz algorithm possedes a proof in the
algorithmic theory of natural numbers $\mathcal{ATN}$.
Let $\Theta_{CL}$ be the following formula of $\mathcal{ATN}$

$\underbrace{\forall_{n}\\{n^{\prime}:=1\\}\bigcup\\{n^{\prime}:=n^{\prime}+1\\}(n^{\prime}=n)}_{\forall_{n\in
N,\,n\geq 1}}\implies\bigcup\left\\{\begin{array}[]{l}\mathbf{if}\ n\neq 1\
\mathbf{then}\\\ \quad\mathbf{if}\ odd(n)\ \mathbf{then}\\\ \ \ \quad
n:=3*n+1\\\ \quad\mathbf{else}\\\ \ \ \quad n:=n\div 2\\\ \quad\mathbf{fi}\\\
\mathbf{fi}\end{array}\right\\}(n=1)$ ($\Theta_{CL}$)

The formula expresses the termination property of Collatz algorithm. The lemma
20 states that the formula $\Theta_{CL}$ is valid in the standard model
$\mathfrak{N}$.
Perhaps, the reader will prefer another formula $\Theta^{\prime}_{CL}$ which
looks as follow

$\mathcal{ATN}\vdash\underbrace{\\{n:=1\\}\bigcap\\{n:=n+1\\}}_{\forall_{n\in
N,\,n\geq 1}}\left\\{\begin{array}[]{l}\mathbf{while}\ n\neq 1\ \mathbf{do}\\\
\quad\mathbf{if}\ odd(n)\ \mathbf{then}\\\ \ \ \quad n:=3*n+1\\\
\quad\mathbf{else}\\\ \ \ \quad n:=n\div 2\\\ \quad\mathbf{fi}\\\
\mathbf{od}\end{array}\right\\}(n=1)$ ($\Theta^{\prime}_{CL}$)

###### Theorem 22

The formula $\Theta_{CL}$ is a theorem of the theory $\mathcal{ATN}$.

Proof. Recall that the $\mathcal{ATN}$ theory is categorical. It means that
every model of this theory is isomorphic to the standard model $\mathfrak{N}$.
The sentence $\Theta_{CL}$ is valid in $\mathfrak{N}$, i.e. in every model
of$\mathcal{ATN}$.
By the completeness property of the calculus of programs, the theory contains
the proof of the sentence $\Theta_{CL}$.
Someone may ask: why this awkward prefix in the formula $\Theta_{CL}$?
Note the difference between phrases $\forall_{n}$ and $\forall_{n\in N}$.

###  4.4 A counterexample

We argue, that the formulation of the Collatz problem requires more precision.
For there are several algebraic structures that can be viewed as structure of
natural numbers of addition. Some of them admit infinite computations of
Collatz algorithm.
We recall less known fact: arithmetic (i.e. first-order theory of natural
numbers) has standard (Archimedean) model $\mathfrak{N}$ as well as another
non-Archimedean model $\mathfrak{M}$333A. Tarski [Tar34] confirms that S.
Jaśkowski observed (in 1929) that the subset of complex numbers
$M\stackrel{{\scriptstyle
df}}{{=}}\bigl{\\{}a+bi\in\mathbb{C}\colon\bigl{(}a\in\mathbb{Z}\land
b\in\mathbb{Q}\land(b\geq 0\land(b=0\implies a\geq 0))\bigr{\\}}$ satisfies
all axioms of Presburger arithmetic.. The latter structure allows for the
existence of infinitely great elements.
Goedel’s incompleteness theorem shows that there is no elementary theory $T$
of natural numbers, such that every model is isomorphic to the standard model.
Two things are missing from the commonly accepted texts: 1) What do we mean by
proof? 2) what properties of natural numbers can be used in the proof? We
recall an algebraic structure $\mathfrak{M}$ that models [Grz71] all axioms of
elementary theory of addition of natural numbers, yet it admits unreachable
elements [Tar34]. It means that the model contains element $\varepsilon$, such
that the computation of Collatz algorithm that starts with $\varepsilon$ is
infinite.
Example of a finite execution

$\langle 13,0\rangle\stackrel{{\scriptstyle\times 3+1}}{{\rightarrow}}\langle
40,0\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\langle
20,0\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\langle
10,0\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}},\langle
5,0\rangle\stackrel{{\scriptstyle\times 3+1}}{{\rightarrow}}\langle
16,0\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\langle
8,0\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\langle
4,0\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\langle
2,0\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\langle 1,0\rangle$

Example of an infinite execution

$\langle 8,\frac{1}{2}\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\
\langle
4,\frac{1}{4}\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\langle
2,\frac{1}{8}\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\langle
1,\frac{1}{16}\rangle\stackrel{{\scriptstyle\times 3+1}}{{\rightarrow}}\langle
4,\frac{3}{16}\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\langle
2,\frac{3}{32}\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\langle
1,\frac{3}{64}\rangle,\stackrel{{\scriptstyle\times
3+1}}{{\rightarrow}}\langle
4,\frac{9}{64}\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\langle
2,\frac{9}{128}\rangle\stackrel{{\scriptstyle\div\,2}}{{\rightarrow}}\mathbf{\cdots}$

As you can guess, the data structure contains pairs $\langle k,w\rangle$ where
$k$ is an integer and $w$ is a non-negative, rational number. The addition
operation is defined componentwise. An element $\langle k,w\rangle$ is even
if k is even, otherwise is odd.. A pair $\langle k,w\rangle$ divided by 2
returns $\langle k\div 2,w\div 2\rangle$ .
The reader may prefer to think of complex numbers instead of pairs, e.g.
($2+\frac{9}{128}\textit{i}$) may replace the pair $\langle
2,\frac{9}{128}\rangle$.
The following observation seems to be of importance:.

###### Remark 23

There exists an infinite computation $\mathbf{c}$ of Collatz algorithm in the
structure $\mathfrak{M}$ , such that the computation $\mathbf{c}$ does not
contain a cycle, and the sequence of pairs is not diverging into still growing
pairs. The latter means, that there exist two numbers $l_{1}\in\mathcal{Z}$
and $l_{2}\in\mathcal{Q}$, such that for every step $\langle k,v\rangle$ of
computation $\mathbf{c}$, the inequalities hold $k<l_{1}\land v<l_{2}$.

More details can be found in subsection 6.1.

##  5 Final remarks

We know that our presentation is clumsy (we are of age, english is not our
native language).
Our message goes beyond the proof of one theorem. On this example we exemplify
the potential of calculus of programs as a tool for

  * •

specification of semantical properties of software and

  * •

verification of software against some specifications.

We hope the reader will forgive us for a moment of insistence (is it an
agitpropaganda?) .
Calculus of programs $\mathcal{AL}$ is a handy tool. For there are some good
reasons to use the calculus of programs

  * (i)

The language of calculus $\mathcal{AL}$ contains algorithms (programs) and
algorithmic formulas besides terms and first-order formulas.

  * (ii)

Any semantical property of an algorithm can be expressed by an appropriate
algorithmic formula. Be it termination, correctness or other properties.

  * (iii)

Algorithmic formulas enable to create complete, categorical specifications of
data structures in the form of algorithmic theories.

  * (iv)

Calculus of programs $\mathcal{AL}$ offers a complete set of tools for proving
theorems of algorithmic theories.

In spite of appearance of $\omega$-rules one can verify proofs in an automatic
way.

###  5.1 Historical remarks

Pàl Erde̋s said on Collatz conjecture: "Mathematics may not be ready for such
problems."
We disagree. In our opinion a consortium of Alfred Tarski, Kurt Goedel and
Stephen C. Kleene was able to solve the Collatz conjecture in 1937. ()Tarski
was advisor of M. Presburger and S. Jaśkowski.)

  * •

Mojżesz Presburger has proved the completeness and decidability of arithmetic
of addition of natural numbers in 1929.

  * •

In the same year Stanisław Jaśkowski found a non-standard model of Presburger
theory (see a note of A. Tarski of 1934).

  * •

Kurt Gödel (1931) published his theorem on incompleteness of Peano’s theory.
His result is of logic, not an arithmetic fact.

  * •

Thoralf Skolem (in 1934) wrote a paper on the non-characterization of the
series of numbers by means of a finite or countably infinite number of
statements with exclusively individual variables [Sko34]

  * •

Stephen C. Kleene has shown (in 1936) that any recurrence that defines a
computable function can be replaced by the operation of effective minimum
(nowadays one can say every recursive function in the integers, is
programmable by means of while instruction).

  * •

Summing up, it seems that P. Erde̋s overlooked the computability theory, his
colleagues - professors Rozsa Peter and Laszlo Kalmar (specialists in the
theory of recursive functions) were able to point it out to him.

Andrzej Mostowski had a hope that many arithmetic theorems independent of the
Peano axioms should be found. Collatz theorem is an example. The theorem on
termination of Euclid’s algorithm is another example of a theorem which is
valid and unprovable in Peano theory. The law of Archimedes is yet another
example. Note, both theorems need to be stated as algorithmic formulas, there
is no first-order formula that expresess the termination property of Euclid’s
algorithm or law of Archimedes.

### Acknowlegments

##  6 Suplements

For the reader’s convenience, in this section we have included some
definitions, some useful theorems, and samples of proofs in algorithmic
natural number theory.

###  6.1 A structure with counterexamples

where Collatz computations may be of infinite length

Here we present some facts that are less known to the IT community.
These facts may seem strange. The reader may doubt the importance of those
facts. Yet, it is worth considering, non-standard data structures do exist,
and this fact has ramifications. Strange as they seem, still it is worthwhile
to be aware of their existence.
Now, we will expose the algebraic structure $\mathfrak{M}$, which is a model
of the theory $Ar$, i.e. all axioms of theory $Ar$ are true in the structure
$\mathfrak{M}$. First we will describe this structure as mathematicians do,
then we will write a class (i.e. a program module) implementing this
structure.

#### Mathematical description of the structure

$\mathfrak{M}$ is an algebraic structure

$\mathfrak{M}=\langle
M;\,\mbox{{\text@underline{0}}},\mbox{{\text@underline{1}}},\oplus;\,=\rangle$

such that $M$ is a set of complex numbers $k+\imath w$, i.e. of pairs $\langle
k,w\rangle$, where element $k\in\mathbb{Z}$ is an integer, and element
$w\in\mathbb{Q}^{+}$ is a rational, non-negative number $w\geq 0$ and the
following requirements are satisfied:

  1. (i)

for each element $k+\imath w$ if $w=0$ then $k\geq 0$,

  2. (ii)

0 $\stackrel{{\scriptstyle df}}{{=}}$ $\langle 0+\imath 0\rangle$,

  3. (iii)

1 $\stackrel{{\scriptstyle df}}{{=}}$ $\langle 1.+\imath 0\rangle$,

  4. (iv)

the operation $\oplus$ of addition is determined as usual

$(k+\imath w)\oplus(k^{\prime}+\imath w^{\prime})\stackrel{{\scriptstyle
df}}{{=}}(k+k^{\prime})+\imath(w+w^{\prime}).$

  5. (v)

the predicate = denotes as usual identity relation.

###### Lemma 24

The algebraic structure $\mathfrak{M}$ is a model of first-order arithmetic of
addition of natural numbers $\mathcal{T}$, cf. next subsection 6.2

The reader may check that every axiom of the $\mathcal{T}$ theory (see
definition32, p.32), is a sentence true in the structure $\mathfrak{M}$.
The substructure $\mathfrak{N}\subset\mathfrak{M}$ composed of only those
elements for which $w=0$ is also a model of the theory $\mathcal{T}$.
It is easy to remark that elements of the form $\langle k,0\rangle$ may be
identified with natural numbers $k$, $k\in N$. Have a look at table 1
The elements of the structure $\mathfrak{N}$ are called reachable, for they
enjoy the following algorithmic property

$\forall_{n\in N}\,\\{y:=\textbf{0};\mathbf{while}\ y\neq n\ \mathbf{do}\
y:=y+\textbf{1}\ \mathbf{od}\\}(y=n)$

The structure $\mathfrak{M}$ is not a model of the $\mathcal{ATN}$,
algorithmic theory of natural numbers, cf . subsection 6.4. Elements of the
structure $\langle k,w\rangle$. such as $w\neq\textbf{0}$ are unreachable.
i.e. for each element $x_{0}=\langle k,w\rangle$ such that $w\neq 0$ the
following condition holds

$\lnot\\{y:=\textbf{0};\mathbf{while}\ y\neq x_{0}\ \mathbf{do}\
y:=y+\textbf{1}\ \mathbf{od}\\}(y=x_{0})$

The subset $\mathfrak{N}\subset\mathfrak{M}$ composed of only those elements
for which $w=0$ is a model of the theory $\mathcal{ATN}$ c.f. subsection 6.4.
The elements of the structure $\mathfrak{N}$ are called reachable. A very
important theorem of the foundations of mathematics is

###### Lemma 25

The structures $\mathfrak{N}$ and $\mathfrak{M}$ are not isomorphic.

For the proof see [Grz71], p. 256. As we will see in a moment, this fact is
also important for IT specialists.

An attempt to visualize structure $\mathfrak{M}$ is presented in the form of
table 1. The universe of the structure $\mathfrak{M}$ decomposes onto two
disjoint subsets (one green and one red). Every element of the form $\langle
k,0\rangle$ (in this case $k>0$) represents the natural number $k$. Such
elements are called reachable ones. Note,

###### Definition 26

An element $n$ is a standard natural number (i.e. is reachable ) iff the
program of adding ones to initial zero terminates

$n\in N\stackrel{{\scriptstyle
df}}{{\Leftrightarrow}}\\{q:=\textbf{0};\,\textbf{while}\ q\neq n\
\textbf{do}\ q:=q+\textbf{1}\ \textbf{od}\\}(q=n)$

or, equivalently

$n\in N\stackrel{{\scriptstyle
df}}{{\Leftrightarrow}}\\{q:=\textbf{0}\\}\bigcup\\{\mathbf{if}\ n\neq q\
\mathbf{then}\ q:=q+\textbf{1}\ \mathbf{fi}\\}(q=n)$

Table 1: Model $\mathfrak{M}$ of Presburger arithmetic  consists of complex
numbers $a+\imath\,b$ where $b\in Q^{+}$ and $a\in Z$, additional condition:
$b=0\Rightarrow a\geq 0$. Definition of order $n>m\stackrel{{\scriptstyle
df}}{{\equiv}}\exists_{u\neq 0}\,m+u=n$. Invention of S. Jaśkowski (1929).

$\begin{array}[]{c|c}\text{{\hbox{\pagecolor{green}Standard}}\ ({reachable})\
elements}&\text{{Unreachable}\ ({\hbox{\pagecolor{red!22}infinite}})
elements}\\\
\hline\cr\hline\cr&\begin{array}[]{c}\pagecolor{red!20}\begin{array}[]{cccccccccc}\pagecolor{red!20}\hfil&&&&\pagecolor{white}\cdots\\\
\hline\cr\pagecolor{white}{-\infty\cdots}&-11+\imath 2&-10+\imath
2&\cdots&0+\imath 2&1+\imath 2&2+\imath 2&\pagecolor{white}{\cdots\infty}\\\
\hline\cr\pagecolor{red!20}\hfil&&&&\pagecolor{white}\cdots\\\
\hline\cr\pagecolor{white}{-\infty\cdots}&-11+\imath\frac{53}{47}&-10+\imath\frac{53}{47}&\cdots&0+\imath\frac{53}{47}&1+\imath\frac{53}{47}&2+\imath\frac{53}{47}&\pagecolor{white}{\cdots\infty}\\\
\hline\cr\pagecolor{red!20}\hfil&&&&\pagecolor{white}\cdots\\\
\hline\cr\pagecolor{white}{-\infty\cdots}&-11+\imath\frac{28}{49}&-10+\imath\frac{28}{49}&\cdots&0+\imath\frac{28}{49}&1+\imath\frac{28}{49}&2+\imath\frac{28}{49}&\pagecolor{white}{\cdots\infty}\\\
\hline\cr\pagecolor{red!20}\hfil&&&&\pagecolor{white}\cdots\\\
\hline\cr\pagecolor{white}{-\infty\cdots}&-11+\imath\frac{3}{47}&-10+\imath\frac{3}{47}&\cdots&0+\imath\frac{3}{47}&1+\imath\frac{3}{47}&2+\imath\frac{3}{47}&\pagecolor{white}{\cdots\infty}\\\
\hline\cr\pagecolor{red!20}\hfil&&&&\pagecolor{white}\cdots\\\ \end{array}\\\
\end{array}\\\
\pagecolor{green!30}\begin{array}[]{ccccccc}0&1&2&\cdots&101&\cdots&\pagecolor{white}{\infty}\\\
\end{array}\\\ \end{array}$

Note that the subset that consists of all non-reachable elements is well
separated from the subset of reachable elements. Namely, every reachable
natural number is less that any unreachable one. Moreover, there is no least
element in the set of unreachable elements. I.e. the principle of minimum does
not hold in the structure $\mathfrak{M}$.
Moreover, for every element $n$ its computation contains either only standard,
reachable numbers or is composed of only unreachable elements. This remark
will be of use in our proof.

###### Remark 27

For every element $n$ the whole Collatz computation is either in green or in
reed quadrant of the table 1.

Elements of the structure $\mathfrak{M}$ are ordered as usual

$\forall_{x,y}\ x<y\stackrel{{\scriptstyle df}}{{=}}\exists_{z\neq\textbf{0}}\
x+z=y.$

Therefore, each reachable element is smaller than every unreachable element.
The order defined in this way is the lexical order. (Given two elements $p$
and $q$, the element lying higher is bigger, if both are of the same height
then the element lying on the right is bigger.)
The order type is $\omega+(\omega^{*}+\omega)\cdot\eta$

###### Remark 28

The subset of unreachable elements (red ones on the table 1) does not obey the
principle of minimum.

#### Definition in programming language

Perhaps you have already noticed that the $\mathfrak{M}$ is a computable
structure. The following is a class that implements the structure
$\mathfrak{M}$. The implementation uses the integer type, we do not introduce
rational numbers explicitly.
unit StrukturaM: class; unit Elm: class(k,li,mia: integer); begin if mia=0
then raise Error fi; if li * mia <0 then raise Error fi; if li=0 and k<0 then
raise Error fi; end Elm; add: function(x,y:Elm): Elm; begin result := new
Elm(x.k+y.k, x.li*y.mia+x.mia*y.li, x.mia*y.mia ) end add; unit one :
function:Elm; begin result:= new Elm(1,0,2) end one; unit zero : function:Elm;
begin result:= new Elm(0,0,2) end zero; unit eq: function(x,y:Elm): Boolean;
begin result := (x.k=y.k) and (x.li*y.mia=x.mia*y.li ) end eq; end StrukturaM
The following lemma expresses the correctness of the implementation with
respect to the axioms of Presburger arithmetic $\mathcal{AP}$ (c.f. subsection
6.2) treated as a specification of a class (i.e. a module of program).

###### Lemma 29

The structure $\mathfrak{E}=\langle E,add,zero,one,eq\rangle$ composed of the
set $E=\\{o\ \mbox{object}:o\ inElm\\}$ of objects of class Elm with the add
operation is a model of the $\mathcal{AP}$ theory,

$\mathfrak{E}\models\mathcal{AP}$

#### Infinite Collatz algorithm computation

How to execute the Collatz algorithm in StructuraM? It’s easy.
pref StrukturaM block var n: Elm; unit odd: function(x:Elm): Boolean; …
result:=(x.k mod 2)=1 … end odd; unit div2: function(x:Elm): Elm; … unit 3xp1:
function(n: Elm): Elm; …result:=add(n,add(n,add(n,one))); …end 3xp1; begin n:=
new Elm(8,1,2); Cl:  while not eq(n,one) do if odd(n) then n:=3xp1(n) else n:=
div2(n) fi od (* a version of algorithm Cl that uses class Elm *) end block;
Below we present the computation of Collatz algorithm for $n=\langle
8,\frac{1}{2}\rangle$.

$\langle 8,\frac{1}{2}\rangle,\,\langle 4,\frac{1}{4}\rangle,\langle
2,\frac{1}{8}\rangle,\,\langle 1,\frac{1}{16}\rangle,\,\langle
4,\frac{3}{16}\rangle,\,\langle 2,\frac{3}{32}\rangle,\,\langle
1,\frac{3}{64}\rangle,\,\langle 4,\frac{9}{64}\rangle,\,\langle
2,\frac{9}{128}\rangle,\cdots$

Note, the computation of algorithm $Gr$ for the same argument, looks simpler

$\langle 8,\frac{1}{2}\rangle,\,\langle 4,\frac{1}{4}\rangle,\langle
2,\frac{1}{8}\rangle,\,\langle 1,\frac{1}{16}\rangle,\,\langle
1,\frac{3}{64}\rangle,\,\langle 1,\frac{9}{256}\rangle,\,\cdots$

None of the elements of the above sequence is a standard natural number. Each
of them is unreachable. It is worth looking at an example of another
calculation. Will something change when we assign n a different object? e.g.
n: = new Elm (19,2,10)?

$\begin{array}[]{l}\langle 19,\frac{10}{2}\rangle,\,\langle
58,\frac{30}{2}\rangle,\langle 29,\frac{30}{4}\rangle,\,\langle
88,\frac{90}{4}\rangle,\,\langle 44,\frac{90}{8}\rangle,\,\langle
22,\frac{90}{16}\rangle,\,\langle 11,\frac{90}{32}\rangle,\,\langle
34,\frac{270}{32}\rangle,\,\langle 17,\frac{270}{64}\rangle,\\\ \langle
52,\frac{810}{64}\rangle,\langle 26,\frac{405}{64}\rangle,\langle
13,\frac{405}{128}\rangle,\langle 40,\frac{1215}{128}\rangle,\langle
20,\frac{1215}{256}\rangle,\langle 10,\frac{1215}{256}\rangle,\langle
5,\frac{1215}{512}\rangle,\langle 16,\frac{3645}{512}\rangle,\langle
8,\frac{3645}{1024}\rangle,\\\ \langle 4,\frac{3645}{2048}\rangle,\langle
2,\frac{3645}{4096}\rangle,\langle 1,\frac{3645}{8192}\rangle,\langle
4,\frac{3*3645}{8192}\rangle,\langle 2,\frac{3645*3}{2*8192}\rangle,\langle
1,\frac{3*3645}{4*8192}\rangle,\langle
4,\frac{9*3645}{4*8192}\rangle,\cdots\end{array}$

And one more computation.

$\begin{array}[]{l}\langle 19,0\rangle,\,\langle 58,0\rangle,\langle
29,0\rangle,\,\langle 88,0\rangle,\,\langle 44,0\rangle,\,\langle
22,0\rangle,\,\langle 11,0\rangle,\,\langle 34,0\rangle,\,\langle
17,0\rangle,\langle 52,0\rangle,\langle 26,0\rangle,\\\ \langle
13,0\rangle,\langle 40,0\rangle,\langle 20,0\rangle,\langle
10,0\rangle,\langle 5,0\rangle,\langle 16,0\rangle,\langle 8,0\rangle,\
\langle 4,0\rangle,\langle 2,0\rangle,\langle 1,0\rangle.\end{array}$

###### Corollary 30

The structure $\mathfrak{M}$, which we have described in two different ways,
is the model of the $\mathcal{AP}$ theory with the non-obvious presence of
unreachable elements in it.

###### Corollary 31

The halting property of the Collatz algorithm cannot be proved from the axioms
of the $\mathcal{T}$ theory, nor from the axioms of $\mathcal{AP}$ theory.

###  6.2 Presburger arithmetic

Presburger arithmetic is another name of elementary theory of natural numbers
with addition.
We shall consider the following theory , cf. [Pre29],[Grz71] p. 239 and
following ones.

###### Definition 32

Theory $\mathcal{T}=\langle\mathcal{L},\mathcal{C},Ax\rangle$ is the system of
three elements:

  * $\mathcal{L}$

is a language of first-order. The alphabet of this language consist of: the
set $V$ of variables, symbols of operations: $0,S,+$, symbol of equality
relation $=$, symbols of logical functors and quantifiers, auxiliary symbols
as brackets …
The set of well formed expressions is the union of te set $T$ of terms and the
set of formulas $F$.
The set $T$ is the least set of expressions that contains the set $V$ and
constants 0 and 1 and closed with respect to the rules: if two expressions
$\tau_{1}$ and $\tau_{2}$ are terms, then the expression $(\tau_{1}+\tau_{2})$
is a term too.
The set $F$ of formulas is the least set of expressions that contains the
equalities (i.e. the expressions of the form $(\tau_{1}=\tau_{2})$) and closed
with respect to the following formation rules: if expressions $\alpha$ and
$\beta$ are formulas, then the aexpression of the form

$(\alpha\lor\beta),\ (\alpha\land\beta),\ (\alpha\implies\beta),\ \lnot\alpha$

are also formulas, moreover, the expressions of the form

$\forall_{x}\,\alpha,\ \exists_{x}\,\alpha$

where $x$ is a variable and $\alpha$ is a formula, are formulas too.

  * $\mathcal{C}$

is the operation of consquence determined by axioms of first-order logic and
the inference rules of the logic,

  * $Ax$

is the set of formulas listed below.

$\displaystyle\forall_{x}\ x+1\neq 0$ (a)
$\displaystyle\forall_{x}\,\forall_{y}\ x+1=y+1\implies x=y$ (b)
$\displaystyle\forall_{x}\ x+0=x$ (c) $\displaystyle\forall_{x,y}\
(y+1)+x=(y+x)+1$ (d)
$\displaystyle\Phi(0)\land\forall_{x}\,[\Phi(x)\implies\Phi(x+1)]\implies\forall_{x}\Phi(x)$
(I)

The expression $\Phi(x)$ may be replaced by any formula. The result is an
axiom of theory This is the induction scheme.
We augment the set of axioms adding four axioms that define a coiple of useful
notions.

$\displaystyle even(x)\stackrel{{\scriptstyle
df}}{{\equiv}}\exists_{y}\,x=y+y$ (e) $\displaystyle
odd(x)\stackrel{{\scriptstyle df}}{{\equiv}}\exists_{y}\,x=y+y+1$ (o)
$\displaystyle x\,div\,2=y\equiv(x=y+y\,\lor\,x=y+y+1)$ (D2) $\displaystyle
3x\stackrel{{\scriptstyle df}}{{=}}x+x+x$ (3x)

The theory $\mathcal{T}^{\prime}$ obtained in this way is a conservative
extension of theory $\mathcal{T}$.

Below we present another theory $\mathcal{AP}$ c.f. [Pre29], we shall use two
facts: 1) theory $\mathcal{AP}$ is complete and hence is decidable, 2) both
theories are elementarily equivalent.

###### Definition 33

Theory $\mathcal{AP}=\langle\mathcal{L},\mathcal{C},AxP\rangle$ is a system of
three elements :

  * $\mathcal{L}$

is a language of first-order. The alphabet of this language contains the set
$V$ of variables, symbols of functors : $0,+$, symbol of equality predicate
$=$.
The set of well formed-expressions is the union of set of terms $T$ and set of
formulas $F$. The set of terms $T$ is the least set of expressions that
contains the set of variables $V$ and the expression $0$ and closed with
respect to the following two rules: 1) if two expressions $\tau_{1}$ and
$\tau_{2}$ are terms, then the expression $(\tau_{1}+\tau_{2})$ is also a
term, 2) if the expression $\tau$ is a term, then the expression $S(\tau)$ is
also a term.

  * $\mathcal{C}$

is the consequence operation determined by the axioms of predicate calculus
and inference rules of first-order logic

  * $AxP$

The set of axioms of the $\mathcal{AP}$ theory is listed below.

$\displaystyle\forall_{x}\ x+1\neq 0$ (A) $\displaystyle\forall_{x}\ x\neq
0\implies\exists_{y}x=y+1$ (B) $\displaystyle\forall_{x,y}\ x+y=y+x$ (C)
$\displaystyle\forall_{x,y,z}\ x+(y+z)=(x+y)+z$ (D)
$\displaystyle\forall_{x,y,z}\ x+z=y+z\implies x=y$ (E)
$\displaystyle\forall_{x}\ x+0=x$ (F) $\displaystyle\forall_{x,z}\
\exists_{y}\ (x=y+z\lor z=y+x)$ (G) $\displaystyle\forall_{x}\,\exists_{y}\
(x=y+y\lor x=y+y+1)$ (H2) $\displaystyle\forall_{x}\,\exists_{y}\ (x=y+y+y\lor
x=y+y+y+1\lor x=y+y+y+1+1)$ (H3) . . . . . . . . .
$\displaystyle\forall_{x}\,\exists_{y}\
\left(\begin{array}[]{l}x=\underbrace{y+y+\dots+y}_{k}\,\lor\\\ \ \ \
x=\underbrace{y+y+\dots+y}_{k}+1\,\lor\\\ \ \ \ \ \ \
x=\underbrace{y+y+\dots+y}_{k}+\underbrace{1+1}_{2}\,\lor\\\ \dots\\\ \ \ \ \
\ \ \ \ \
x=\underbrace{y+y+\dots+y}_{k}+\underbrace{1+1+\dots+1}_{k-2}\,\lor\\\ \ \ \ \
\ \ \ \ \ \ \ \
x=\underbrace{y+y+\dots+y}_{k}+\underbrace{1+1+\dots+1}_{k-1}\end{array}\right)$
…

The axioms $H2$ -$Hk$ … may be given a shorter form. Let us introduce
numerals, ie. the constants representing term of the form

$\displaystyle\textbf{\text@underline{2}}\stackrel{{\scriptstyle df}}{{=}}1+1$
$\displaystyle\textbf{\text@underline{3}}\stackrel{{\scriptstyle
df}}{{=}}1+1+1$ $\displaystyle\cdots$
$\displaystyle\textbf{\text@underline{k}}\stackrel{{\scriptstyle
df}}{{=}}\underbrace{1+1+\dots 1}_{k\ \text{ times}}$ $\displaystyle\cdots$

Now, the axioms take form

$\displaystyle\forall_{x}\
x\text{\,mod\,}\textbf{\text@underline{2}}=\textbf{\text@underline{0}}\lor
x\text{\,mod\,}\textbf{\text@underline{2}}=\textbf{\text@underline{1}}$ (H2’)
$\displaystyle\forall_{x}\
x\text{\,mod\,}\textbf{\text@underline{3}}=\textbf{\text@underline{0}}\lor
x\text{\,mod\,}\textbf{\text@underline{3}}=\textbf{\text@underline{1}}\lor
x\text{\,mod\,}\textbf{\text@underline{3}}=\textbf{\text@underline{2}}$ (H3’)
$\displaystyle\cdots$ $\displaystyle\forall_{x}\bigvee_{j=0}^{k-1}\
x\text{\,mod\ }\textbf{\text@underline{k}}=\textbf{\text@underline{j}}$ (Hk’)

Let us recall a couple of useful theorems
F1. Theory $\mathcal{T}$ is elementarily equivalent to the theory
$\mathcal{AP}$.[Pre29] [Sta84]
F2. Theory $\mathcal{AP}$ is decidable. [Pre29].
F3. The computational complexity of theory $\mathcal{AP}$, is double
exponential $O(2^{2^{n}})$ this result belongs to Fisher and Rabin, see
[MF74].
F4. Theories $\mathcal{T}$ and $\mathcal{AP}$ have non-standard model, see
section 6.1, p. 6.1.
Now, we shall prove a couple of useful theorems of theory $\mathcal{T}$.
First, we shall show that the sentence $\forall_{n}\exists_{x,y,z}\,n\cdot
3^{x}+y=2^{z}$ is a theorem of the theory $\mathcal{T}$ of addition.
Operations of multiplication and power are inaccessible in the theory
$\mathcal{T}$. However, we do not need them.
We enrich the theory $\mathcal{T}$ adding two functions $P2(\cdot)$ and
$P3(\cdot.\cdot).$ defined in this way

###### Definition 34

Two functions are defined $P2$ (of oneargument) and $P3$ (of two-arguments).
$\begin{array}[]{l|l}P2(0)\stackrel{{\scriptstyle
df}}{{=}}1&P3(y,0)\stackrel{{\scriptstyle df}}{{=}}y\\\
P2(x+1)\stackrel{{\scriptstyle
df}}{{=}}P2(x)+P2(x)&P3(y,x+1)\stackrel{{\scriptstyle
df}}{{=}}P3(y,x)+P3(y,x)+P3(y,x)\end{array}$

###### Lemma 35

The definitions given above are correct, i.e. the following sentences
aretheorems of the theory with two definitions

$\mathcal{T}\vdash\forall_{x}\exists_{y}\,P2(x)=y\ \ \mbox{and }$
$\mathcal{T}\vdash\forall_{x,y,z}P2(x)=y\land P2(x)=z\implies y=z.$

Similarly, the sentences $\forall_{y,x}\exists_{z}\,P3(y,x)=z$ and
$\forall_{y,x,z,u}P3(y,x)=z\land P3(y,x)=u\implies z=u$ are theorems of theory
$\mathcal{T}$ .

An easy proof goes by induction with respect to the value of variable $x$.

In the proof of the lemma 36 , below, we shall use the definition of the order
relation

$a<b\stackrel{{\scriptstyle df}}{{=}}\exists_{c\neq 0}\ a+c=b.$

Making use of the definition of function $P2$ and $P3$ we shall write the
formula $P3(n,x)+y=P2(z)$ as it exppresses the same content as expression
$n\cdot 3^{x}+y=2^{z}$.

###### Lemma 36

The following sentence is a theorem of the theory $\mathcal{T}$ enriched by
the definitions of $P2$ and $P3$ functions.

$\forall_{n}\exists_{x,y,z}P3(n,x)+y=P2(z)$

Proof. We begin proving by induction that
$\mathcal{T}\vdash\forall_{n}\,n<2^{n}$. It is easy to see that
$\mathcal{T}\vdash 0<P2(0)$. We shall prove that
$\mathcal{T}\vdash\forall_{n}(n<P2(n)\implies(n+1<P2(n+1))$. Inequality
$n+1<P2(n+1)$ follows from the two following inequalities $\mathcal{T}\vdash
n<P2(n)$ and $\mathcal{T}\vdash 1<P2(n)$. Hence the formula $n+1<P2(n)+P2(n))$
is a theorem of theory $\mathcal{T}$. By definition $P2(n)+P2(n)=P2(n+1)$.
In the similar manner, we can prove the formula
$\mathcal{T}\vdash\forall_{n}\,\forall_{x}\,P3(n,x)<P2(n+x+x)$
As a consequence we have $\mathcal{T}\vdash\forall_{n}\exists_{x,y,z}\
P3(n,x)+y=P2(z)$.

###### Lemma 37

Let $\mathfrak{M}$ be any model of Presburger arithmetic. If there exists a
triple $\langle x,y,z\rangle$ of reachable elements such that it satisfies the
equation $P3(n,x)+y=P2(z)$ i.e. $n\cdot 3^{x}+y=2^{z}$ then the element $n$ is
reachable.

Proof. If the following formulas are valid in the structure $\mathfrak{M}$
$\\{q:=0;\,\mathbf{while}\ q\neq x\ \mathbf{do}\ q:=q+1\ \mathbf{od}\\}(x=q)$,
$\\{q:=0;\,\mathbf{while}\ q\neq y\ \mathbf{do}\ q:=q+1\ \mathbf{od}\\}(y=q)$,
$\\{q:=0;\,\mathbf{while}\ q\neq z\ \mathbf{do}\ q:=q+1\ \mathbf{od}\\}(z=q)$
and the following equation is valid too $P3(n,x)+y=P2(z)$ then it is easy to
verify that the formula $\\{t:=0;\,\mathbf{while}\ n\neq t\ \mathbf{do}\
t:=t+1\ \mathbf{od}\\}(t=n)$ is valid too.
Nr Reason 1 a1=P2(z) is reachable 2 y+a2 =a1, a2 is reachable and a2=$2^{z}$-y
3 a3=P3(1,x) is reachable , a3=$3^{x}$ 4
$\left\\{\begin{array}[]{l}q:=1;a5:=a3;\\\ \textbf{while}\ a5\neq a2\
\textbf{do}\\\ \ \ q:=q+1;\\\ \ \ a5:=a5+a3\\\
\textbf{od}\end{array}\right\\}(q*a3=a2)$ hence q=n

###  6.3 An introduction to calculus of programs $\mathcal{AL}$

For the convenience of the reader we cite the axioms and inference rules of
calculus of programs i.e. algorithmic logic $\mathcal{AL}$.
Note. Every axiom of algorihmic logic is a tautology.
Every inference rule of $\mathcal{AL}$ is sound. [MS87]

Axioms

  * axioms of propositional calculus

  * $Ax_{1}$

$((\alpha\Rightarrow\beta)\Rightarrow((\beta\Rightarrow\delta)\Rightarrow(\alpha\Rightarrow\delta)))$

  * $Ax_{2}$

$(\alpha\Rightarrow(\alpha\vee\beta))$

  * $Ax_{3}$

$(\beta\Rightarrow(\alpha\vee\beta))$

  * $Ax_{4}$

$((\alpha\Rightarrow\delta)~{}\Rightarrow((\beta\Rightarrow\delta)~{}\Rightarrow~{}((\alpha\vee\beta)\Rightarrow\delta)))$

  * $Ax_{5}$

$((\alpha\wedge\beta)\Rightarrow\alpha)$

  * $Ax_{6}$

$((\alpha\wedge\beta)\Rightarrow\beta)$

  * $Ax_{7}$

$((\delta\Rightarrow\alpha)\Rightarrow((\delta\Rightarrow\beta)\Rightarrow(\delta\Rightarrow(\alpha\wedge\beta))))$

  * $Ax_{8}$

$((\alpha\Rightarrow(\beta\Rightarrow\delta))\Leftrightarrow((\alpha\wedge\beta)\Rightarrow\delta))$

  * $Ax_{9}$

$((\alpha\wedge\lnot\alpha)\Rightarrow\beta)$

  * $Ax_{10}$

$((\alpha\Rightarrow(\alpha\wedge\lnot\alpha))\Rightarrow\lnot\alpha)$

  * $Ax_{11}$

$(\alpha\vee\lnot\alpha)$

  * axioms of predicate calculus

  * $Ax_{12}$

$((\forall x)\alpha(x)\Rightarrow\alpha(x/\tau)))$
where term $\tau$ is of the same type as the variable x

  * $Ax_{13}$

$(\forall x)\alpha(x)\Leftrightarrow\lnot(\exists x)\lnot\alpha(x)$

  * axioms of calculus of programs

  * $Ax_{14}$

$K((\exists x)\alpha(x))\Leftrightarrow(\exists y)(K\alpha(x/y))$ for $y\notin
V(K)$

  * $Ax_{15}$

$K(\alpha\vee\beta)\Leftrightarrow((K\alpha)\vee(K\beta))$

  * $Ax_{16}$

$K(\alpha\wedge\beta)\Leftrightarrow((K\alpha)\wedge(K\beta))$

  * $Ax_{17}$

$K(\lnot\alpha)\Rightarrow\lnot(K\alpha)$

  * $Ax_{18}$

$((x:=\tau)\gamma\Leftrightarrow(\gamma(x/\tau)\wedge(x:=\tau)true))~{}\wedge((q:=\gamma\prime)\gamma\Leftrightarrow\gamma(q/\gamma\prime))$

  * $Ax_{19}$

begin $K;M$ end $\alpha\Leftrightarrow K(M\alpha)$

  * $Ax_{20}$

if $\gamma$ then $K$ else $M$ fi $\alpha\Leftrightarrow((\lnot\gamma\wedge
M\alpha)\vee(\gamma\wedge K\alpha))$

  * $Ax_{21}$

while $\gamma$ do $K$ od
$\alpha\Leftrightarrow((\lnot\gamma\wedge\alpha)\vee(\gamma\wedge K($while
$\gamma$ do $K$ od$(\lnot\gamma\wedge\alpha))))$

  * $Ax_{22}$

$\displaystyle{\bigcap K\alpha\Leftrightarrow(\alpha\wedge(K\bigcap
K\alpha))}$

  * $Ax_{23}$

$\displaystyle{\bigcup K\alpha\equiv(\alpha\vee(K\bigcup K\alpha))}$

Inference rules

  * propositional calculus

  * $R_{1}$

$\dfrac{\alpha,(\alpha\Rightarrow\beta)}{\beta}$ (also known as modus ponens)

  * predicate calculus

  * $R_{6}$

$\dfrac{(\alpha(x)~{}\Rightarrow~{}\beta)}{((\exists
x)\alpha(x)~{}\Rightarrow~{}\beta)}$

  * $R_{7}$

$\dfrac{(\beta~{}\Rightarrow~{}\alpha(x))}{(\beta\Rightarrow(\forall
x)\alpha(x))}$

  * calculus of programs AL

  * $R_{2}$

$\dfrac{(\alpha\Rightarrow\beta)}{(K\alpha\Rightarrow K\beta)}$

  * $R_{3}$

$\dfrac{\\{s({\bf if}\ \gamma\ {\bf then}\ K\ {\bf
fi})^{i}(\lnot\gamma\wedge\alpha)\Rightarrow\beta\\}_{i\in N}}{(s({\bf while}\
\gamma\ {\bf do}\ K\ {\bf od}\ \alpha)\Rightarrow\beta)}$

  * $R_{4}$

$\dfrac{\\{(K^{i}\alpha\Rightarrow\beta)\\}_{i\in N}}{(\bigcup
K\alpha\Rightarrow\beta)}$

  * $R_{5}$

$\dfrac{\\{(\alpha\Rightarrow K^{i}\beta)\\}_{i\in
N}}{(\alpha\Rightarrow\bigcap K\beta)}$

In rules $R_{6}$ and $R_{7}$, it is assumed that $x$ is a variable which is
not free in $\beta$, i.e. $x\notin FV(\beta)$. The rules are known as the rule
for introducing an existential quantifier into the antecedent of an
implication and the rule for introducing a universal quantifier into the
successor of an implication. The rules $R_{4}$ and $R_{5}$ are algorithmic
counterparts of rules $R_{6}$ and $R_{7}$. They are of a different character,
however, since their sets of premises are infinite. The rule $R_{3}$ for
introducing a while into the antecedent of an implication of a similar nature.
These three rules are called $\omega$-rules. The rule $R_{1}$ is known as
modus ponens, or the cut-rule. In all the above schemes of axioms and
inference rules, $\alpha$, $\beta$, $\delta$ are arbitrary formulas, $\gamma$
and $\gamma^{\prime}$ are arbitrary open formulas, $\tau$ is an arbitrary
term, $s$ is a finite sequence of assignment instructions, and $K$ and $M$ are
arbitrary programs.

######  Theorem 38 (theorem on completeness of the calculus  $\mathcal{AL}$)

Let $\mathcal{T}=\langle\mathcal{L},\mathcal{C},\mathcal{A}x\rangle$ be a
consistent algorithmic theory, let $\alpha\in\mathcal{L}$ be a formula. The
following conditions are equivalent

  1. (i)

Formula $\alpha$ is a theorem of the theory T,
$\alpha\in\mathcal{C}(\mathcal{A}x)$,

  2. (ii)

Formula $\alpha$ is valid in every model of the theory T,
$\mathcal{A}x\models\alpha$.

The proof may be found in [MS87].

###  6.4 An introduction to algorithmic theory of natural numbers
$\mathcal{ATN}$

The language of algorithmic theory of natural numbers $\mathcal{ATN}$ is very
simple. Its alphabet contains one constant 0 zero , one one-argument functor
$s$ and predicate = of equality. We shall write $x+1$ instead of $s(x)$.
Axioms of $\mathcal{ATN}$ were presented in the book [MS87]

$\begin{array}[]{llr}A_{1})&\forall x\\{q:=0;\,\textbf{while}\ q\neq x\
\textbf{do}\ q:=s(q)\ \textbf{od}\\}(q=x)&\qquad\ \qquad(R)\\\ A_{2})&\forall
x\ s(x)\neq 0&\qquad\ \qquad(N)\\\ A_{3})&\forall x\forall
y\,s(x)=s(y)\implies x=y&\qquad\ \qquad(J)\end{array}$

We can add another two-argument functor + and its definition
$\begin{array}[]{llr}A_{4})&\forall x\,\forall
y\left\\{\begin{array}[]{l}q:=0;w:=x;\\\ \textbf{while}\ q\neq y\
\textbf{do}\\\ \quad q:=s(q)\ ;w:=s(w)\\\
textbf{od}\end{array}\right\\}(x+y=w)&\quad(D)\end{array}$
The termination property of the program in $A_{4}$ is a theorem of
$\mathcal{ATN}$ theory as well as the formulas $x+0=x$ and $x+s(y)=s(x+y)$.

#### A sample (8 – 20) of Theorems of $\mathcal{ATN}$

$\displaystyle\mathcal{ATN}$
$\displaystyle\vdash{\exists_{x}\,\alpha(x)\Leftrightarrow\\{x:=0\\}\bigcup\\{x:=x+1\\}\alpha(x)}$
(8) $\displaystyle\mathcal{ATN}$
$\displaystyle\vdash{\forall_{x}\,\alpha(x)\Leftrightarrow\\{x:=0\\}\bigcap\\{x:=x+1\\}\alpha(x)}$
(9) Law of Archimedes $\displaystyle\mathcal{ATN}$ $\displaystyle\vdash
0<x<y\implies\\{a:=x;\,\mathbf{while}\ a<y\ \mathbf{do}\ a:=a+x\
\mathbf{od}\\}(a\geq y)$ (10) Scheme of induction $\displaystyle\mathcal{ATN}$
$\displaystyle\vdash\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\Bigl{(}\alpha(x/0)\land\forall_{x}\bigl{(}\alpha(x)\Rightarrow\alpha(x/s(x))\bigr{)}\Bigr{)}\implies\forall_{x}\alpha(x)}$
(11) Correctness of Euclid’s algorithm $\displaystyle\mathcal{ATN}$
$\displaystyle\vdash\left(\begin{array}[]{l}n_{0}>0\land\\\
m_{0}>0\end{array}\right)\implies\left\\{\begin{array}[]{l}n:=n_{0};\
m:=m_{0};\\\ \mathbf{while}\,n\neq m\,\mathbf{do}\\\ \quad\mathbf{if}\,n>m\
\mathbf{then}\ \ n:=n\stackrel{{\scriptstyle.}}{{\\_}}m\\\
\qquad\mathbf{else}\ \ m:=m\stackrel{{\scriptstyle.}}{{\\_}}n\\\
\quad\mathbf{fi}\\\ \mathbf{od}\end{array}\right\\}(n=gcd(n_{0},m_{0}))\ $
(20)

The theory $\mathcal{ATN}$ enjoys an important property of categoricity.

######  Theorem 39 ( meta-theorem on categoricity of $\mathcal{ATN}$ theory)

Every model $\mathfrak{A}$ of the algorithmic theory of natural numbers is
isomorphic to the structure $\mathfrak{N}$, c.f. subsection 6.1.

###  6.5 Proof of lemma 4

Let $P$ and $P^{\prime}$ be two programs. Let $\alpha$ be any formula. The
semantic property programs $P$ and $P^{\prime}$ are equivalent with respect to
the postcondition $\alpha$ is expressed by the formula of the form
$(\\{P\\}\,\alpha\Leftrightarrow\\{P^{\prime}\\}\,\alpha)$.
We shall use the following tautology of calculus of programs $\mathcal{AL}$.

$\vdash\left(\overbrace{\left\\{\begin{array}[]{l}\textbf{while}\ \,\gamma\
\textbf{do}\\\ \quad\textbf{if}\ \,\delta\ \textbf{then}\ K\ \textbf{else}\ M\
\textbf{fi}\\\ \textbf{od};\\\
\end{array}\right\\}}^{P:}\,\alpha\Leftrightarrow\overbrace{\left\\{\begin{array}[]{l}\textbf{while}\
\gamma\ \textbf{do }\\\ \quad\begin{array}[]{l}\textbf{while}\
\gamma\land\delta\ \textbf{do}\ K\ \textbf{od};\\\ \textbf{while}\
\gamma\land\lnot\delta\ \textbf{do}\ M\ \textbf{od }\\\ \end{array}\\\
\textbf{od}\\\ \end{array}\right\\}}^{P^{\prime}:}\,\alpha\right)$ (21)

We apply the axioms Ax20 and Ax21

$\vdash\left(\left\\{\begin{array}[]{l}\textbf{while}\ \,\gamma\
\textbf{do}\\\ \quad\textbf{if}\ \,\delta\ \textbf{then}\ K\ \textbf{else}\ M\
\textbf{fi}\\\ \textbf{od};\\\
\end{array}\right\\}\,\alpha\Leftrightarrow\left\\{\begin{array}[]{l}\textbf{if}\
\gamma\ \textbf{then }\\\ \quad\begin{array}[]{l}\textbf{while}\
\gamma\land\delta\ \textbf{do}\ K\ \textbf{od};\\\ \textbf{while}\
\gamma\land\lnot\delta\ \textbf{do}\ M\ \textbf{od };\\\ \textbf{while}\
\gamma\ \textbf{do }\\\ \quad\textbf{while}\ \gamma\land\delta\ \textbf{do}\
K\ \textbf{od};\\\ \quad\textbf{while}\ \gamma\land\lnot\delta\ \textbf{do}\
M\ \textbf{od }\\\ \end{array}\\\ \qquad\textbf{od}\\\ \textbf{fi}\\\
\end{array}\right\\}\,\alpha\right)$ (22)

We can omit the instruction if (why?) . We swap internal instructions while
inside the instruction while.

$\vdash\left(\left\\{\begin{array}[]{l}\textbf{while}\ \,\gamma\
\textbf{do}\\\ \quad\textbf{if}\ \,\delta\ \textbf{then}\ K\ \textbf{else}\ M\
\textbf{fi}\\\ \textbf{od};\\\
\end{array}\right\\}\,\alpha\Leftrightarrow\left\\{\begin{array}[]{l}\textbf{while}\
\gamma\land\delta\ \textbf{do}\ K\ \textbf{od };\\\ \textbf{while}\
\gamma\land\lnot\delta\ \textbf{do}\ M\ \textbf{od}\\\ \textbf{while}\ \gamma\
\textbf{do }\\\ \quad\begin{array}[]{l}\textbf{while}\ \gamma\land\lnot\delta\
\textbf{do}\ M\ \textbf{od};\\\ \textbf{while}\ \gamma\land\delta\
\textbf{do}\ K\ \textbf{od }\\\ \end{array}\\\ \textbf{od}\\\
\end{array}\right\\}\,\alpha\right)$ (23)

We can safely skip the second instruction while.

$\vdash\left(\left\\{\begin{array}[]{l}\textbf{while}\ \,\gamma\
\textbf{do}\\\ \quad\textbf{if}\ \,\delta\ \textbf{then}\ K\ \textbf{else}\ M\
\textbf{fi}\\\ \textbf{od};\\\
\end{array}\right\\}\,\alpha\Leftrightarrow\left\\{\begin{array}[]{l}\textbf{while}\
\gamma\land\delta\ \textbf{do}\ K\ \textbf{od };\\\ \textbf{while}\ \gamma\
\textbf{do }\\\ \quad\begin{array}[]{l}\textbf{while}\ \gamma\land\lnot\delta\
\textbf{do}\ M\ \textbf{od};\\\ \textbf{while}\ \gamma\land\delta\
\textbf{do}\ K\ \textbf{od }\\\ \end{array}\\\ \textbf{od}\\\
\end{array}\right\\}\,\alpha\right)$ (24)

Now, we put $(\gamma\stackrel{{\scriptstyle df}}{{=}}n\neq 1)$,
$(\delta\stackrel{{\scriptstyle df}}{{=}}even(n))$, $(K\stackrel{{\scriptstyle
df}}{{=}}\left\\{n:=n\div 2\right\\})$ and $(M\stackrel{{\scriptstyle
df}}{{=}}\left\\{n:=3n+1\right\\})$. We make use of two theorems
$(even(n)\implies n\neq 1)$ and $(M\delta)$ of theory $\mathcal{AP}$ c.f.
subsection 6.2.

$\mathcal{T}\vdash\left(\left\\{\begin{array}[]{l}\textbf{while}\ n\neq 1\
\textbf{do}\\\ \quad\begin{array}[]{|l|}\hline\cr\textbf{if}\ even(n)\\\
\textbf{then}\ n:=n\div 2\\\ \textbf{else}\ n:=3n+1\\\ \textbf{fi}\\\
\hline\cr\end{array}\\\ \textbf{od};\\\
\end{array}\right\\}\,(n=1)\Leftrightarrow\left\\{\begin{array}[]{l}\textbf{while}\
even(n)\ \textbf{do }n:=n\div 2\ \textbf{od};\\\ \textbf{while}\ n\neq 1\
\textbf{do }\\\ \quad\begin{array}[]{|l|}\hline\cr n:=3n+1;\\\ \textbf{while
}\ even(n)\ \textbf{do}\ n:=n\div 2\ \textbf{od}\\\ \hline\cr\end{array}\\\
\textbf{od}\\\ \end{array}\right\\}\,(n=1)\right).$ (25)

###  6.6 Proof of invariant of algorithm $Gr3$

We are going to prove the following implication (27) is a theorem of
algorithmic theory of natural numbers $\mathcal{ATN}$.

$\mathcal{ATN}\vdash(\varphi\implies\\{\Delta_{3}\\}\varphi)$ (26)
$\overbrace{\left(\begin{array}[]{l}n\cdot 3^{i}+Y_{i}=m_{i}\cdot
2^{Z_{i}}\land\\\ Z_{i}=\sum\limits_{j=0}^{i}\,k_{j}\land X_{i}=i\land\\\
Y_{i}=\sum\limits_{j=0}^{i-1}\biggl{(}3^{i-1-j}\cdot
2^{Z_{j}}\biggr{)}\land\\\ m_{0}=n\land\ k_{0}=exp(m_{0},2)\land\\\
\mathop{\forall}\limits_{0<l\leq i}\,\bigl{(}m_{l}=m_{l-1}/2^{k_{l}}\land\\\
k_{l}=exp(m_{l},2)\bigr{)}\\\
\end{array}\right)}^{\varphi}\implies\overbrace{\left\\{\begin{array}[]{l}\
aux:=3*m_{i}+1;\\\ \ k_{i+1}:=exp(aux,2);\\\ m_{i+1}:=aux/2^{k_{i+1}};\\\ \
Y_{i+1}:=3Y_{i}+2^{Z_{i}};\\\ Z_{i+1}:=Z_{i}+k_{i+1};\\\ X_{i}:=i;;\\\
\hline\cr\ i:=i+1;\\\
\end{array}\right\\}}^{\Delta_{3}}\,\overbrace{\left(\begin{array}[]{l}n\cdot
3^{i}+Y_{i}=m_{i}\cdot 2^{Z_{i}}\land\\\
Z_{i}=\sum\limits_{j=0}^{i}\,k_{j}\land\land X_{i}=i\\\
Y_{i}=\sum\limits_{j=0}^{i-1}\biggl{(}3^{i-1-j}\cdot
2^{Z_{j}}\biggr{)}\land\\\ m_{0}=n\land\ k_{0}=exp(m_{0},2)\land\\\
\mathop{\forall}\limits_{0<l\leq i}\,\bigl{(}m_{l}=m_{l-1}/2^{k_{l}}\land\\\
k_{l}=exp(m_{l},2)\bigr{)}\\\ \end{array}\right)}^{\varphi}$ (27)

We apply the axiom of assignment instruction $Ax_{18}$. Note, we applied also
axiom $Ax_{19}$ of composed instruction. Namely, in the implication (27) we
replace the its successor $\\{\Delta_{3}\\}\varphi$ by the formula
$\\{\Delta_{3}^{(1)}\\}\varphi^{(1)}$.

$\varphi\implies\overbrace{\left\\{\begin{array}[]{l}\ aux:=3*m_{i}+1;\\\ \
k_{i+1}:=exp(aux,2);\\\ m_{i+1}:=aux/2^{k_{i+1}};\\\ \
Y_{i+1}:=3Y_{i}+2^{Z_{i}};\\\ Z_{i+1}:=Z_{i}+k_{i+1};\\\ \hline\cr
X_{i}:=i;;\\\
\end{array}\right\\}}^{\Delta_{3}^{(1)}}\,\overbrace{\left(\begin{array}[]{l}\
n\cdot 3^{(i+1)}+Y_{(i+1)}=m_{(i+1)}\cdot 2^{Z_{(i+1)}}\land\\\
Z_{(i+1)}=\sum\limits_{j=0}^{(i+1)}\,k_{j}\land X_{i+1}={(i+1)}\land\\\
Y_{(i+1)}=\sum\limits_{j=0}^{i}\biggl{(}3^{{(i+1)}-1-j}\cdot
2^{Z_{j}}\biggr{)}\land\\\ m_{0}=n\land\ k_{0}=exp(m_{0},2)\land\\\
\mathop{\forall}\limits_{0<l\leq{(i+1)}}\,\bigl{(}m_{l}=m_{l-1}/2^{k_{l}}\land
k_{l}=exp(m_{l},2)\bigr{)}\\\ \end{array}\right)}^{\varphi^{(1)}}$ (28)
$\varphi\implies\left\\{\begin{array}[]{l}\ aux:=3*m_{i}+1;\\\ \
k_{i+1}:=exp(aux,2);\\\ m_{i+1}:=aux/2^{k_{i+1}};\\\ \
Y_{i+1}:=3Y_{i}+2^{Z_{i}};\\\ \hline\cr Z_{i+1}:=Z_{i}+k_{i+1};\\\
\end{array}\right\\}\,\left(\begin{array}[]{l}n\cdot
3^{(i+1)}+Y_{(i+1)}=m_{(i+1)}\cdot 2^{Z_{(i+1)}}\land\\\
Z_{(i+1)}=\sum\limits_{j=0}^{(i+1)}\,k_{j}\land X_{i+1}={(i+1)}\land\\\
Y_{(i+1)}=\sum\limits_{j=0}^{i}\biggl{(}3^{{(i+1)}-1-j}\cdot
2^{Z_{j}}\biggr{)}\land\\\ m_{0}=n\land\ k_{0}=exp(m_{0},2)\land\\\
\mathop{\forall}\limits_{0<l\leq{(i+1)}}\,\bigl{(}m_{l}=m_{l-1}/2^{k_{l}}\land
k_{l}=exp(m_{l},2)\bigr{)}\land\\\ \end{array}\right)$ (29)
$\varphi\implies\left\\{\begin{array}[]{l}\ aux:=3*m_{i}+1;\\\ \
k_{i+1}:=exp(aux,2);\\\ m_{i+1}:=aux/2^{k_{i+1}};\\\ \hline\cr\
Y_{i+1}:=3Y_{i}+2^{Z_{i}};\\\
\end{array}\right\\}\,\left(\begin{array}[]{l}n\cdot
3^{(i+1)}+Y_{(i+1)}=m_{(i+1)}\cdot 2^{(Z_{i}+k_{i+1})}\land\\\
(Z_{i}+k_{i+1})=\sum\limits_{j=0}^{(i+1)}\,k_{j}\land X_{i+1}={(i+1)}\land\\\
Y_{(i+1)}=\sum\limits_{j=0}^{i}\biggl{(}3^{{(i+1)}-1-j}\cdot
2^{Z_{j}}\biggr{)}\land\\\ m_{0}=n\land\ k_{0}=exp(m_{0},2)\land\\\
\mathop{\forall}\limits_{0<l\leq{(i+1)}}\,\bigl{(}m_{l}=m_{l-1}/2^{k_{l}}\land
k_{l}=exp(m_{l},2)\bigr{)}\\\ \end{array}\right)$ (30)
$\varphi\implies\left\\{\begin{array}[]{l}\ \ aux:=3*m_{i}+1;\\\ \
k_{i+1}:=exp(aux,2);\\\ \hline\cr m_{i+1}:=aux/2^{k_{i+1}};\\\
\end{array}\right\\}\,\left(\begin{array}[]{l}\ n\cdot
3^{(i+1)}+(3Y_{i}+2^{Z_{i}})=m_{(i+1)}\cdot 2^{(Z_{i}+k_{i+1})}\land\\\
(Z_{i}+k_{i+1})=\sum\limits_{j=0}^{(i+1)}\,k_{j}\land X_{i+1}={(i+1)}\land\\\
(3Y_{i}+2^{Z_{i}})=\sum\limits_{j=0}^{i}\biggl{(}3^{{(i+1)}-1-j}\cdot
2^{Z_{j}}\biggr{)}\land\\\ m_{0}=n\land\ k_{0}=exp(m_{0},2)\land\\\
\mathop{\forall}\limits_{0<l\leq{(i+1)}}\,\bigl{(}m_{l}=m_{l-1}/2^{k_{l}}\land
k_{l}=exp(m_{l},2)\bigr{)}\\\ \end{array}\right)$ (31)
$\varphi\implies\left\\{\begin{array}[]{l}\ aux:=3*m_{i}+1;\\\ \hline\cr\
k_{i+1}:=exp(aux,2);\\\ \end{array}\right\\}\,\left(\begin{array}[]{l}n\cdot
3^{(i+1)}+(3Y_{i}+2^{Z_{i}})=(aux/2^{k_{i+1}})\cdot
2^{(Z_{i}+k_{i+1})}\land\\\
(Z_{i}+k_{i+1})=\sum\limits_{j=0}^{(i+1)}\,k_{j}\land X_{i+1}={(i+1)}\land\\\
(3Y_{i}+2^{Z_{i}})=\sum\limits_{j=0}^{i}\biggl{(}3^{{(i+1)}-1-j}\cdot
2^{Z_{j}}\biggr{)}\land\\\ m_{0}=n\land\ k_{0}=exp(m_{0},2)\land\\\
\mathop{\forall}\limits_{0<l\leq{(i+1)}}\,\bigl{(}m_{l}=m_{l-1}/2^{k_{l}}\land
k_{l}=exp(m_{l},2)\bigr{)}\\\ \end{array}\right)$ (32)
$\varphi\implies\left\\{\begin{array}[]{l}\ aux:=3*m_{i}+1;\\\
\end{array}\right\\}\,\left(\begin{array}[]{l}n\cdot
3^{(i+1)}+(3Y_{i}+2^{Z_{i}})=(aux/2^{(exp(aux,2)))}\cdot
2^{(Z_{i}+(exp(aux,2)))}\land\\\
(Z_{i}+(exp(aux,2)))=\sum\limits_{j=0}^{(i+1)}\,k_{j}\land
X_{i+1}={(i+1)}\land\\\
(3Y_{i}+2^{Z_{i}})=\sum\limits_{j=0}^{i}\biggl{(}3^{{(i+1)}-1-j}\cdot
2^{Z_{j}}\biggr{)}\land\\\ m_{0}=n\land\ k_{0}=exp(m_{0},2)\land\\\
\mathop{\forall}\limits_{0<l\leq{(i+1)}}\,\bigl{(}m_{l}=m_{l-1}/2^{k_{l}}\land
k_{l}=exp(m_{l},2)\bigr{)}\\\ \end{array}\right)\\\ $ (33)
$\varphi\implies\left\\{\begin{array}[]{l}\end{array}\right\\}\,\overbrace{\left(\begin{array}[]{l}n\cdot
3^{(i+1)}+(3Y_{i}+2^{Z_{i}})=((3*m_{i}+1)/2^{(exp((3*m_{i}+1),2)))}\cdot
2^{(Z_{i}+(exp((3*m_{i}+1),2)))}\land\\\
(Z_{i}+(exp((3*m_{i}+1),2)))=\sum\limits_{j=0}^{(i+1)}\,k_{j}\land
X_{i+1}={(i+1)}\land\\\
(3Y_{i}+2^{Z_{i}})=\sum\limits_{j=0}^{i}\biggl{(}3^{{(i+1)}-1-j}\cdot
2^{Z_{j}}\biggr{)}\land\\\ m_{0}=n\land\ k_{0}=exp(m_{0},2)\land\\\
\mathop{\forall}\limits_{0<l\leq{(i+1)}}\,\bigl{(}m_{l}=m_{l-1}/2^{k_{l}}\land
k_{l}=exp(m_{l},2)\bigr{)}\\\ \end{array}\right)}^{\psi}$ (34)

The implications (27) –(34) are mutually equivalent.
One can easily verify that the last implication $(\varphi\implies\psi)\
(\ref{last})$ is a theorem of Presburger arithmetic $\mathcal{T}$ and hence it
is a theorem of $\mathcal{ATN}$ theory.
Therefore the first implication $(\varphi\implies\\{\Delta_{3}\\}\varphi)\
(\ref{first})$ is a theorem of algorithmic theory of natural numbers
$\mathcal{ATN}$.

q.e.d.

###### Remark 40

Note, the process of creation a proof like this can be automatized.
The verification of the above proof can be automatized too.

## References

  * [Grz71] Andrzej Grzegorczyk.  Zarys Arytmetyki Teoretycznej.  PWN, Warszawa, 1971.
  * [Lag10] Jeffrey C. Lagarias, editor.  The Ultimate Challenge: The 3x+1 Problem.  American Mathematical Society, Providence R.I., 2010.
  * [MF74] M.O.Rabin M.J. Fisher.  Super-exponential complexity of presburger arithmetic.  In Proceedings of AMS Symposia on Complexity of Real Computational Processes, volume VIII, 1974.
  * [MS87] Grażyna Mirkowska and Andrzej Salwicki.  Algorithmic Logic.  http://lem12.uksw.edu.pl/wiki/Algorithmic_Logic, 1987.  [Online; accessed 7-August-2017].
  * [MS21] G. Mirkowska and A. Salwicki.  On Collatz theorem.  http://lem12.uksw.edu.pl/images/2/27/On-Collatz-thm-11-10-21.pdf.  [Online: accessed 17 December 2021], 2021.
  * [Pre29] Mojżesz Presburger.  Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen , in welchem die Addition als einzige Operation hervortritt .  pages 92–101,395, 1929.
  * [Sko34] Thoralf Skolem.  Über die nicht-charakterisierbarkeit der zahlenreihe mittels endlich oder abzählbar unendlich vieler aussagen mit ausschließlich zahlenvariablen.  Fundamenta Mathematicae, 23:150–161, 1934.
  * [Sta84] Ryan Stansifer.  Presburger’s Article on Integer Arithmetic: Remarks and Translation.  Cornell University, Technical Report TR84-639, 1984.  http://cs.fit.edu/~ryan/papers/presburger.pdf.  [Online; accessed 6-August-2021].
  * [Tar34] Alfred Tarski.  Bemerkung der Redaktion.  Fundamenta Mathematicae, 23:161, 1934.