By Thomas Hales
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\).
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.