Can ‘concrete’ statements be undecidable?

[u/Lehatan]

Let me preface by saying that, while I’m a mathematician, I am not a logician. I’m simply curious about the field. This post is about things that have always bugged me about undecidability.

I’ll take the Collatz conjecture (CC) as an example. Suppose the CC is undecidable in ZFC. Then, if we believe ZFC is consistent, we cannot find a counterexample. If we did, this would contradict it being undecidable. This is strange to me: we would have a statement for which we can’t show its truth while knowing we cannot find a counterexample.

Compare this with the continuum hypothesis (CH), the statement people usually refer to as example of undecidable statement. If we choose it to be true, we know there is a subset S of the real numbers which has cardinality between countable and the continuum. CH being undecidable implies that if we believe ZFC is consistent, we will not stumble into such an S by construction (say with schema specification, etc.). If we did, this would contradict ZFC. But that’s ok, because not every subset of the reals can necessarily be obtained ‘constructively’ through schema specification etc. (I am being informal here, but I believe there is a formal way to say this). So us not being able to produce a counterexample of CH does not mean that one cannot exist.

To me, this seems like a different flavour to CC. There, it seems that any counterexample would be constructive (it’s just a natural number!), and hence, if CC is undecidable, such a counterexample cannot exist.

I informally define ‘concrete’ statements are ones which are about ‘constructive’ objects. Thus any counterexample to a ‘concrete’ statement would be constructive, and hence undecidability of a ‘concrete’ statement would ‘say’ that no such counterexample exists (otherwise we would be able to construct it!).

I am left with the question: should we expect ‘concrete’ statements, such as CC, to be decidable? Maybe there is a formal answer to this question, by formalising what a ‘concrete’ statement is, and showing that such statements are decidable. Though, to me, this seems unlikely to be possible, by Gödel.
Moreover Gödel’s incompleteness theorem holds just under Peano Arithmetic, and so it seems to be saying there is a priori no difference between a statement about the natural numbers such as CC and a statement about cardinalities such as CH. But my intuition cannot help but telling me these are of different nature. Am I wrong to assume this?

A more general version of my question is, why as mathematicians do we expect the questions we are working on to be decidable? We get a sense that a proof or counterexample exists, and it seems that outside of certain ‘non-constructive’ parts of mathematics, we never run into such issues.

[u/SOTGO]

I would avoid relying too heavily on intuition here. Take the Busy Beaver function, from Wikipedia "the n-state busy beaver game consists of finding the longest-running or highest-scoring Turing machine which has n states and eventually halts." By definition the longest running Turing machine of a given size that halts must run for a finite amount of time (or else it would never halt), so the busy beaver function must be finite for any n. But it has been shown that for large enough values of n (I believe at least for n > 748) the value of the busy beaver function is undecidable, even though we know for a fact that it is some finite value.

[u/NewtonsThirdEvilEx → u/SOTGO]

I don't think that helps me. You can physically evolve an n-state Turing machine in time with it's transition function and see if it halts or not after an arbitrary amount of steps. But some don't halt. For small ones, we're able to associate certain Turing machines with certain problems and prove that they don't halt in some cases and sometimes we're able to enumerate them. Not in all though.

But for the Collatz case if we find a non 4-2-1 loop, that is a experimentally testable counterexample.

[u/djao → u/NewtonsThirdEvilEx]

There could conceivably exist Collatz counterexamples that never devolve into a loop, but just continue infinitely without ever looping.

[u/NewtonsThirdEvilEx → u/djao]

Yes, but that's beside my point. Nothing forbidding a nontrivial loop assuming the proof is undecidable. Still a counterexample.

[u/djao → u/NewtonsThirdEvilEx]

Um, actually, yes, if you assume the problem is undecidable, there is something that forbids a nontrivial loop; namely, the existence of a nontrivial loop contradicts the supposed undecidability of the problem.

Suppose there exists a nontrivial loop starting from some value x not equal to 1, 2, or 4. Then, start from x and compute enough terms in the sequence to reach x again. Congratulations! You have decided the Collatz conjecture, contradicting the assumed undecidability of the conjecture.

[u/cuervamellori → u/djao]

Only a nontrivial loop in the standard natural numbers would contradict undecideability, correct? A nontrivial loop in nonstandard numbers would not.

It's possible that collatz is undecideable and nontrivial loops can't exist, but that's stronger statement than saying collatz is undecideable.

[u/djao → u/cuervamellori]

I interpret Collatz to state that no counterexample exists in the standard natural numbers.

[u/cuervamellori → u/djao]

"X is true in this particular model of ZFC" will always be either true or false; it can't be a statement in ZFC and can't be said to independent of ZFC, right?

[u/Kaomet → u/cuervamellori]

Hu ?

You can build an inner model of ZFC in any model of ZFC (forcing). Then ZFC can prove X is true in this inner model / false in that inner model. And this is precisely how CH was proven independant of ZFC (Gödel built a model where CH is true, Cohen built a model in which it is false).

ZFC is the axiomatic theory, by definition true in all models. Independant of ZFC means the axiom does not give enough information to decide a statemeent. As in geometry : you need Euclid fith postulate to rule out elliptic and hyperbolic geometry, so it is independant of the previous postulates.

[u/djao → u/cuervamellori]

Ok, maybe this is why non-logician mathematicians get tired of logicians. When someone asserts the existence of a nontrivial Collatz loop, I am imagining something very concrete: here is a natural number x, here is its decimal expansion, here are all the subsequent terms in its Collatz sequence, each of which one can verify, and here is x repeating itself in this sequence after n terms. If you are imagining some different scenario, then we are not thinking about the same thing. If your language is insufficient to express what I am thinking, then your language is inadequate.

[u/cuervamellori → u/djao]

I'd love to take credit for creating ZF(C), but I'm afraid I can't 😀 it's fine to say "what I care about is if CC has a counterexample in the standard numbers". But if you're saying that, then there's no useful way to use words like "undecideable" in relation to ZF(C), those concepts no longer apply.

Undecideable, independent, etc., all relate to a set of axioms. There is no set of first order axioms that define exactly the standard numbers.

The question of whether a fact (like Goodstein's theorem) is independent of a set of first order axioms or not I think usually should not be that interesting to people who care about whether it's true in a particular model.

[u/djao → u/cuervamellori]

OK, but ZFC or not, I can still perfectly clearly express my intended meaning in other programming languages, for example Rocq:

From Stdlib Require Import Arith Utf8.
Definition collatz (n : nat) : nat := if Nat.even n then n / 2 else 3 * n + 1.
Definition nontrivial_collatz_loop : Type := { x : nat & { n : nat | x ≠ 0 ∧ x ≠ 1 ∧ x ≠ 2 ∧ x ≠ 4 ∧ 0 < n ∧ Nat.iter n collatz x = x } }.

[u/cuervamellori → u/djao]

Presumably, in Roq, "nat" is defined as only taking on values in the standard numbers - in other words, it is operating in a specific model of the natural numbers.

To make things even more concrete, imagine a Turing machine that halts if a nontrivial collatz loop exists. It might be true that there is no standard natural number n such that the Turing machine halts in n steps. If that were true, it would mean that there are no nontrivial loops in the standard natural numbers. This is a statement that is either true or false, even if there is no proof of that statement using the axioms of ZFC.

However, it's possible that if this Turing machine ran for N steps, where N is a number that satisfies the axioms of (let's make things simple) first order Peano Arithmetic, but is not a standard natural number, it could halt. That would imply there are nontrivial loops in some nonstandard model.

[u/NewtonsThirdEvilEx → u/djao]

Okay, then that clears about everything.

[u/BiasedEstimators → u/NewtonsThirdEvilEx]

The set <n, k> is countable infinite. Say n is the number of k is the collatz step.

Enumerate <n, k>. Go through the enumeration calculating collatz(n, k) each time. Terminate when you find a nontrivial loop. This algorithm is guaranteed to terminate in finite time given a nontrivial loop.