Independence Day

Will logical independence have its day?

John Adams was the second president of the United States. He predicted that July 2nd would be always remembered: “The second day of July, 1776, will be the most memorable epoch in the history of America.” He based this on the day that the Second Continental Congress voted to affirm a resolution of independence from Great Britain. He was off because the text of the explanation for that decision was not finalized and adopted until the 4th, whereupon it was immediately sent to printers for publication that evening. That is to say, the publication date of the paper is what counts.

Today Ken and I wish to talk about independence, not the day, not the holiday, but the notion of logical independence.

When we think about the question, among other open problems, we often think about whether such questions could be independent. Recall that these means that a given logical theory is unable to prove or disprove the question. Of course thanks to Kurt Gödel we now know that there are such statements in any reasonably powerful logical theory . One can say his method was based on a variation of the Liar Paradox. Here is one version:

‘All Britons are liars’? True, false, or impossible?

But there is no method on the horizon that seems to give any hope that the question could be shown to be independent. Anyway, we thought in the spirit of our independence day you might like to hear some thoughts on logical independence.

Some Fun

The long July 4th weekend also serves as a traditional beginning of summer celebrations, since many schools continue until the end of June. This includes seeing summer movies. One such movie was “Independence Day” itself, whose plot turns on the fact that Turing computability is literally universal. For fun this post has allusions to other movies, by title or quote. The answers are at the end. In the spirit of fun and a holiday we thought you might enjoy this. Can you handle the truth?

It is interesting that the Declaration was first read in public by a man named Nixon, on July 8, 1776, in Philadelphia. On July 9th a newspaper for the first time printed it on the front page, in German—our readers who know German can judge whether anything was lost in translation. If so, well nobody’s perfect.

Double Trouble and Triple Trouble

The notion that a math question is independent from a given formal theory, say , is based on two, luckily not 39, steps. The initial step is to encode the statement into the theory as some formal statement . Note this can be straightforward, but it can be tricky. Indeed there are examples in logic where if the “wrong” encoding is used, then the statement can be proved. On the other hand, if the “right” stuff is used, then the statement can be proved to be independent. This arises already in Gödel’s famous Second Theorem on the unprovability of the consistency of arithmetic. Thus there are “wrong statements” that seem to capture consistency but can be proved. Let’s leave this for another time.

Okay so we have a statement and our theory . Then we say the statement is independent provided the theory cannot prove and also cannot prove its negation. This is the second step. We can call the statement of this step .

The trouble is in the third step: How do we prove ? The double-trouble is that this is a more complicated beast than was. The triple-trouble is that there actually seem to be barriers to proving independence results:

1. There’s something about definability…

2. The statement, when basic, is already resolved.

3. Pi statements get added when only the strong systems are in the line of fire.

A Clue

The following idea seems like it should readily generate independence results, but there’s a hitch. Instead of defining logical systems formally, let us consider the rational numbers and the informal idea of a theory of them. We can write lots of interesting statements in this theory. For example,

This statement is, of course, true: it encodes in the formal system the informal statement that the square root of two is irrational.

Imagine the rationals which we will denote by . Did you ever wonder why the symbol for rationals is not or something like that? Que será, será. Well it does have a rational—ha—reason for this name. Giuseppe Peano named it in 1895 after quoziente, Italian for “quotient.”

Now suppose that we want to extend the rationals to include a new element . But we want this element to be generic. We want it to have all the properties that it needs to make the extension still look close to the rationals, but also want to avoid having any specific property.

The generic notion is a bit vague, so let’s try and say it more precisely. For example, we would not want the addition of to change the fact that statement above is now false. Thus cannot be , since that would make false:

On the other hand, we would want to satisfy

And we would want all the usual rules of addition and multiplication to apply to expressions that contain .

The way to do all this is to think of as variable. Then we formally consider all the rational functions in with coefficients from . These elements are now the elements of our world. It is not hard to show that all the usual rules still apply to them. What is really important is that aside from this they have nothing in common. The element is truly generic: for example, for any non-trivial polynomial with coefficients in ,

is false.

This adding of has created a new world where the old rules of engagement mostly apply, but where we have new elements that are available for use. The problem is that the world is not enough. Let’s see why.

Over the Top

We would like to apply an overspill argument that would go like this: For every polynomial as above, adjoin the axiom

to . Call the resulting theory . Now every finite subset of is consistent, because given any finite set of polynomials , we can always find a rational number that is not a zero of any of them. Hence by the first-order compactness theorem, is consistent. Hence it has a model , in which is assigned a value—still a suitably generic value.

We have in fact forced the extension of by a transcendental number , plus all the elements that follow algebraically from . The model is the new world. We would like to interpret this new world in terms of independence under the old theory , but this is not easy living.

The original sentence does not become independent—all sentences that were true in remain true in . Indeed they are classed as trivial theorems of both theories. That’s a trouble with our initial informality: if we take to consist of all first-order statements that are true in then we already have a complete theory and there is nowhere to hide anything else.

So we would like to start with a natural, limited, computably axiomatized theory , and frame statements that express ignorance of elements like . We would like to define statements that intuitively say, “There exists an that is not rational,” or “There exists an that is not algebraic,” and conclude that they are independent. The problem when we naturally try to define as follows,

is that we have no way within to specify that is a member of . First-order theories usually cannot define their domains. If we could, then “overspill” would actually give us a contradiction or inconsistency.

The genius of Paul Cohen’s method of forcing is that it is able to adjoin new elements in a first-order controlled manner while staying within the domain of sets. Maybe in a future post we can try to make this analogy better. We wonder whether one can adapt this method to complexity theory via an algebra of constructing languages and considering their differences. If so, we could call this the “Delta Force.”

The Power of One Quantifier

A second trouble with trying to prove a statement is independent is that if is sufficiently simple, then this is tantamount to proving itself. Consider Goldbach’s Conjecture:

If is false, then can prove it is false by finding a bad and verifying the finite computation showing it is not the sum of two primes. So if is independent, then must be true. Similar considerations apply to big fish like the Riemann Hypothesis—undecided problems with forms that have only universal or only existential unbounded quantifiers in their statements.

Importantly, is not so simple. It has one of both kinds of quantifier:

where is a fixed definable enumeration of polynomial time Turing machines. We can also re-cast the negation as the statement that the function the least such that is a total computable function: .

Feeling the Need For Speed

The third difficulty—maybe the one that really qualifies as a “barrier”—is the following fact also given special note in this survey by Scott Aaronson on whether can be independent. Let stand for Peano Arithmetic augmented with all true statements about natural (or rational) numbers. That is we add universal statments like Goldbach and Riemann as above—if they are true. The basic fact was proved by Georg Kreisel:

Lemma 1 An integer function —such as above for —is provably total in if and only if it is provably total in .

The upshot—not a mathematical consequence but practically—is noted earlier in the survey:

With the exception of Gödel’s Incompleteness Theorem, all the techniques we have for proving independence from actually prove independence from the stronger theory .

What comes out is that the other independence results by and large revolve around functions whose values grow faster than those of any function that can prove to be recursive. This means even faster than Ackermann’s function, into intuitively unimaginable rates of growth. Besides , this is a “general nonsense” when all true statements in a theory are added as axioms—independence becomes a matter of speed.

In particular, if is true but independent, then the function must actually grow faster than the speed limit, for infinitely many . This means that there would be infinitely many relatively short and fast programs that get satisfiability correct on an extraordinarily long range of input lengths. I (Ken) once tried to argue that the self-reducibility structure of would rule out this independence scenario, but no one seems to have made real progress since the early 1990’s. There was also work on weaker theories whose growth limits would come down to the accessible realm of exponential or even polynomial, but they lack the correspondence to strong proof techniques used in everyday mathematics, and this too seems to be in the rear window. How can this line get its groove back?

Instead of adding true universal statements as axioms and working up, we suggest the idea of looking for weaker conditions that could help in working the logical statement down:

Can we find interesting conditions such that when is assumed, becomes equivalent to a purely universal or purely existential statement?

There have been some abortive claims to have obtained this unconditionally, thus classifying as “resolvable if independent,” but we suspect that interesting properties ought to come out of this more modest goal.

Open Problems

Can any of the “movies on P=NP” be an indie flick?

Those in the US, we hope you have enjoyed the fireworks, the traditional foods, and the fun. To all elsewhere, Ken and I hope you all enjoy your own independent ways, wherever you are.

Answers? We ain’t got no answers. We don’t need no answers! I don’t have to show you any stinkin’ answers! Maybe the Friday after next…

Advertisements