Provability and computability

Question

Is there an algorithm whose correctness is not provable? That is, it works but we are sure that we will never know that it’s correct. I’m basically exploring the difference between computability and provability: does the former imply the latter? What’s the relationship between the two concepts?

On the one hand I think provability is stronger, because there are facts that can be proved but never verified. And if it’s provable, then you can search for the proof in finite time. On the other hand, the existence of unprovable statements is equivalent to the existence of undecidable problems, since both concepts are regarding finiteness.

Answer 1

Is there an algorithm whose correctness is not provable?

Not provable in what system? If you do not specify the formal system, then "provability" is a completely meaningless concept! In any case, given any reasonable system $S$ and any algorithm $A$ that takes an input natural number and that $S$ proves to be correct, we can trivially construct an algorithm $B$ that takes the input $n$ and first checks all proofs over $S$ of length $n$, and if it ever finds a proof over $S$ of "$0=1$" then it purposely does something incorrect, otherwise it does exactly the same as $A$. Then obviously $S$ cannot prove that $B$ is correct, otherwise $S$ would also prove $\text{Con}(S)$.

Answer 2

Yes, it is easy to write programs whose correctness is not provable or disprovable in, say, ZFC (or whatever other computably axiomatized theory you prefer). For instance, let's say that $P$ is a program that solves some problem. Consider the program $P'$ which does the following: on an input of size $n$ it searches for a proof of size at most $n$ that ZFC is not consistent. If it finds such a proof then it gives some garbage as its output. If it doesn't find such a proof then it just does whatever $P$ would do.

Assuming ZFC is consistent, this program will solve the problem correctly. But ZFC can't prove that because then ZFC would prove that ZFC is consistent.

For what it's worth, Adam Yedidia and Scott Aaronson have worked on finding the smallest Turing machine whose behavior is not provable in ZFC. See here for the paper.