Tekst źródłowy strony Collatz theorem

Collatz conjecture is  valid in the standard structure of natural numbers, therefore  it is  <big>Collatz theorem</big> .<br />

Finally!<br />
Many people worked on the Collatz problem for more than 83 years.<br />
We succeeded.  The statute of 'Collatz conjecture" is now [http://lem12.uksw.edu.pl/images/2/21/HotelCollatza.pdf   '''Collatz theorem'''].<br />
Here is a version of June 5, 2022 [https://dx.doi.org/10.2139/ssrn.4158238 '''theorem of Collatz''']  submitted to TCS Journal  .<br />
An abridged version of the proof is  [http://lem12.uksw.edu.pl/images/9/9f/MainPointsProofCollatz.pdf  here].<br />
==ntroduction==
Rozpatrzmy zdanie<br/>
dla każdej liczby naturalnej <math>n</math>, poniższy program <math>Cl </math> ma obliczenie sończone<br/>
<math>\color{blue}\qquad Cl:\,\left\{\begin{array}{l}  \mathbf{while}\ n \neq 0 \ \mathbf{do} \\
\quad \mathbf{if}\  nieparzyste(n) \ \mathbf{then}\  n:=3n+1 \  \mathbf{else}\ n:=n/2\  \mathbf{fi} \\
\mathbf{od} \end{array}\right\} </math> <br />
Zaczynamy od uwagi, że prawdziwośc powyższego zdania pociaga za sobą prawdzowość tezy Collatza, tak jak ona została sformułowana przed II wojną światową. <br />
Ale w  r.1937  nie istniały komputery ani języki programowania<br />
.Z drugiej strony istniała i była już mocno rozwinięta teoria algorytmów. Teorię funkcji rekurencyjnych rozwijanow w Getyndze (David Hilbert i jego uczniowie), Budapeszcie (Rozsza Pterer, Laszlo Kalmar), ...<br />
W Londynie Alan Turing stworzył abstrakcyjną maszynę Turinga.<br />
W Moskwie Kołmogorow i w Kazaniu Malcew badali pojęcie funkcji obliczalnej. <br />
<br />
W Warszawie Alfred Tarski wraz z uczniami Mojżeszem Presburgerem, Stanisławem Jaskowskim uzyskali ważne wyniki dotycące teorii dodawania liczb naturalnych.

==Remark made in  2004==
*The Collatz algorithm does not require operations of multiplication and division. For the operation of multiplying by 3 is done as x+x+x. Division by 2 is done by an auxiliary algorithm.
* In the non-standard model of elementary theory of addition of natural numbers (best known as Presburger arithmetic)  the computation of Collatz algorithm <math>Cl</math>  is infinite for every unreachable number <math>n</math>.
* Hence, Collatz conjecture is unprovable in the elementary theory of addition of natural numbers.
* Moreover, the halting property of Collatz algorithm is not expressible in the language of first-order theory of addition of natural numbers (''aka'' Presburger arithmetic).

==Collatz thesis reformulated ==
In the standard model of natural numbers with addition the Collatz algorithm <math> CL </math> for every number <math> n </math> terminates.<br />
But, how to describe standard model up to isomorphisms?

==Halting formula==
Należy zatem stworzyć formułę <math>\theta</math> (wyrażenie logiczne) taką, że przyjmuje ona wrtośc prawda wtedy i tylko wtedy gdy obliczenie programu <math>Cl</math> jest skończone. Takich formuł jest wiele w języku urachunku programów, tj. logiki algorytmicznej.<br/>
,<math>\qquad \theta:\,\left\{\begin{array}{l}  \mathbf{while}\ n \neq 0 \ \mathbf{do} \\
\quad \mathbf{if}\  nieparzyste(n) \ \mathbf{then}\  n:=3n+1 \  \mathbf{else}\ n:=n/2\  \mathbf{fi} \\
\mathbf{od} \end{array}\right\} (n=1) </math>
<br />
Można też rozważać inne formuły, np, <br/>
,<math>\qquad \xi:\,\bigcup \left\{K:\,\begin{array}{l}  \mathbf{if}\ n \neq 0 \ \mathbf{then} \\
\quad \mathbf{if}\  nieparzyste(n) \ \mathbf{then}\  n:=3n+1 \  \mathbf{else}\ n:=n/2\  \mathbf{fi} \\
\mathbf{fi} \end{array}\right\} (n=1) </math>  <br/>
{co się czyta: ''istnieje taka iteracja ,<math>K^i</math> programu <math>K</math>, że po  wykonaniu  <math>K^i</math>  zachodzi równość'' <math>n=1</math>  .} <br/>
Druga część zadania jest znacznie trudniejsza: nalezy przeprowadzić dowód formuły stopu posiłkując się aksjomatami rachunku programów i aksjomatami algorytmicznej teorii liczb naturalnych.<br/>

<br />
==Elementary theory od addition of natural numbers  and its models==
Poprzednia obserwacja stwierdzająca, że w tej teorii nie można przeprowadzić dowodu tezy Collatza pozostaje w mocy. Jednak, w dalszych rozważaniach pomocne będą własności niestandardowego modelu tej teorii a także parę twierdzeń tej teorii.<br />
<br />
Teoria ta jest wyznaczona przez podanie trzech składników: języka, logiki czyli operacji konsekencji oraz aksjomatów specyficznych dla tej teorii. <br />
'''Język.''' Wyrażenia języka zbudowane są z następujących symboli: symbole zmiennych np. x,y,n, symbou  + dwuargumentoweji operacji, symbolu = dwuargumentowej relacji, symboli 0,1 stałych i symboli funktorów logicznych oraz symboli pomocniczych np. nawiasy<br />
.
Przykładami wyrażeń są ...<br />

'''Logika.''' Operacja konsekwencji (wnioskowania) jest wyznaczona przez podanie aksjomatów logiki pierwszego rzędu i reguł wnioskowania. <br />
'''Aksjomaty.'''


Nonstandard model of Presburger arithmetic was invented by Stanisław Jaśkowski in 1929.

[[Plik:MonStandardModel.png|center|thumb|600px|Nonstandard model of Presburger arithmetic]]
The universe of the model is a subset of the set of complex numbers <math>a+\imath b</math> 
where  <math>a \in \mathbb{Z} </math> i.e. a is an integer number and <math>b \in \mathbb{Q}^+ </math> is a positive rational number. Additionally, whenever <math>b=0 </math> we have <math>a>0</math>.
Addition is defined as  usual addition of complex numbers.

==Algorithmic theory of natural numbers ==
* Język.  Alfabet języka zawiera zbiór zmiennych, np. x,y. funktor + dwiargumentowego działania dodawania, dwie stałe 0 i 1, znak relacji = równości.<br />
Termy (tj. wyrażenia nazwowe: jest to najmniejszy zbiór wyrażeeń zawierający zmienne, stałe i zamknięty ze wzgledu na lączenie dwu termów w ten sposób (t1 + t2).<br />
Formuły. 
* Logika. Rachunek programów.  Rachunek programów zawiera w sobie logikę pierwszego rzędu. Język rachunku programów oprócz formuł pierwszego rzędu zaiera formuły algorytmiczne. Najprostsza taka formuła to napis składający się z programu i następującej po nim formuły (zwykle formuły pierwszego rzędu).
Do aksjomatów logiki pierszego rzędu należy dodać aksjomaty opisujące własności spójników programotwórczych, zob. [[Logika algorytmiczna]].
Do reguł wnioskowania logiki pierwszego rzędu należy dodać reguły specyficzne dla rachunku programów. <br />

* Aksjomaty teorii. <br />
Tylko trzy formuły. <br />
<math>   
\begin{eqnarray}
 \tag{ATN1} \forall_x\, x+1 \neq 0 &&\\
 \tag{ATN2} \forall_{x,y}\,x+1=y+1 \implies x=y  &&\\
 \tag{ATN3}\forall_x\, \{y :=0; \mathbf{while}\ y\neq x\ \mathbf{do}\ y:=y+1\ \mathbf{od} \}\,(y=x) &&
\end{eqnarray}   </math><br />

Są to właściwie aksjomaty teorii następnika.<br/>
Formuła ATN1 stwierdza, że 0 nie jest następnikiem żadnej liczby naturalnej. <br/>
Formuła ATN2 stwierdza, że następnik jest funkcją róznowartosciową. <br/>
Formuła ATN3 stwierdza, że każda liczba naturalna jest ''osiągalna'' z zera przez dodanie skończonej liczby jedynek.<br/>
W tej teorii można napisać definicje działań dodawania, mnożenia i każdej funkcji obliczalnej.

==Analiza formuły stopu==
xxx

==Triples ==
Spostrzeżenie (wynikłe z przygladania się formule stopu).<br />

<math>\forall_{n \neq 0} \exists_{x,y,z}\ n \cdot 3^x+y=2^z  </math>

==  Collatz tree==
xxx
==Własności obliczeń na trójkach==

== Archive ==
[https://dx.doi.org/10.2139/ssrn.4158238 \On Collatz theorem II.pdf wersja z 5 czerwca 2022 ]

][http://lem12.uksw.edu.pl/images/a/ab/On-Collatz-thm17-09-21.pdf wersja z 20 wrzesnia 2021]

[http://lem12.uksw.edu.pl/images/7/7d/Algorytmy-bliskie-Collatzowi.pdf  algorytmy wokół Collatzowe]

[http://lem12.uksw.edu.pl/images/c/c0/On-Collatz-thm-27-09-21.pdf  wersja z 27 wrzesnia 2021]

[http://lem12.uksw.edu.pl/images/8/8f/On-Collatz-thm-7-10-21.pdf   wersja z 7 pażdziernika 2021]