What are some implications of Gödel's theorems on AI research?

Question

Note: My experience with Gödel's theorem is quite limited: I have read Gödel Escher Bach; skimmed the 1st half of Introduction to Godel's Theorem (by Peter Smith); and some random stuff here and there on the internet. That is, I only have a vague high level understanding of the theory.

In my humble opinion, Gödel's incompleteness theorem (and its many related Theorems, such as the Halting problem, and Löbs Theorem) are among the most important theoretical discoveries.

However, its a bit disappointing to observe that there aren't that many (at least to my knowledge) theoretical applications of the theorems, probably in part due to 1. the obtuse nature of the proof 2. the strong philosophical implications people aren't willing to easily commit towards.

Despite that, there are still some attempts to apply the theorems in a philosophy of mind / AI context. Off the top of my head:

• The Lucas-Penrose Argument: which argues that the mind is not implemented on a formal system (as in computer). (Not a very rigour proof however)

• Apparently, some of the research at MIRI uses Löbs Thereom, though the only example I know of is Löbian agent cooperation.

These are all really cool, but are there some more examples? Especially ones that are actually seriously considered by the academic community.

See also What are the philosophical implications of Gödel's First Incompleteness Theorem?

Answer 1

Definitely there are a lot of implications for AI, including:

1. Inference with first-order-logic is semi-decidable. This is a big disappointment for all the folks that wanted to use logic as a primary AI tool.

2. Basic equivalence of two first-order logic statements is undecidable, which has implications for knowledge-based systems and databases. For example, optimisation of database queries is an undecidable problem because of this.

3. Equivalence of two context-free grammars is undecidable, which is a problem for formal linguistic approach toward language processing

4. When doing planning in AI, just finding a feasible plan is undecidable for some planning languages that are needed in practice.

5. When doing automatic program generation - we are faced with a bunch of decidability results, since any reasonable programming language is as powerful as a Turing machine.

6. Finally, all non-trivial questions about an expressive computing paradigm, such as Perti nets or cellular automata, are undecidable.

Answer 2

I found this paper by mathematician and philosopher Solomon Feferman on Gödel's 1951 Gibbs lecture on certain philosophical consequences of the incompleteness theorems, while reading the following Wikipedia article

Philosophy of artificial intelligence,

whose abstract gives us (as expected) a high-level idea of what's discussed in the same:

This is a critical analysis of the first part of Gödel's 1951 Gibbs lecture on certain philosophical consequences of the incompleteness theorems.

Gödel's discussion is framed in terms of a distinction between objective mathematics and subjective mathematics, according to which the former consists of the truths of mathematics in an absolute sense, and the latter consists of all humanly demonstrable truths.

The question is whether these coincide; if they do, no formal axiomatic system (or Turing machine) can comprehend the mathematizing potentialities of human thought, and, if not, there are absolutely unsolvable mathematical problems of diophantine form.

Either ... the human mind ... infinitely surpasses the powers of any finite machine, or else there exist absolutely unsolvable diophantine problems.

which may be of interest, at least philosophically, to the research in AI. I'm afraid this paper may be similar to the article you're linking to regarding Lucas and Penrose philosophical "attempts" or arguments.

Answer 3

I've written an extensive article on this some twenty years ago, which was published in Engineering Applications of Artificial Intelligence 12 (1999) 655-659. It's fairly technical and you can read it in full on my personal website, but here's the conclusion:

In the above it was shown that there are infinitely many proof constructions to Gödel’s theorem – in contrast to the single one that was used in discussions on artificial intelligence so far. Though all constructions that have been actually disclosed can be imitated by a computer, it is evident that there are constructions that have not been disclosed yet. Our analysis has shown that there might exist constructions that might only be discovered by a human. This is a small and definitely unprovable ‘maybe’ that depends on the limits of human imagination.

Hence, people arguing for the mathematical equivalence of humans and machines must ultimately rely on their belief in a limited mind, which implies that their conclusion is contained in their assumption. On the other hand, people advocating the superiority of humans must assume this superiority in their mathematical arguments, ultimately only deriving the conclusion that was already present in their system of reasoning from the very start.

So, it is not possible to produce (meta)mathematically sound arguments concerning the relation between the human mind and the Turing Machine without making an assumption on the human mind that is at the same time the conclusion of the argument. Therefore, the matter is undecidable.

Disclaimer: I have left academia since, so I do not know of contemporary thinking.