Independence Day

July 4, 2013

tags: complexity, independence, John Adams, July 4, Logic, movies

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 ${\mathsf{P}=\mathsf{NP}}$ 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 ${T}$ . 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 ${\mathsf{P}=\mathsf{NP}}$ 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 ${\cal T}$ , is based on two, luckily not 39, steps. The initial step is to encode the statement into the theory as some formal statement ${S}$ . 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 ${S}$ and our theory ${\cal T}$ . Then we say the statement is independent provided the theory cannot prove ${S}$ and also cannot prove its negation. This is the second step. We can call the statement of this step ${I_{S,T}}$ .

The trouble is in the third step: How do we prove ${I_{S,T}}$ ? The double-trouble is that this is a more complicated beast than ${S}$ 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 ${T}$ 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,

$\displaystyle (S) \ \ \forall x \forall y \ \ x^{2} = 2\cdot y^{2} \Rightarrow x=0 \vee y=0.$

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 ${\mathbb{Q}}$ . Did you ever wonder why the symbol for rationals is not ${R}$ 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 ${\mathbb{Q}}$ to include a new element ${\alpha}$ . 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 ${\alpha}$ 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 ${\alpha}$ to change the fact that statement ${S}$ above is now false. Thus ${\alpha}$ cannot be ${\sqrt{2}}$ , since that would make ${S}$ false:

$\displaystyle \alpha^{2} = 2\cdot 1.$

On the other hand, we would want ${\alpha}$ to satisfy

$\displaystyle (2 + \alpha) \cdot 3 = 6 + 3\alpha.$

And we would want all the usual rules of addition and multiplication to apply to expressions that contain ${\alpha}$ .

The way to do all this is to think of ${\alpha}$ as variable. Then we formally consider all the rational functions in ${\alpha}$ with coefficients from ${\mathbb{Q}}$ . 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 ${\alpha}$ is truly generic: for example, for any non-trivial polynomial ${f(x)}$ with coefficients in ${\mathbb{Q}}$ ,

$\displaystyle f(\alpha) = 0$

is false.

This adding of ${\alpha}$ 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 ${f}$ as above, adjoin the axiom

$\displaystyle (S_f)\ \ f(\alpha) \neq 0$

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

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

The original sentence ${S}$ does not become independent—all sentences that were true in ${T}$ remain true in ${T'}$ . Indeed they are classed as trivial theorems of both theories. That’s a trouble with our initial informality: if we take ${T}$ to consist of all first-order statements that are true in ${\mathbb{Q}}$ 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 ${T}$ , and frame statements that express ignorance of elements like ${\alpha}$ . We would like to define statements ${S'}$ that intuitively say, “There exists an ${x}$ that is not rational,” or “There exists an ${x}$ that is not algebraic,” and conclude that they are independent. The problem when we naturally try to define ${S'}$ as follows,

$\displaystyle (S)\ \ (\exists x)(\forall r)\dots$

is that we have no way within ${T}$ to specify that ${r}$ is a member of ${\mathbb{Q}}$ . 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 ${S}$ is independent is that if ${S}$ is sufficiently simple, then this is tantamount to proving ${S}$ itself. Consider Goldbach’s Conjecture:

$\displaystyle (G) \ \ (\forall x > 1) (\exists p,q)[x+x = p+q \wedge p,q\text{ are prime}].$

If ${G}$ is false, then ${T}$ can prove it is false by finding a bad ${x}$ and verifying the finite computation showing it is not the sum of two primes. So if ${G}$ is independent, then ${G}$ 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, ${\mathsf{P = NP}}$ is not so simple. It has one of both kinds of quantifier:

$\displaystyle (\mathsf{P=NP})\ \ (\exists i)(\forall x)[P_i(x) = \mathsf{SAT}(x)],$

where ${[P_i]}$ is a fixed definable enumeration of polynomial time Turing machines. We can also re-cast the negation ${\mathsf{P \neq NP}}$ as the statement that the function ${f(i) =}$ the least ${x}$ such that ${P_i(x) \neq \mathsf{SAT}(x)}$ is a total computable function: ${(\forall i)(\exists x,c)[c\text{ verifies }f(i) = x]}$ .

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 ${\mathsf{P=NP}}$ can be independent. Let ${\mathsf{PA}+\Pi_1}$ stand for Peano Arithmetic augmented with all true ${\Pi_1}$ 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 ${f}$ —such as ${f}$ above for ${\mathsf{NP \neq P}}$ —is provably total in ${\mathsf{PA}}$ if and only if it is provably total in ${\mathsf{PA+\Pi_1}}$ .

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 ${\mathsf{PA}}$ actually prove independence from the stronger theory ${\mathsf{PA+\Pi_1}}$ .

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 ${\mathsf{PA}}$ can prove to be recursive. This means even faster than Ackermann’s function, into intuitively unimaginable rates of growth. Besides ${\mathsf{PA}}$ , this is a “general nonsense” when all true ${\Pi_1}$ statements in a theory are added as axioms—independence becomes a matter of speed.

In particular, if ${\mathsf{P \neq NP}}$ is true but independent, then the function ${f}$ must actually grow faster than the ${\mathsf{PA}}$ speed limit, for infinitely many ${i}$ . This means that there would be infinitely many relatively short and fast programs ${P_i}$ that get satisfiability correct on an extraordinarily long range of input lengths. I (Ken) once tried to argue that the self-reducibility structure of ${\mathsf{SAT}}$ 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 ${\mathsf{P = NP}}$ down:

Can we find interesting conditions ${P}$ such that when ${P}$ is assumed, ${\mathsf{P = NP}}$ becomes equivalent to a purely universal or purely existential statement?

There have been some abortive claims to have obtained this unconditionally, thus classifying ${\mathsf{P = NP}}$ as “resolvable if independent,” but we suspect that interesting properties ${P}$ 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…

8 Comments leave one →

KWRegan permalink

July 5, 2013 12:34 am

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.

Reply
- KWRegan permalink
  
  July 5, 2013 11:02 am
  
  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.
  
  Reply
Jon Awbrey permalink

July 5, 2013 8:00 am

Strange luck that so much of our scientific knowledge depends on the IIDea of IIDiocracy.

Reply
william e emba permalink

July 5, 2013 8:25 am

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.

Reply
John Sidles permalink

July 5, 2013 10:24 am

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.

Q1 What is the optimal/stable PD response to “prisoner” algorithms whose runtime is polynomial, but not provably polynomial?

Q2 Would it be reasonable to exclude “independent” algorithms from the PD game, in the event that powerful theorems were made easier to prove by this exclusion?

As Joseph Landsberg has said (in the context of geometric complexity theory):

When complexity theorists and mathematicians are confronted with a [difficult/conflicting] situation, what else do they do other than make another definition?

The celebrated GLL “Flaming arrow principle” appears in yet another guise!🙂

Reply
Proof Checker permalink

July 10, 2013 7:39 am

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.

Reply
- KWRegan permalink
  
  July 10, 2013 11:39 pm
  
  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.
  
  Reply

Trackbacks

Surely You Are Joking? | Gödel's Lost Letter and P=NP

	B. on A Creeping Model Of Compu…
	andreimigunov on A Creeping Model Of Compu…
	Laci Pyber on The World Series Of Complexity…
	Borei Lubicich on Miracle Numbers Such as…
	gentzen on The Word Problem for Free…
	A Proof Of The Halti… on A Proof Of The Halting Th…
	Aula on A Proof Of The Halting Th…
	jean temps on Cantor’s Non-Diagonal Pr…
	Cris Moore on A Proof Of The Halting Th…
	Jim Hefferon on A Proof Of The Halting Th…
	kevembuangga on A Proof Of The Halting Th…
	Cris Moore on A Proof Of The Halting Th…
	rjlipton on A Proof Of The Halting Th…
	Sheshbazzar on Judging A Book By Its Cov…
	domotorp on A Proof Of The Halting Th…

a personal view of the theory of computation

Independence Day

Some Fun

Double Trouble and Triple Trouble

A Clue

Over the Top

The Power of One Quantifier

Feeling the Need For Speed

Open Problems

Trackbacks

Leave a Reply Cancel reply

Subscribe to Gödel’s Lost Letter

Our Book

Recent Posts

Top Posts

Recent Comments

Blogroll

Archives

Sitemeter

a personal view of the theory of computation

Independence Day

Some Fun

Double Trouble and Triple Trouble

A Clue

Over the Top

The Power of One Quantifier

Feeling the Need For Speed

Open Problems

Share this:

Like this:

Related

Trackbacks

Leave a Reply Cancel reply

Subscribe to Gödel’s Lost Letter

Our Book

Recent Posts

Top Posts

Recent Comments

Blogroll

Archives

Sitemeter