Waiting for Gödel

the theorem proved, using mathematics, that mathematics could not prove all of mathematics. Of course, it has a proper and technically precise formulation, but the late logician Verena Huber-Dyson paraphrased it for me as follows: “There is more to truth than can be caught by proof.” Or, as the British novelist Zia Haider Rahman put it in his award-winning début, “In the Light of What We Know,” “Within any given system, there are claims which are true but which cannot be proven to be true.”

.. Famously, Gödel informed the judge at his U.S. citizenship hearing about an inconsistency that he had discovered in the Constitution, which would allow a dictator to rise in America.

.. included a computer scientist obsessed with recursion (that is, self-referential things, like Russian nesting dolls or Escher’s drawing of a hand drawing a hand);

.. In the nineteenth century, the German mathematician Georg Cantor launched an investigation into various sizes of infinities, thereby inventing set theory, which became an overarching paradigm for mathematics. “A set is a Many that allows itself to be thought of as a One,” Cantor said. But, from nearby realms of logic, paradoxes emerged, such as the Russell set, the set of all sets that do not contain themselves.

.. For any consistent axiomatic formal system that can express facts about basic arithmetic:

1) There are true statements that are unprovable within the system.

2) The system’s consistency cannot be proven within the system.

.. “Gödel’s theorem has a major impact on what all computer scientists do,” he told me. “It puts a fundamental limit on questions we can answer with computers. It tells us to go for approximation—more approximate solutions, which find many right answers, but not all right answers. That’s a positive, because it constrains me from trying to do stupid things, trying to do impossible things.”