I don't fully understand this other question, but there's a clear relationship between logic and number theory


[the strength of saying "each sentence of true arithmetic has a recursive proof"](https://mathoverflow.net/questions/264201/the-strength-of-saying-each-sentence-of-true-arithmetic-has-a-recursive-proof)


Here's a statement: **every integer $n \in \mathbb{Z}\backslash\{0\}$ has a unique prime factorization** which could be thought of as defining a tree structure on the integers.


For a theoretical computer scientist this is just like any other tree, which can be iterated through or breadth-first search or DFS, etc. The fact that the nodes are integers is almost immaterial.


All I know is that certain number theory statements could be be proven with first order logic and others with second order logic, but I doubt anyone details which logic structures were actually used.


Even more basic, does the Euclidean algorithm define a recursive structure on pairs of integers or sequence of integers?



what ordinals were used in proving unique factorization over $\mathbb{Z}$
Let me first address the specific issue of how statements in number theory correspond to recursive "infinitary tree proofs."


Well, first of all, the point is that *every* true statement about natural numbers has a recursive proof. So asking *whether* something like the (statement of the effectiveness of the) Euclidean algorithm has a recursive proof, will always receive the answer "yes." Here's an example of a recursive proof of the Euclidean algorithm's correctness and termination:


* For each specific natural number $n$, we can prove using PA that the Euclidean algorithm "works" on $n$ (or that $n=0$). Moreover, we may effectively find the *first* proof (in some reasonable indexing) of this fact, $\pi\_n$.
* The function $f$ taking $n$ to $\pi\_n$ - "search until you find a proof that EA works for $n$" - is recursive; and so constitutes a "level-one" recursive proof. That is, we only need one use of the recursive $\omega$-rule.
* The overall structure of this proof is a tree: it has a root, branching $\omega$-many times, and at each branch we have a usual first-order proof. (Note that this tree really doesn't come from the details of the algorithm at all, just the fact that PA can prove each specific instance of it working; the complexity of the algorithm is not necessarily related to the complexity of the recursive proof.)


Note that indeed, this picture applies to *any true $\Pi^0\_1$ sentence* (in particular, it works regardless of whether that sentence is provable in PA alone). More complicated statements require more uses of the recursive $\omega$-rule, leading to more complicated trees of rank up to $\omega^2$ (I believe that bound is sharp).


EDIT: By a small tweak, we can in fact show that any true $\Sigma^0\_3$ sentence $\exists x\forall y\exists z\varphi(x, y, z)$ (with $\varphi$ having only bounded quantifiers) has a recursive proof of height 1, as follows:


* Begin the proof by guessing correctly the right value of $x$. We don't have a good way of knowing what $x$ should be, but this is just one bit of information - so "coding it in" to the recursive proof doesn't break anything. (This is exactly analogous to how the set $\{x:$ the Riemann hypothesis is true and $x=0\}$ is computable, even though we don't know if it is $\emptyset$ or $\{0\}$.)
* Now, consider a function $f$ which - on a given $y$ - searches for some $z$ such that $\varphi(x, y, z)$ holds together with a proof ("certificate") of this fact. Since such a $z$ always exists, and whether $\varphi(x, y, z)$ holds can be effectively tested since $\varphi$ has only bounded quantifiers, a proof that such a $z$ works also exists, and moreover the function $f$ can be taken to be recursive.
* But then this $f$ (basically) constitutes a recursive proof.


So it's at the $\Pi^0\_3$ level that things first can become interesting - the idea being that we somehow need to "guess correctly" at the existential quantifier in the middle not once but *infinitely many* times, one for each possible value of the outermost "$\forall$;" so the "guess $x$ correctly" trick above doesn't work. Moreover, *telling* whether a given guess works is a $\Pi^0\_1$ (noneffective, that is) question, so even if by luck we happen to have guessed the right witness, we can't obviously *verify* its correctness, and that's necessary for a recursive proof.


So this is the subtlety of the Shoenfield completeness theorme: the naive idea of just "bootstrapping" up the $\Pi^0\_1$ idea (which *does* work if we replace the recursive $\omega$-rule with the full $\omega$-rule, and then every true sentence has a proof of finite height!) doesn't work, and something more complicated has to be done.




---


Now what do ordinals have to do with all this? Well, the linked question is about the difficulty of proving "Every true statement has a recursive proof," and specifically asks how much transfinite induction is needed to prove this (and the stronger statement that only height $\omega^2$ is needed). Well, in order to formalize transfinite induction principles in PA, we need some way to talk about ordinals (e.g. how do you write "$\epsilon\_0$ is well-founded" in the language of arithmetic alone?), so this is what the "appropriate coding of ordinals" is about. And if you look at [Franzen's paper](http://projecteuclid.org/euclid.bsl/1102022662), you'll see how this shows up in the statement and proof of the result.


This, of course, leaves off an important question: *why* are transfinite induction principles the right metric to use to gauge how hard it is to prove something? This is a general theme in proof theory (and elsewhere), that transfinite induction principles help you prove statements about the existence (or non-existence) of well-founded labelled trees with certain properties; e.g. here it's about the existence of well-founded labelled trees which correspond to recursive proofs, while [in ordinal analysis](https://en.wikipedia.org/wiki/Ordinal_analysis) it's about the nonexistence of finite labelled trees corresponding to proofs of $0=1$ from specific families of axioms.


In particular, the analysis of the Euclidean algorithm case is provable in PA alone (and indeed much less), so no ordinal strength at all is needed to show that that statement has a recursive proof (and indeed, I believe the vast majority of statements in basic number theory will have recursive proofs provably in PA alone, although I'm not an expert here so don't quote me on that).


