Can ‘concrete’ statements be undecidable?
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.
3
u/Equivalent-Costumes 5d ago
There exists an explicit family of Diophantine equation in integers in which there are no algorithms to correctly identify which one has solutions. This is very concrete.
Because there are no algorithms to decide that, it's also undecidable in the logical sense: given any "reasonable" axiomatic system, there are always an equation in the family which you cannot prove nor disprove that it has a solution; and since if there were a solution you would had been able to prove that, what really happen here is that there are no solutions but you cannot prove that there are no solutions with the current system. This remains the case even if you don't have a fixed system of axioms, but an algorithmic scheme to add axioms as needed.
In fact, there is a way to make this even more concrete. Lob's theorem said that (under every Godelian system, such as even a very weak version of Peano arithmetic without induction) the very fact that proof implies truth is itself should be expected to be unprovable except for known vacuous case; more specifically, given a statement T, a combinatorial object describe statement T as part of a proof system, then given any proof that the existence of the combinatorial object describing the proof of T (from the same axioms) implies T is true, you can modify that proof to get a proof of T itself. You can apply this theorem to a contradictory T like 1=0 to immediately get something unprovable, unless the system itself can prove 1=0, ie. it is inconsistent.
But this can be made even more concrete than that. Under extension of PA we actually have a wonderful scheme to produce such kind of statement. Let's start with PA itself. Let P(n) be the statement that "omega tetration n is an ordinal", more specifically, what the statement really say is that certain type of trees up to height n, under certain specific ordering, is "algorithmically" well-ordered (there are no algorithms to produce a strictly decreasing sequence) - in fact this is actually well-ordered but the concept of well-ordering cannot be stated in PA itself. Then we know the following: we can prove P(0) (in fact this is essentially just the induction axiom), and we have an algorithm that given any proof of P(n) the algorithm produce the proof of P(n+1), and we also has a proof that this algorithm always work. That sounds like we should be able to prove that "for all n, P(n) is true", right? No, we actually can't. In fact, you can prove that "for all n, there exists a proof of P(n)", but that cannot be lifted to show that "for all n, P(n) is true".
Lob's theorem showed that this gap cannot be closed, ever. If you add in axioms that works for individual kind of statement, you can produce more complicated statement where this gap exist. On the other hand, if you attempt to make a general axiom applicable to all T to close off this gap, your system will necessarily have a contradiction.
However, an exercise in attempting to close this gap reveal exactly where the problem lies. Note that in Lob's theorem, the axioms used by the combinatorial proof system must be exactly the same as your actual axioms. If you attempt to fix the gap by adding in as axiom "well, if there exists a proof of T using this axioms, then T is true", then your new system of axioms is no longer the same as the axiom in that statement. This means that you must somehow, in your new axioms, being able to talk about the system of axiom after this new axiom had been added. This is - not surprisingly - a form of self-reference, which should immediately raise a lot of red flags.
And if you think about it, this kind of self-reference existed in ZF itself. ZF lets you define a set P(X) containing all subsets of a set X, while simultaneously let you define a subset of X (hence an element of P(X)) using P(X) itself. Believing that ZF is consistent is believing that this kind of self-reference is safe.
If self-reference is so inherently problematic, why not avoid it altogether? Because being able to declare that certain self-reference is safe is a very strong ontological statement about the nature of finite number itself. Let's think about the example above with the trees. In PA, it is consistent that there exists some n such that simultaneously, there is a proof (more specifically a combinatorial object describing a proof) that "there are no algorithms that produce a strictly descending chain of tree from height n" and also there is an algorithm that does produce such a strictly descending chain of tree. How is this possible? The problem is simple: either the algorithm itself, or the proof, is "fake", it does not correspond to an actual proof or an actual algorithm. But...you cannot write down any actual such n, because we have an algorithm to produce the proof for each particular n. In fact, for each particular number that you can write down, you can prove that such n must be strictly bigger than that number. So what is happening here is that PA is not strong enough to eliminate the possibility that there are some "finite number" that you cannot write down at all. The existence of such a finite number implies that certain form of self-reference is not safe aka. an algorithm runs forever. Conversely, by declaring that certain self-reference is safe, what you are really describing is that certain algorithm which looks really fishy with its self-reference, actually always halt. And the reason you believe it will halt is because you cannot imagine it running forever on any actual number you can write down.
This is the crux of the issue. You want to be able to declare certain self-reference to be safe, because you believe it is true for actual finite number you can write down, because you want your axioms about finite number to have any many true property about the actual finite numbers as possible. But as things become more and more complicated, these self-reference started to look more and more fishy, and one has to wonder where things stopped being intuitively should be true.
And this ties back to the Diophantine example. There are always Diophantine equation whose solution does not exist amongst the one you can write down because it breaks some forms of safe self-reference.
So to answer your question, yes, very concrete statement can be undecidable. It's not a property of non-constructive math at all.
In fact, it's actually possible to produce CH maybe-counterexample very concretely. Take the union of all countable von Neumann ordinal. By construction, it is always of cardinality Aleph_1 . If CH is true, there is secretly a bijection between this set and the real, even if you cannot construct it; if CH is false this is a counterexample.
So, what keeps people hoping that what they are working on isn't one of those case? Probably the fact that we are still very far from any sorts of self-reference that we would consider questionable. Of course, there are always skeptics: there are plenty of people who think that even second-order Peano's arithmetic is already too much self-referential. But for most ordinary mathematician, the kind of questionable self-reference seems extremely far away. For example, if you work in higher category theory, it's not uncommon to run into statements that cannot be proved within ZF, yet seems intuitively should be true; for example if you want to prove that certain algebraic operation always work on categories, you want to be able to talk about category of category, but wait, many categories are already proper classes, so this is something that contains proper classes which is illegal! If you care about ZF, you juggle around this U-small machinery, which seems cumbersome; naturally at some points people (such as Godel) are like "nope, let's just have a big enough universe so that we don't have to do this U thing", and bam, you got yourself Mahlo's cardinal. There is some sense the idea that there are still a lot more self-reference we can intuitively accept to be safe.
(...to be continued)