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/GoldenMuscleGod → u/SOTGO]

You have partial understanding but it is incomplete and I think your answer may mislead OP. The value of the busy beaver function is independent of an axiomatizable theory for sufficiently large inputs, where the size depends on the theory. It isn’t undecidable. Undecidable and Independent are not synonyms. It is impossible (in classical math) for any specific proposition to be undecidable - only decision problems can be undecidable. A single proposition can be independent of a theory but there is no such thing as being “independent” in general - it can only be independent of a theory, not of all theories. Independence is a binary relation.

There is a fact about the busy beaver function related to their intuition: there exists exactly one explictly written n for which BB(1000)=n is consistent with, say, ZFC (assuming ZFC is consistent). This is the “true” value of BB(1000). We can consistently add BB(1000)=/=n as an axiom to ZFC, this theory then proves BB(1000)=/=k for any numeral k. In a model of this theory the value of BB(1000) is a nonstandard element, not an alternative standard natural number.

Edit: actually I think to justify that claim I have to assume more than that ZFC is consistent - enough is to assume that an inaccessible cardinal exists.

[u/SOTGO → u/GoldenMuscleGod]

My apologies, I am not an expert in this area. I called it undecidable based on the title of a paper linked from the Wikipedia page, "The Undecidability of BB(748)" (link). Looking back the actual statement on the page is "it is undecidable by a general algorithm whether an arbitrary Turing machine is a busy beaver," which you are correct is different than the claim I made

[u/GoldenMuscleGod → u/SOTGO]

To be fair the terms are sometimes used synonymously even though they shouldn’t be.

To clarify the difference: a decision problem can be thought of as a case where we have a class of questions and we want a “yes” or “no” answer on each of them. It is decidable if there exists an algorithm taking the question as input and outputting the answer. If not it is undecidable. Note that this definition does not mention any theory.

With this definition (in classical math, using the law of the excluded middle) a single question cannot be undecidable: its answer is either “yes” or “no” and so one of the two algorithms “ignore the input and say yes” and “ignore the input and say no” must give the correct answer. Of course this doesn’t help find the answer, which is why the classical notion of decidability can be counterintuitive (this is one area where constructive theories better capture intuition).

A sentence is “independent” of a theory if that theory neither proves it nor its negation. This depends on the theory. No sentence is independent of every theory: consider the theory where we take that sentence as an axiom. Of course this does not help us to determine whether the sentence is true with the meaning we intend for it. This is similar to the decidability issue for single propositions.

The ideas are distinct but related: suppose we have a binary relation where the problem of whether it holds is undecidable. For example, “does BB(n)=m?” Where n and m are variables that must be set for us to have a specific question. Then that means for any sound axiomatizable theory there must be some specific case of it that is independent of the theory (such as “does BB(1000)=[some explicitly written enormous number]?)

However which of these statements is independent of the theory will depend on the theory, and there is no statement that is independent from all sound and axiomatizable theories.

[u/ZookeepergameWest862 → u/GoldenMuscleGod]

there exists exactly one explictly written n for which BB(1000)=n is consistent with, say, ZFC (assuming ZFC is consistent)

While this is true, it's a bit funny, because that one explicitly written n is BB(1000), of the metatheory. So there is one explicitly written n but we cannot explicitly write (or rather can never confirm) because it was conjured out of excluded middle.

[u/GoldenMuscleGod → u/ZookeepergameWest862]

Yes I’m giving a classical account. I think constructive and intuitionistic theories can give useful alternative ways of looking at it, these theories often deal with the issue at a much earlier step: they are either agnostic about or affirmatively reject the idea that the busy beaver function even exists as a function defined on all natural numbers, and as for specific values like BB(1000) they wouldn’t normally actively deny it exists but they will say, essentially “I’ll believe it exists when I see it.”

Whether they ever will “see it” or not depends how strong the constructive theory is.

[u/GoldenMuscleGod → u/ZookeepergameWest862]

Oh and thank you for this reply because thinking about it a little more made me realize I cannot justify that conclusion simply by assuming ZFC is consistent, if I am restricting myself to ZFC: I cannot eliminate the case where ZFC is consistent but proves BB(1000)=/=k for all standard k. Enough is to assume that an inaccessible cardinal exists.

[u/ZookeepergameWest862 → u/GoldenMuscleGod]

Right. It is generally true that there is at most one (you don't even need consistency of ZFC for this), but Cons(ZFC+BB(1000)=n) (this notation is a bit quacky since n is not necessarily a number writable in the metametatheory, but only exists within the meta ZFC) isn't provable from ZFC+Cons(ZFC) because this would mean that ZFC+BB(1000)=n and ZFC are equiconsistent in ZFC, but this can't be the case because ZFC+BB(1000)=n proves ZFC is consistent.

If ZFC is inconsistent (in the meta ZFC) then ZFC+BB(1000)=n can prove anything, including the (internal) consistency of ZFC. If it is consistent, then the Turing machine M checking the consistency of ZFC doesn't halt, the version of M inside ZFC+BB(1000)=n cannot halt since it would take a nonstandard number of steps which is larger than n, contrary to BB(1000)=n and so M does not halt and ZFC is consistent.

I was confused for a while before writing down the proof above, because this it seems that ZFC+BB(1000)=n can prove the consistency of even large cardinals. Like if T is a theory stronger than ZFC, then ZFC+BB(1000)=n (inside T) seems to prove the consistency of T (assuming that T is checkable with a 1000 states Turing machine, which would include pretty much all theories that we care about), violating Gödel if your argument works. It turns out that the possibility that T is inconsistent inside T is an issue. An interesting thing is that if n is standard with respect to the metametatheory, then ZFC+BB(1000)=n inside T does prove the consistency of T. So it seems that there is a philosophical issue with asserting the definiteness of BB(1000) by appealing to standard natural, as being standard itself is not definite but only with respect to a metatheory, and the precise value of BB(1000) can never be found but only be turtled all the way up the metatheories.

[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/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.

[u/GoldenMuscleGod → u/NewtonsThirdEvilEx]

The claim that there is no nontrivial loop is a pi_1 claim (as I described that term in another comment I made replying to you), and so is true if it is independent, however it can be independent of PA, or ZFC (in the sense that pi_1 claims in general can be independent - of course we do not know whether this claim is independent). The claim there is no divergent sequence is pi_2 claim so could be true or false if it is independent (as far as we know).

By the way I think the comment above could be potentially misleading so I will link here my response to it clarifying what I think it misses.

[u/NewtonsThirdEvilEx → u/GoldenMuscleGod]

I do like this more formal argument a lot better. I will read a bit more into it, but thank you!

[u/OmnipotentEntity → u/NewtonsThirdEvilEx]

To add to /u/djao on how Collatz could be independent of ZFC. Let's say we have an orbit that may be infinite, or may just be very, very long, so long that we have no way of concretely simulating it in the universe. However, while analyzing it, we somehow find that this particular orbit belongs to an infinite family of related orbits, such that all such orbits terminate if and only if the continuum hypothesis is true.

Any particular orbit may converge, and we may even be able to demonstrate this for particular orbits, but if we prove all such orbits diverge then we have a proof of the continuum hypothesis.

[u/NewtonsThirdEvilEx → u/OmnipotentEntity]

why are you making this “in our universe”. as a trained physicist, that’s making it far more worse for me lol.

[u/OmnipotentEntity → u/NewtonsThirdEvilEx]

well, you had mentioned "physically evolving" Turing machines, which is why I mentioned that in particular.

[u/lurgi → u/SOTGO]

I can't find a reference to 748, but this is relevant.

[u/SourKangaroo95 → u/lurgi]

In his latest blog post he says the number has been brought down to 335

[u/Foreign_Implement897 → u/SOTGO]

Nice!