Does Gödel’s theorem preclude the existence of all means of proving all statements in a formal system, or preclude only computable means?

Question

It is necessarily the case that you can eventually generate all possible finite proofs on a UTM. It also necessarily the case that you can eventually generate all possible theorems on a UTM. This follows trivially from the fact that both proofs and theorems are finite collections of characters from some finite alphabet. As a result, it is necessarily the case, that you can generate all proofs, and all theorems, given enough time.

In this view, where we mechanistically generate all theorems and proofs, being able to prove a given theorem is being able to connect the theorem to its proof, since as demonstrated, generating all possible theorems and proofs is trivial, given enough time on a UTM.

At the same time, Gödel’s First Incompleteness Theorem states that it is not as a general matter possible to prove or disprove all statements within a formal system. Therefore, Gödel’s theorem implies that we cannot map every theorem to its proof, since that would be equivalent to being able to prove every theorem in the system, which is forbidden by the theorem.

As a corollary, it must be the case that there is no computable mapping from the set of theorems to their corresponding proofs. If you assume otherwise, then you can prove every theorem in the system using a computable function, which would certainly violate Gödel’s theorem.

Does Gödel’s theorem preclude the existence of any such mapping as a general matter?

Or, does it imply that such any such mapping is not computable?

Another way to think about this is if we have a given theorem, we generate all proofs, until we find the proof for the theorem in question. However, we don't know how long the proof is, even if we're told ex ante that the theorem is in fact true. As a result, mapping a theorem to its proof in this manner is not decidable, if you assume you can't know how long the proof is, ex ante.

The intuition is that a short theorem, could have an extremely long proof. This is arguably the case for the Robertson–Seymour Theorem, which has fairly succinct statements, but an incredibly long and complex proof, that I do not claim to understand.

So if you can't know how long the proof for a given theorem is ex ante, then generating all proofs in this manner is no different than the Halting Problem, since you'll have wait to indefinitely to find the applicable proof. Knowing the theorem is true, is like knowing the UTM will halt, but you still don't know when. If you don't know the theorem is true, then it is exactly the Halting Problem, since you don't even know you'll eventually find a proof.

Taking this to its extreme, we can at least posit the idea of a finite theorem, that requires an infinite proof. This is obviously beyond the realm of human knowledge, since human beings can only write a finite number of symbols over a lifetime. But the point is, if such a theorem exists, it would be unprovable.

Any thoughts on this tertiary point would be welcome as well.

Answer 1

There is a computable map from theorems to proofs of them.

In particular, for each theorem $\phi$, we just go through the list of proofs and once we find one that's a proof of $\phi$, we stop and return that proof. This map is clearly computable, and since any theorem has a proof, is defined on the set of theorems.

The issue, of course, is that it's not clear (i.e. not computable) whether any given sentence $\phi$ is a theorem or not. If $\phi$ is a theorem, we have a means of checking this because we will eventually find a proof using the above algorithm. But if $\phi$ isn't, we would simply keep searching forever: we never arrive at a "no" answer. So Gödel's Theorem really tells us that the set of theorems is $\Sigma^0_1$ (i.e. computably enumerable) but not $\Delta^0_1$ (i.e. computable).

In general, one can show that a set is $\Sigma^0_1$ iff it is the image of a (total) computable function. This gives a "yes" answer to set membership in finite time just by searching for the input that ouputs our desired value. But this doesn't give a "no" answer in a finite amount of time. For the set to be computable, we need both answers in a finite amount of time, i.e. it needs to be $\Sigma^0_1$ and its complement needs to be $\Sigma^0_1$.

Answer 2

First, a minor terminology issue (but one which I think will clarify things): you misuse the word "theorem" in your post. Godel shows that as long as $T$ is an "appropriate" theory (consistent, computably axiomatizable, and capable of interpreting Robinson arithmetic) then there is some sentence in the language of $T$ which $T$ cannot prove. However, the theorems of $T$ are by definition the $T$-provable sentences. So your claim "being able to prove every theorem in the system [is] forbidden by [Godel]" is false - by definition we can prove every theorem in the system, since the theorems are exactly the sentences we can prove in the system.

---

OK, now let's think about computable functions. There are two notions of "computable function" we might consider (restricting attention to unary functions for simplicity):

• A total computable function is a function $f:\mathbb{N}\rightarrow\mathbb{N}$ such that there is some Turing machine $M$ such that for all $x,y$ we have $M(x)\downarrow=y$ iff $f(x)=y$ (here "$\downarrow =$" means "halts and outputs").

• A partial computable function is a function $f:D\rightarrow\mathbb{N}$ for some $D\subseteq\mathbb{N}$ such that there is some Turing machine $M$ such that for all $x, y$ we have $M(x)\downarrow=y$ iff $f(x)=y$. Note that consequently this $M$ will halt only on inputs from $D$.

Although a total computable function is definitely a nicer object than a partial computable funciton, one of the big realizations of basic computability theory is that the class of partial computable functions, rather than the class of total computable functions, is the right class of functions to think about. For example, we can effectively enumerate the partial computable functions in a precise sense (this is basically what a universal Turing machine does), whereas we cannot do the same for the total computable functions (since if we could we could diagonalize against them).

The partial/total issue crops up here as well. A quick corollary of Godel is:

If $T$ is an appropriate theory, then the set of $T$-theorems is not computable.

(If you haven't seen the proof of this, this is a good exercise.) Consequently we have:

Suppose $T$ is appropriate. There is no total computable function $f$ such that for every $\varphi$, if $\varphi$ is (the Godel number of) a $T$-theorem then $f(\varphi)$ is (the Godel number of) a $T$-proof of $\varphi$.

Proof: Suppose we had such an $f$. Given $\varphi$, compute $f(\varphi)$ (we can do this since $f$ is total computable) and check whether that is in fact a $T$-proof of $\varphi$; if it is then $\varphi$ is a $T$-theorem, and if it isn't $\varphi$ isn't a $T$-theorem. $\quad\Box$

However, at the same time we have:

Suppose $T$ is appropriate. Then there is a partial computable function $g$ such that the domain of $g$ is the set of theorems of $T$ and for each $T$-theorem $\varphi$, $g(\varphi)$ is a $T$-proof of $\varphi$.

(Note that this $g$ cannot be extended to a total computable function, since such an extension would contradict the previous point!)

Proof: Brute-force search. Consider a machine $M$ which, on input $\varphi$, starts searching for $T$-proofs of $\varphi$ and halts iff it finds one (and if it does, it outputs it). This $M$ halts on exactly the $T$-theorems, and when fed a $T$-theorem as input it outputs a proof of that $T$-theorem. $\quad\Box$

---

Finally, re: the end of your post, Godel is only about computable objects; it only proves that there is no computable function/set/whatever satisfying such-and-such properties, not that no function/set/whatever at all satisfies those properties.