Undecidability and force-brute checking

Question

Suppose we have a predicate $\forall n P(n)$ with n natural number (e.g. Goldbach's conjecture) and we have proved that is undecible (undecidable proposition for any system of recursive axioms capable of formalizing arithmetic like axiom of choice) so we can't find a proof to show if it is true or false. Now if we use a computer to check P(n) for n in natural number we must not find a k such that P(k) is false otherwise we have a proof that $\forall n P(n)$ is false in contraddiction with the fact we have proved undecidability. But if we can not find a k such that P(k) is false this means that $\forall n P(n)$ is true and we have again a contraddiction with the fact we have proved undecidability. Is my argument right?

Answer 1

There is something to your argument, but it's not quite right. First off, note that it relies on $P$ being computable. Second, more importantly, note that there is no (universally agreed upon) notion of absolute undecidability. We generally talk about undecidability with respect to some fixed formal system. PA seems the natural choice, so let's assume we've proved $\forall n P(n)$ is undecidable in PA.

If so, then we reason that $\forall n P(n)$ must be true, since if it were false there would be a counterexample and surely PA will be able to establish this, so it would not be undecidable after all.

So we have the theorem that if $\forall nP(n)$ is undecidable in PA, then it is true. But this doesn't mean that a proof that $\forall nP(n)$ is undecidable in PA would cause a contradiction. Just because we can prove that it is undecidable in PA doesn't mean that PA can prove that it is undecidable in PA. In fact, assuming PA is consistent, can't prove any statement is undecidable in PA since this would imply PA is consistent and violate Gödel's theorem. So, even if the implication is provable in PA, PA will never be able to prove the premise, and thus can't conclude $\forall n P(n)$. So we don't get a contradiction with the fact that $\forall n P(n)$ is undecidable in PA.

---

I see now that you've added a clarification that you do mean "absolutely undecidable". As alluded to above, that's a problematic notion, but we can still say something useful. If there is some statement of Goldbach type that we prove undecidable in some system, we can always just strengthen the system to include it as an axiom and get a perfectly good system where it is decidable. For example, we can extend PA to PA + Con(PA), which is a perfectly correct system, assuming PA is correct. So in this sense there can't be an "absolutely undecidable" statement of Goldbach type that we can prove is undecidable. But eventually when we get to systems as strong as our metatheory, we can't prove things are undecidable anymore, anyway.

Answer 2

First, a single statement can never be undecidable. Consider the following two routines:

A. When given as input $\forall n \ P(n)$, it will return "True!"

B. When given as input $\forall n \ P(n)$, it will return "False!"

One of these two routines will correctly decide the truth of $\forall n \ P(n)$

Instead, the question you want to ask is: is there a routine that, when given as input any number $n$, correctly decides whether $P(n)$ is true or false?

Second, using a computer to go through all numbers one by one isn't going to work to decide whether $\forall n \ P(n)$ is true or false. Yes, if $P(k)$ is false for some $k$, then eventually the computer will run into that number, and then we know: $\forall n \ P(n)$ is false. However, if $\forall n \ P(n)$ is true, then this computer will run forever .... meaning that there will never be a point in time where the computer has checked all numbers .. and thus there will never be a point at which you can say that the statement is True.