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.

The Question

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 ${T}$ that is strong enough—more on this in a moment—cannot prove its own consistency. More precisely if ${T}$ proves its own consistency, then ${T}$ is able to prove everything, that is ${T}$ 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 ${T}$ 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 ${T}$ can prove a given sentence ${S}$. So the real question is:

Can we prove that there exists a theory of arithmetic ${T}$ 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.

Open Problems

Does a consistent undecidable theory exist? Can we prove this? How would we prove this? Belated happy Halloween. Boo.

1. November 3, 2013 6:30 pm

The scary question might get a scary answer in case New Foundations turns out indeed to be provably consistent, as announced by Randall Holmes about an year ago.

November 3, 2013 6:55 pm

Reblogged this on Pink Iguana.

November 3, 2013 8:09 pm

Here are three non-Gödelian maxims that address the concerns raised by Dick and Ken: the first attributed to a mathematician, the second to a sage, the third to a basketball player:

•  “Allez en avant, et la foi vous viendra” (Set forth and faith will come to you).

•  “If you are not happy, act the happy man. Happiness will come later. So also with faith. If you are in despair, act as though you believed. Faith will come afterwards.”

•  “I’ve missed more than nine thousand shots in my career. I’ve lost almost three hundred games. Twenty-six times, I’ve been trusted to take the game winning shot and missed. I’ve failed over and over and over again in my life. And that is why I succeed.”

Summary  Faith comes after the practice of creative mathematics, the discovery of new science, the performance of kind deeds, and the creation of successful enterprises. Not before!

————-
References
@book{, Annote = {p. 481: Carnot quotes Jean-Baptiste le Rond d'Alembert \emph{Allez en avant, et la foi vous viendra''} (Set forth and faith will come to you)}, Author = {Carnot, L.N.M.}, Publisher = {Paris, Imprimerie de Crapelet}, Title = {G{\'e}om{\'e}trie de position}, Year = {1803}}

 @incollection{, Annote = {p. 144 (concluding words) If you are not happy, act the happy man. Happiness will come later. So also with faith. If you are in despair, act as though you believed. Faith will come afterwards.''}, Author = {Singer, I.B.}, Booktitle = {Spinoza of Market Street and Other Stories}, Pages = {135--144}, Publisher = {Farrar, Straus and Giroux}, Title = {A piece of Advice}, Year = {1979}} 

@misc{, Annote = {I've missed more than nine thousand shots in my career. I've lost almost three hundred games. Twenty-six times, I've been trusted to take the game winning shot and missed. I've failed over and over and over again in my life. And that is why I succeed.''}, Author = {Michael Jordan}, Howpublished = {Motivational poster}, Title = {Why I succeed}, Year = {2013}}

• November 4, 2013 10:52 am

Ah, but a man’s reach should exceed his grasp,
Or what’s a heaven for?

July 15, 2014 3:03 pm

“Faith comes after the practice of creative mathematics”

I think you’ve HTNOTH! Based on the success of numeric mathematics, all of which depends on Peano arithmetic, we believe it is consistent. It has earned our trust.

There are some things in life that just don’t need to be proven.

4. November 3, 2013 9:23 pm

I’ve solved (eluded) that problem as follows: there’s evidence that we can find in Nature (not the magazine) that confirms the coherent use of Peano’s theory. In fact, the rules it follows are coherent with our use of our fingers to count. So, why not to believe Math’s logical systems are consistent?

I can’t stop laughing, «Boo!», ha, ha, ha. That’s great! 😀

5. November 3, 2013 10:28 pm

Reblogged this on My Chick Mail.

November 4, 2013 3:24 am

I’m sure you’re aware of Gentzen’s consistency proof, which arguably resolved this open question in 1936. In particular, it is not accurate to say that “it is impossible to show that PA is consistent without appeal to a stronger theory”. Gentzen’s proof provides a counterexample, since it takes place in $PRA+\epsilon_0$ (primitive recursive arithmetic plus transfinite induction up to the ordinal $\epsilon_0$), which is strictly incomparable with PA (it includes a stronger induction principle, but a weaker logical language). Moreover, Gentzen’s proof can be given a simple combinatorial interpretation, e.g., corresponding to the termination of all Goodstein sequences.

Yes, it is still possible that PA is *inconsistent*, as Edward Nelson and more recently Vladimir Voevodsky have pointed out. But we don’t use this permanent fact of life to question whether, say, Andrew Wiles’ proof really solved the open problem of Fermat’s Last Theorem, even though it used principles much stronger than Gentzen’s proof.

November 4, 2013 8:52 am

“But perhaps we can make an existence proof that is immune to even these concerns? … Behind the scenes we have been discussing a possibility that raises the spectre of a `no’ answer. … Does a consistent undecidable theory exist? Can we prove this? How would we prove this?”

Such spectres can be seen to be evanescent if we view arithmetic from a finitary computational, rather than a non-finitary set-theoretical, perspective.

For instance, so far as the consistency of arithmetic is concerned, this paper on ‘Evidence-Based Interpretations of PA’, presented at IACAP/AISB Turing 2012 in Birmingham, shows that Tarski’s inductive definitions admit evidence-based interpretations of the first-order Peano Arithmetic PA that allow us to define the satisfaction and truth of the quantified formulas of PA constructively over the domain $\mathbb{N}$ of the natural numbers in two essentially different ways:

(a) in terms of algorithmic verifiabilty; and

(b) in terms of algorithmic computability.

Definition (a) yields the classical standard non-finitary interpretation of PA, from which we cannot conclude that PA is consistent (since the Axiom Schema of Finite Induction does not interpret as an arithmetical statement about the natural numbers that can be algorithmically verified as ‘true’ in an intuitionistically unobjectionable manner).

Definition (b) yields an algorithmic finitary interpretation of PA from which we can, however, conclude that PA is consistent (since the Axiom Schema of Finite Induction does interpret as an arithmetical statement about the natural numbers that can be algorithmically computed as ‘true’ in an intuitionistically unobjectionable manner).

So far as existence proofs and undecidable Gödelian propositions are concerned:

(i) PA admits undecidable Gödelian propositions if we admit Aristotle’s particularisation (i.e., if we allow the—non-verifiable—conclusion from the provability of $[(\exists x)R(x)]$ that there exists some natural number $n$ such that $R(n)$ is a ‘true’ arithmetical statement);

(ii) PA does not admit undecidable Gödelian propositions if we do not admit Aristotle’s particularisation (i.e., if we only allow the—equally non-verifiable—conclusion from the provability of $[(\exists x)R(x)]$ that there is no algorithm that can determine whether there exists some natural number $n$ such that $R(n)$ is a ‘true’ arithmetical statement).

So, prima facie, the choice seems determined by what it is we intend to communicate as ‘true’!

It is not really as ‘scary’ a choice as it may seem, because the two interpretations appear to be equally valid ways of reasoning about arithmetical propositions which, though seemingly contradictory, may actually be complementary.

For instance, a case can be made that the ‘truths’ of nature are algorithmically verifiable, but not necessarily algorithmically computable.

On the other hand, the ‘truths’ that would allow effective and unambiguous communication between any two essentially different intelligences can only be those that are both algorithmically verifiable and algorithmically computable.

November 4, 2013 11:44 am

Responses to this Gödel’s Lost Letter essay “A Really Scary Thought” are particularly welcome to the degree that they also address the well-rated but unanswered MathOverflow question For which Millennium Problems does undecidable -> true?

Nowadays that question might be posed:in a variant form:

For which Millennium Postulates could non-disprovable counter-examples be constructed?

E.g., how might we unmask a charlatan who constructed a Turing Machine (TM) that was asserted to run in PTIME (but was not provably in PTIME); a TM that was further asserted to solve NP-complete problems for all input tape-lengths greater than some threshold length (a threshold length that however the charlatan does not specify, and that therefore can exceed any concretely given finite bound).

The intent of these questions is to capture a scary intuition — that possibly is associated to Dick and Ken’s “scary thought” — that the rigorous verification and validation of PvsNP counter-examples encounters proof-theoretic difficulties that are insurmountably tougher than the difficulties associated to verifying and validating counter-examples of (for example) the Hodge Conjecture.

• November 4, 2013 12:35 pm

November 4, 2013 2:20 pm

Thank you Michael. You might enjoy too the work reported in Henri Darmon’s on-line notes The Hodge and Tate conjectures: some numerical experiments (joint work with Massimo Bertolini and Kartik Prasanna) which illustrates concrete computational methods for verifying and validating the Hodge and Tate postulates. Needless to say, it is far from straightforward to formalize the intuition that “charlatan TMs” in P readily defeat comparable tests of PvsNP separation, such that PvsNP belongs to an intrinsically tougher class of problems than the Hodge/Tate conjectures (perhaps even an undecidable class?).

Disclaimer  In-depth appreciation of the Hodge/Tate conjectures (in particular their verification/validation) is vastly beyond my own mathematical expertise … comments from *real* experts are welcome.

• November 5, 2013 5:30 pm

Cool!

9. November 4, 2013 11:45 am

“There are very weak theories with no finite models that are still easily seen to be consistent.”
so whats the strongest nonfinite-model theory that has been proven consistent?
“Does a consistent undecidable theory exist? Can we prove this? How would we prove this? ”
sounds very close to an undecidable question, doesnt it?

dont quite have an answer to your difficult question but suggest there may be some relation to quasi-algorithms, a seemingly important idea but which hasnt been formalized much.

November 4, 2013 3:33 pm

“Mathematics is consistent” – my favorite axiom! 🙂

In any case, it’s no more daring than the consistency of set theory itself, from which follows that an arbitrary real number is almost surely normal in every base. Unfortunately, the only known number to have this property happens to be uncomputable: that’s Chaitin’s constant Omega. Indeed, numbers seem to behave like theories…

November 5, 2013 7:54 pm

My conjecture:

A real number that can be defined without referring to its digits can’t contain every integer as a specific computable subsequence of its digits.

November 5, 2013 12:11 am

this is just a note to the moderators: I left a comment yesterday morning, and it is still awaiting moderation. Since other comments have followed, I wonder if it got overlooked?

November 5, 2013 4:00 pm

Noam, if you restrict your comment to include at most one web-link, then the comment will (usually) appear immediately. Because your web page “In Tune With Fun” is wonderfully funny and good-natured — which (as it seems to me) is an not-too-common and valuable combination — it is my pleasure to provide this link to it.

Now please sir, Oliver Twist would like some type theory!

November 5, 2013 6:37 pm

Thanks for the tip!

12. November 11, 2013 3:27 am

I think one of the things that makes mathematics tricky but beautiful is how the discipline is very fluid but consistently so.

Leopold Kronecker once said, “God made natural numbers; all else is the work of man.” This quote is, in my opinion, the foundation of mathematics. Most of what we study in theoretical mathematics has been constructed by us through the compilation of centuries of work. We create rules that govern the essential mechanics of the field (laws and definitions) but the way those rules interact or how they manifest in math are fluid, or dependent on the other constructions.

“Existence” in mathematics differs from other fields, such as physics. Mathematicians often create functions or sets in order to represent concepts or ideas and thus (1) are not limited to just physical phenomena or patterns and (2) are tools rather than hard and fast rules or laws. Take the Cantor set for example, which is an example of a sequence that is both bounded and infinite, and fundamental to modern topology. Without such an example, a person may be inclined to believe it is impossible to have a sequence that can exhibit seemingly contradictory properties.

In the case of Peano axioms, the axioms are representative of how we have come to understand the behavior of natural numbers historically and while Peano axioms can be thought of as fundamental to mathematical analysis (especially for constructs the real numbers from the natural numbers), it is not necessarily true in other fields of mathematics. One reason for this is that natural numbers in mathematical analysis are assumed to extend to infinity and therefore, there is no largest natural number N that can be an upper bound.

In contrast, in algebra we often categorize numbers into groups or rings by using a different set of assumptions or constructions. It is not uncommon to use modular arithmetic, which allows a sequence of integers to extend to infinity, yet have an upper bound. It is also possible for two consecutive values in the sequence to violate the Peano axioms.

Maybe we should be asking as a secondary question: Is consistency even sufficient or necessary to consider something true? And if so, what are the rules for a consistent theory or for a true theory?