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:
- There’s something about definability…
- The statement, when basic, is already resolved.
-
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…
Regarding Kreisel’s lemma, I’d previously recalled the “general nonsense” for a reasonably strong theory T being that if a function f is provably recursive in T+Π_1 then f is bounded by a provably recursive function of T. Under what circumstances does this make no difference? This may be related to the issue in the appendix of the 1991 paper by Shai Ben-David and Shai Halevi about whether the provably total machine used to compute f also needs to be provably equivalent to some original specification of f.
I can deduce the stronger statement from my version with “bounded by” as follows: Let f be provably recursive in T+Pi_1, meaning there is a TM M computing f such that T+Pi-1 proves “M is total”. Replace f by the step-counting function f’ of M, then f’ is also provably recursive in T+Pi_1, and we may suppose as a general rule that f’ always majorizes f. By hypothesis f’ is bounded by some function g computed by a TM G that is provably total in T alone, and ditto the step-counting function g’ of G. Now define a TM H that is coded to work as follows on input x:
H(x): Simulate M(x) and G(x) in lockstep. If G(x) halts before M(x) does, then H(x) outputs 0; else H(x) outputs what M(x) has already outputted, which is f(x).
Now per “general nonsense” assumptions about the ability of T to decipher code, T itself can prove that H is total. And in fact H computes f. So f meets the definition of being provably recursive in the theory T.
The “weakness” noted by Ben-David and Halevi in their appendix is here that T might not prove that the function computed by H is the same as f. When f is the witness function for SAT, this issue gets dicey. In any event, the point that tumbles out is that the only thing that matters is the growth rate of the functions, which (IMHO) limits the interest of this line unless and until we find something more clever.
Strange luck that so much of our scientific knowledge depends on the IIDea of IIDiocracy.
Forcing was generalized to model theory by Abraham Robinson. It was essentially an intuitive way to apply the omitting types theorem, see Hodges, Building models and games. It has been used to generate models of bounded arithmetic, and thus has applications to complexity theory. See Krajíček, Forcing with random variables and proof complexity.
Single-quantifier formulas can still be susceptible to set-theoretic issues. The rate of growth could be so large, for example, that it not only goes beyond PA, but ZF. For example, the Matiyasevich theorem tells us there is a Diaphontine equation encoding the proofs that measurable cardinals are inconsistent with ZF. A complexity analog would be to offer an algorithm that is provably polynomial except for one stubborn case, whose very existence depends on large cardinals.
Less Wrong has a charming thread on the topic Robust Cooperation in the Prisoner’s Dilemma (PD). The novel element of the Less Wrong PD game is that every “prisoner” is a concrete algorithm that is given full access to the source code of every other “prisoner” algorithm.
As Joseph Landsberg has said (in the context of geometric complexity theory):
The celebrated GLL “Flaming arrow principle” appears in yet another guise! 🙂
Ben-David and Halevi don’t have an unconditional “P!=NP independent of PA => SAT is often easy.” Their result has an ominous additonal hypothesis that independence is proved “by any known method.” Thus, another way to interpret their result is to say that “new methods” would be needed to prove independence and retain the hardness of SAT (similar like oracle results tell us that “known methods” of recursion theory don’t suffice to decide the P vs NP problem). Also in the Appendix a caveat is put on a too optimistic use of Kreisel’s Lemma that Aaronson falls prey to in Section 5 of his survey.
Great to hear from you. I recognized the same about Aaronson’s survey and tried to nudge this in how I wrote the last section—see also my comments above which I added soon after posting. Maybe I still need to clarify that my sentence beginning “In particular…independent” in the post is following on from the previous sentence where the Pi_1 statements are added. It’s also not quite right that you get small circuits in the way Aaronson states—I worded that carefully with the “i.o.” aspect clear.