I was reading this answer that no free ultrafilter can be exhibited on the natural numbers.
I have as a theorem that if the Collatz conjecture is true then the following is a free ultrafilter on the natural numbers:
Let $f(x)=(3x+2^{\nu_2(x)})/2$
where $2^{\nu_2(x)}$ indicates the highest power of $2$ that divides $x$ while still giving an integer quotient so for example $2^{\nu_2(24)}=8$.
Let $f^n(x)$ indicate the $n^{th}$ iterate of $f(x)$
Let $F_y$ be the filter at $y$ and be defined as the set of integers $x$ such that there is some $n\in\Bbb N$ such that $f^n(x)=y$, ordered by $n$. So for example $3\preceq5\preceq8\preceq16\ldots$
Then it is a theorem that if the Collatz conjecture is true, the set of all subsets of $N$ with the order inherited from $F_y:y\in\Bbb N$ is a free ultrafilter on $\Bbb N$.
I'm using this definition of free ultrafilter. Is it compatible with the one in use in Noah's answer?
Question
It appears to me that I have explicitly exhibited a free ultrafilter on $\Bbb N$ (modulo the small matter of a proof of the Collatz conjecture), yet such a thing can not be explicitly exhibited. What implications does this have for a proof of the Collatz conjecture? Does it mean nothing more than; such a proof will necessarily require the axiom of choice? Does it mean the proof cannot be explicitly exhibited?
I was curious a good long while ago about the possibility some apparently hard theorems could be unprovable or equivalent to the Godel sentence of a system. This reminds me of that hypothesis. Certainly the Collatz conjecture is "an arithmetical statement which claims that no number exists with a particular property", and therefore among the candidates for a Godel sentence.
Is it possible that this proves no arithmetical statement expressible in Peano arithmetic can disprove the Collatz conjecture, and therefore that the conjecture is true?
The claim that the proof of the Collatz conjecture would imply the existence of a free ultrafilter would establish that the Collatz conjecture cannot be proved in ZF. This is because ZF does not prove the existence of a free ultrafilter. Similarly, ZF+ACC does not prove the existence of a free ultrafilter, and therefore (if your claim is correct) would not be able to prove the Collatz conjecture, either (here ACC is the axiom of countable choice). Even the stronger system ZF+ADC cannot prove the existence of a free ultrafilter and therefore would be unable to prove Collatz (here ADC is the axiom of dependent choice). One would need a stronger version of the axiom of choice, such as for example the axiom of choice for families indexed by the continuum, if one is to have any hope of establishing Collatz. Of course, as mentioned in the comments it is not known whether even the full ZFC would prove it. I notice that there is some doubt in the comments whether your $F_y$ can be used to get an ultrafilter (without using choice), which I haven't checked, so my remarks are contingent on the possibility of doing so, which needs to be established.