A Really Scary Thought
A scary question, a really scary question
Vincent Price was just featured last Thursday night with a series of his movies, scary horror ones shown on Turner Classic Movies. Price was known for his distinctive voice and special smirk, which was perfect for these movies. The series was in honor of Halloween. October 31 is the day of trick-or-treating, wearing costumes, going door-to-door to get candy, telling scary stories, and watching horror films.
Today Ken and I want to raise a simple fundamental, and scary question.
No it’s not about the world economy, the possibility that my NFL Giants could lose the rest of their games, or any other mundane problem. It’s about the most fundamental question there is:
Is there some substantial logical theory that is consistent?
This might almost sound silly, a joke, or a late Halloween prank, but it is a real question. It is one that I previously never thought about, but I think it is the question to ask in logic. Can we answer it?
Let’s turn and look carefully at what we are asking.
David Hilbert started this all with his famous program to prove by finite methods that mathematics is consistent. This program was turned aside by Kurt Gödel’s proof of his First and Second Incompleteness Theorems. These theorems show, of course, that any formal theory that is strong enough—more on this in a moment—cannot prove its own consistency. More precisely if proves its own consistency, then is able to prove everything, that is is inconsistent.
Thus, we know that Penao Arithmetic (PA) and Zermelo-Fraenkel Set Theory (ZF) are both unable to prove their own consistency. Well not quite. They cannot prove their own consistency provided they are consistent. How do we know that they are consistent? This is a well-known state of affairs, that Gödel created—or did he discover it? It is anyway very unappealing. We all work at proving theorems, usually working implicitly in PA or perhaps ZF, yet we could be proving nonsense. A scary thought—an old scary thought.
So what is our new scary thought? Since it is impossible to show that PA is consistent without appeal to a stronger theory, perhaps we can at least try to prove this:
There is some theory that is consistent.
Well the empty theory is consistent. If a theory has a finite model, then its consistency can be checked “by hand.” There are very weak theories with no finite models that are still easily seen to be consistent. So we mean strong enough theories that at least encode a substantial piece of mathematics. This means at least having arithmetic, which also is enough to make the theory undecidable—that is, that there is no decision procedure for deciding whether can prove a given sentence . So the real question is:
Can we prove that there exists a theory of arithmetic that is consistent and undecidable?
Of course ZF proves that PA is consistent, and there are subsets of ZF doing this that ZF can prove are consistent, but this hasn’t been enough to convince everyone—see this too. But perhaps we can make an existence proof that is immune to even these concerns?
Throughout mathematics and complexity theory we have existence proofs. We know, for example, that there are Boolean functions that require super-linear circuit complexity, yet all proofs are existence ones. We know that such functions exist, but have no explicit examples. Mathematics in general is filled with similar existence results, where we can prove that there are objects with property X but no one knows a single explicit example.
Behind the scenes we have been discussing a possibility that raises the spectre of a ‘no’ answer. Well maybe we have been seeing a ghost. We don’t know, and we are looking for the best way to express it—and maybe “ghostbust” it. This has been part of our delay with a Halloween post, though we could pretend that the “pretending” post was it. But for our further purposes too, we first want to put out this form of the idea that a formal theory might be able to prove the existence of something, even the existence of a proof, without being able to construct the theory or carry the proof out by itself.
Does a consistent undecidable theory exist? Can we prove this? How would we prove this? Belated happy Halloween. Boo.