Gödel and the mechanization of thought

At the recent Society of Catholic Scientists conference, Peter Koellner gave a lucid presentation on the relevance of Gödel’s incompleteness results to the question of whether thought can be mechanized. Naturally, he had something to say about the Lucas-Penrose argument. I believe that video of the conference talks will be posted online soon, but let me briefly summarize the main themes of Koellner’s talk as I remember them, so that the remarks I want to make about them will be intelligible.

Lucas and Penrose argue that Gödel’s results show that thought cannot be mechanized in the sense of being entirely captured by the algorithmic rules of a Turing machine. It is sometimes supposed that Gödel himself took his Incompleteness results to show this. But as Koellner pointed out, what Gödel actually thought was that the Incompleteness results entail a disjunctive proposition to the effect that either thought cannot be mechanized or there are mathematical truths that outstrip human knowledge. Of course, the disjunction is not exclusive. It could be that both disjuncts are true. The point, though, is that Gödel claimed only that his results show that at least one of them must be true. They don’t by themselves tell us which.

Another way to think about it is as follows. There is (1) the realm of mathematical truth, (2) the realm of human thought, and (3) the realm of matter. Gödel thought his Incompleteness results show either that the first is irreducible to the second or that the second is irreducible to the third (or, again, maybe both). But they don’t show which.

It is important to emphasize that what is at issue here is what can be formally demonstrated. Gödel did think that thought cannot be mechanized, but Koellner’s point is that Gödel did not claim that that could be formally demonstrated. He claimed only that the disjunctive statement could be. Was Gödel right about that much? Koellner thinks so. More precisely and cautiously, he thinks that if we confine ourselves to the question of what we can know by way of mathematical truth, and if we work with what he takes to be a plausible formalization of the notion of knowledge, then Gödel can be said to be correct that his disjunction can be formally demonstrated.

Lucas and Penrose claim that the first disjunct of Gödel’s disjunction (to the effect that human thought cannot be mechanized) can also be demonstrated, but Koellner argues that their attempts to show that fail.

There’s more to Koellner’s presentation that that, but this suffices for present purposes. The issue I want to consider is the idea of a formal demonstration of the proposition that human thought cannot be mechanized. Let us grant for the sake of argument that Lucas and Penrose fail to provide such a thing. The question I want to ask is: If thought cannot be mechanized, should we expect to be able to provide a formal demonstration to that effect?

The whole idea seems fishy to me, though it is difficult to point precisely to the reason why. But blogs exist in part for the purpose of airing inchoate or half-baked ideas, so here goes.

For human thought to be mechanized would entail that it could be entirely captured in a formal system. So to give a formal demonstration that thought cannot be mechanized would entail giving a formal demonstration that thought cannot be entirely captured in a formal system. And of course, it would be a human thinker who would be giving this demonstration. It is the conjunction of these elements – the idea of human thought giving a formal demonstration that not everything about human thought can be captured in a formal demonstration – that seems fishy.

But the way that I’ve just stated it is not precise enough to show that there really is any inconsistency or incoherence here. For there is nothing necessarily suspect about the idea of a formal result having implications about the limits of formal results in general – that is what Gödel’s Incompleteness theorems themselves do, after all. And human thinkers are the ones who discover these implications. So what’s the problem?

The problem would be something like this. If you are going to produce a formal result concerning all human thought, it seems that you would first have to be able to formalize all of human thought, so that you would be able to say something about human thought in general in the language of your formal system. But in the case at hand, that means that you would have to be doing for all of human thought – namely, formalizing it – exactly what your purported formal demonstration is supposed to be showing cannot be done. In other words, a formal demonstration to the effect that human thought cannot be mechanized would presuppose that all human thought can be mechanized. In which case the idea is incoherent.

If this is correct, then if human thought cannot be mechanized, then we should expect that we should not be able to give a formal demonstration that it cannot be.

Notice that this does not mean that we should expect not to be able to give a compelling philosophical argument for the conclusion that thought cannot be mechanized. On the contrary, I think there are compelling philosophical arguments to that effect (for example, Kripke’s argument, which is something I talked about in my own SCS talk). The point is rather that we should expect not to be able to give for this conclusion a formal demonstration of the kind familiar from mathematics and formal logic. The limitation in question concerns only that particular kind of argument.

But again, I’m just spitballing here.

Gödel and the unreality of time

Kripke contra computationalism

Accept no imitations [on the Turing test]

Do machines compute functions?

Can machines beg the question?

From Aristotle to John Searle and Back Again: Formal Causes, Teleology, and Computation in Nature [a 2016 article from the journal Nova et Vetera]