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

It's true that there are certain statements that, if they were false, would obviously be provable to be false with an equally obviously computable counterexample. Proof of undecidability can then be interpreted as a proof of the statement (but in the formal system that the proof of undecidability takes place in).

The Riemann hypothesis is such an example. Not in its classical form, but it is equivalent to a statement about integers that has this property.

I'm not sure the same goes for Collatz since a counterexample might grow without bound, and that could be unprovable (I guess).

[u/Lehatan → u/TheBB]

> Proof of undecidability can then be interpreted as a proof of the statement (but in the formal system that the proof of undecidability takes place in).

This is exactly what I’d like to understand. Is this a statement one can make formal?

I see your point that the Collatz conjecture may not be the best example due to unbounded sequences. Instead we can say that undecidability of the Collatz conjecture means we won’t find a non-trivial loop.

[u/GoldenMuscleGod → u/Lehatan]

Here’s a formalized statement: if a sentence is sigma_1 in the arithmetical hierarchy and true then it can be proved by any theory that is sufficiently strong for Gödel’s incompleteness theorems to apply to it, this means if a sigma_1 sentence is independent then it must be false.

In fact this fact is used in the proof of the incompleteness theorems and is one of the most overlooked steps among people who otherwise understand the basic proof strategy. Understanding why you need this for the theorems to work is, I think, arguably the key insight to understand in the proofs

A negation of a sigma_1 sentence is a pi_1 sentence. If a pi_1 sentence is consistent with that type of theory it must be true, if it is false the theory proves it is false.

For intuition, some examples of pi_1 sentences are claims like that a particular Turing machine will never halt when run on empty input, a claim that a particular theory is consistent, or a claim that all natural numbers have a particular algorithmically checkable property.

So examples of sigma_1 claims are that a machine will halt, a theory is inconsistent, or there is a number with a checkable property.

The Collatz conjecture is, on its face, a pi_2 claim. This is like a claim that a particular recursive function is total - that a Turing machine will halt on every input. A pi_2 claim that is independent can be either true or false.