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/djao]

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/djao → u/cuervamellori]

If there is a nontrivial Collatz loop in the standard natural numbers, then this loop would render Collatz decidable, in all models of the natural numbers. That is all I claim, and that is all I care about.

[u/cuervamellori → u/djao]

That's fine, but then in that sense, the word "decideable" (in the sense of "this statement is undecideable in ____") no longer has a meaningful definition - it becomes trivial.

[u/djao → u/cuervamellori]

Ok, let me be more concrete. If a nontrivial Collatz loop exists in the standard natural numbers, then Collatz is decidable in ZFC. This usage of the word decidable is meaningful.

[u/cuervamellori → u/djao]

Oh, I see. Yes, of course.

[u/GoldenMuscleGod → u/cuervamellori]

Whenever any mathematician says “there is no non-trivial Collatz loop” absent special context to suggest a nonstandard meaning they either mean there isn’t one in the standard model, or they are miscommunicating, or they are confused.

In your case your comments seem to reflect a confusion about the distinction between syntax and semantics. It is a type of confusion that commonly arises when someone learns just enough model theory to somewhat understand it but not really get the full picture. This results from a lot of emphasis on the syntax side and not enough on the semantics side.

The easiest way to fix the misunderstanding is to be scrupulous about observing the social convention that we imagine everything we say is being formalized in ZFC - do not think when you speak meta mathematically you are justified saying things ZFC does not prove.

In particular, ZFC can prove that every Goodstein sequence terminates if and only if every Goodstein sequence terminates in the standard model of PA. Why? Because if you examine definitions you’ll see that’s just repeating yourself. That you can find nonstandard models of PA that have things that they regard as nonterminating Goodstein sequences does not mean that there are nonterminating Goodstein sequences. Nonstandard models of PA are not the natural numbers. Goodstein sequences are sequences of natural numbers. We have a definition in ZFC of what a natural number is and it does not even mention PA, so why should we care about other models of that theory?