# Strong AI vs Gödel's Theorem?

If Gödel's Theorem is true, it means that for every formal system, there is a thesis that is true but can't be proven from the formal system. Every agent system which humans can build by modern computer is a formal system. That means that there are some truths in the causal world which can't be verified by the agent. But if the human mind is also a formal system under formal rules, the truth that can't be verified by the machine agent also can't be verified by humans. Then the above truth can only be appreciated by God.

Someone will argue that humans aren't formal systems for they have creativity, imagination, can create new axioms. But that just means that creativity and imagination can't be formalized at all. So I infer that Strong AI is impossible because the human mind has some mysterious faculty beyond the formal system.

As a programmer, I would be happy if Strong AI were realizable. So should I discard Gödel's theorem?

• So should I discard the Godel theorem? - Actually you can do whatever you want. May 20, 2013 at 10:22
• `Humans create AI`... may be, may be not. we don't even have evidence of an intelligent creator of humans themselves.
– user2411
May 20, 2013 at 13:30
• As a computer scientist myself, I'm not quite sure if the conclusions you're mixing together are that straightforward. I don't think it's impossible to create strong AI, but we don't know yet, and it's hard to know if we'll know some day - i.e. the zombie problem. Godel theorem, AFAIK, is rigorous. Strong AI possibility is speculative. You seem to assume the second and from that want to discard the first. May 20, 2013 at 13:51
• @Koeng Just as I mentioned here. May 21, 2013 at 7:27
• Gödel's Theorems establish important principal limitations of proof systems. Why do you think an intelligent program needs to be able to proof everything? Humans don't do that either. May 22, 2013 at 20:43

This kind of misguided/soft/wrong/vague reasoning about Gödel's theorem is an example of what Franzen had in mind with his criticisms in the book Gödel's Theorem: An Incomplete Guide to Its Use and Abuse. See also Feferman's criticism of Penrose's similar arguments involving Gödel's theorem.

I don't think strong AI is possible.

Godels theorem applies to formal systems. It remains to prove or at least persuade that minds are formal systems. I doubt it - it's confusing a model with the thing being modelled. In the same way a video of a tornado isn't the tornado.

I don't think that Godel was the first person to bring up the difference between proof and truth. But he did mathematise it.

• Would it suffice to prove that a mind can be simulated in a formal system? In that case, a mind could do nothing a formal system couldn't. May 24, 2013 at 3:25

There is no reason that Human can't create machines as powerful as themselves. They don't have to be formal systems at all. Only limitation in this case is that, once such machines are built, and if they become as powerfull as us, they will never be able to tell us in a formal way how they do it ("creativity", "imagination" etc). This also means, one (a human being) will not be able to "reverse-engineer" them to see how a human-like machine operates proving theorems or doing math and logic even better than humans.

It seems that Godel's Theorems are not closing doors for consturcting such machines but are just preventing us from reverse-engineering their code(i.e., formally describe their internals when they do imagination). We may ask, if reverse-engineerig will not be possible, how they are going to be constructed. Evolution, hybrid-computing (a combination of biological, solid-state, and quantum computing) would allow such a machine.

• The answer is very interesting. you just said Human can't duplicate mind by digital computer, but can build it by evolution and biology. As a programmer, I can't agree you. May 20, 2013 at 6:33
• No, actually he said: Evolution, hybrid-computing (a combination of biological, solid-state, and quantum computing) would allow such a machine. - Which is different from: can build it by evolution and biology. May 20, 2013 at 10:13
• @mami Could you cite your sources for such statements? I don't know about GT but I've read the preface of: Gödel's Theorem: An Incomplete Guide to It's Use and Abuse. The author says: No mathematical theorem has aroused as much interest among nonmathematicians as Gödel's Incompleteness Theorem[...] Many references to the incompleteness theorem outside the field of formal logic are rather obviously nonsensical and appear to be based on gross misunderstandings or some process of free association. May 20, 2013 at 10:33
• @GustavoBandeira you may search using the following key-words and you will see reasonable alternatives, extensions or paradigms for computation beside the Turing-Machine based ones (i.e. formal systems): biocomputation, natural computation, real-number/continous computation etc. If you like to read a popular-science book on the matter (at least partly), "The Emperor's New Mind" would be for you.
– mami
May 20, 2013 at 21:19
• @mami Are you aware that some of the ideas on that book are deeply controversial? May 21, 2013 at 5:09

His theorem applies to the way the mind works as well. The consistency issue is not relevant with human thought, though it is often offered as a final desperate measure, to avoid Godel's obvious implication on the limitations of logic. Whenever the mind contains a complex set of axioms (related to , for example, the faculty of logic or math), then there are proofs within them that are only derivable through a different set of axioms.