SIAM Lecture: How Paradoxes Shape Mathematics and Give Us Self-Verifying Computer Programs

Abstract:

A paradox is a seeming contradiction. The liar’s paradox is one of the best known: “This statement is a false.” If the statement is true, then it is false; if it is false, then it is true.

Paradoxes can be so amusing that we might think that paradoxes are nothing more than a game. However, paradoxes triggered a crisis in math a century ago when a paradox similar to the barber paradox was found: 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.

Other clever paradoxes show us the disturbing limits of computation and mathematics. These results are mathematical bombshells.

Today, we design computer programs that check that other computers programs have no bugs. Can computer programs be fed into themselves to check their own correctness? Or does paradox stop us in our tracks? And can we know that beneficial artificial intelligence will not turn evil when it starts to modify its own computer code?