By Thomas Hales
Thomas Hales, University of Pittsburgh.
The following is a short introduction to the I. E. Block Community Lecture, to be presented at the upcoming 2018 SIAM Annual Meeting (AN18) in Portland, Ore., from July 9-13. Look for feature articles by other AN18 invited speakers introducing the topics of their talks in future issues.
A paradox is a seeming contradiction, and the liar’s paradox is among the best-known. “This statement is false” — the statement is true exactly when it is false. A paradox is often self-referential, making a statement about itself.
Paradoxes can be so amusing that we might be tempted to believe they are nothing more than a game. However, they became a serious business more than a century ago, through a paradox similar to the barber paradox: a barber named Bertie shaves exactly those who do not shave themselves. Does Bertie shave himself? If he does, then he doesn’t; if he doesn’t, then he does. This paradox triggered a deep crisis in the foundations of mathematics. Bertrand Russell and Alfred North Whitehead spent years rebuilding mathematics from the ground up; after a decade of effort, they finally produced a paradox-free proof that \(1+1=2\).
Drawing Hands, a lithograph by M.C. Escher, is an example of a paradox. Thomas Hales will explore the relation between paradoxes and mathematics at the 2018 SIAM Annual Meeting. Public domain image.
Other clever paradoxes expose the disturbing limits of computation and mathematics. Researchers such as Alan Turing and Kurt Gödel discovered these mathematical bombshells.
To avoid paradox, most current mathematicians work within restrictive systems that banish self-reference. Rebelling against these restrictions, some have avoided paradox in mathematics by placing the entire mathematical universe inside a “nutshell” that sits within a still larger universe, and then continuing with an ever increasing expanse of universes, each a nutshell in the next.
Today, we design computer programs that verify the lack of bugs in other computer programs. Can computer programs be fed into themselves to verify their own correctness? Or does paradox stop us in our tracks? One approach to self-verification is the design of computer languages that avoid paradox through nutshell universes. Other ideas for program self-verification come from the century-old proof that \(1+1=2\).
Researchers in artificial intelligence are carrying paradoxes into new realms. Can beneficial artificial intelligence turn malevolent when it starts modifying its own computer code?
In my talk at the 2018 SIAM Annual Meeting, I will present some of my favorite paradoxes and explain how they play into self-verifying computer programs.
 |
Thomas Hales is the Andrew Mellon Professor of Mathematics at the University of Pittsburgh. |