# Axioms necessary for theoretical computer science

This question is inspired by a similar question about applied mathematics on mathoverflow, and that nagging thought that important questions of TCS such as P vs. NP might be independent of ZFC (or other systems). As a little background, reverse mathematics is the project of finding the axioms necessary to prove certain important theorems. In other words, we start at a set of theorems we expect to be true and try to derive the minimal set of 'natural' axioms that make them so.

I was wondering if the reverse mathematics approach has been applied to any important theorems of TCS. In particular to complexity theory. With deadlock on many open questions in TCS it seems natural to ask "what axioms have we not tried using?". Alternatively, have any important questions in TCS been shown to be independent of certain simple subsystems of second-order arithmetic?

-
Two possible axioms that may not be independent: 1) 3-SAT requires $2^{\Omega(n)}$ time. 2) Given satisfiable 3SAT formula, every efficient algorithm satisfies at most $7/8$-fraction of the clauses. Also, multiplication of two equal size primes is hard to invert (efficiently). –  Mohammad Al-Turkistany Feb 9 '11 at 6:37
This paper is relevant: Harry Buhrman, Lance Fortnow, Leen Torenvliet, "Six Hypotheses in Search of a Theorem," CCC, pp.2, 12th Annual IEEE Conference on Computational Complexity (CCC'97), 1997 –  Mohammad Al-Turkistany Feb 9 '11 at 7:46
The following question is related: cstheory.stackexchange.com/questions/1923/… Most of TCS can be formalized in RCA_0. The graph minor theorem is a rare exception. As Neel emphasizes, if you want new ideas, then look for new ideas; don't look for new axioms. The two are not at all the same. –  Timothy Chow Feb 9 '11 at 16:30
I am confused why results like statements on $P$ or $NP$ are stated. In my first TCS lecture, we started with natural numbers and some basic functions on them. The rest follows. Apparently I do not understand the question. –  Raphael Feb 9 '11 at 23:02
I just noticed this, but apparently Lipton asked a similar question in this post: rjlipton.wordpress.com/2011/02/03/… , to quote: "I wonder if there are proof techniques that involve ideas far beyond PA that we have not used, and which would help break open some of important problems. Should we be teaching our graduate students methods from areas of mathematics that lie beyond PA?" (PA = Peano Arithmetic) –  Artem Kaznatcheev Feb 11 '11 at 3:23

Yes, the topic has been studied in proof complexity. It is called Bounded Reverse Mathematics. You can find a table containing some reverse mathematics results on page 8 of Cook and Nguyen's book, "Logical Foundations of Proof Complexity", 2010. Some of Steve Cook's previous students have worked on similar topics, e.g. Nguyen's thesis, "Bounded Reverse Mathematics", University of Toronto, 2008.

Alexander Razborov (also other proof complexity theorists) has some results on the weak theories needed to formalize the circuit complexity techniques and prove circuit complexity lowerbounds. He obtains some unprovability results for weak theories, but the theories are considered too weak.

All of these results are provable in $RCA_0$ (Simpson's base theory for Reverse Mathematics), so AFAIK we don't have independence results from strong theories (and in fact such independence results would have strong consequences as Neel has mentioned, see Ben-David's work (and related results) on independence of $\mathbf{P} vs. \mathbf{NP}$ from $PA_1$ where $PA_1$ is an extension of $PA$).

-
Such independence results would be major breakthroughs, but I don't think they have any immediate strong consequences; see my comment on Neel's answer. –  Timothy Chow Feb 9 '11 at 16:37
@Tim, thanks, you are right, I fixed my answer. It is not $PA$, it is $PA_1$, $PA$ extended with all true universal sentences of arithmetic, and Ben-David claims that if the question is independent from this stronger theory then SAT has an almost polynomial time algorithm. So the assumption is (much) stronger but the final claim is the same. (and currently known methods of proving independence from $PA$ would also imply independence from $PA_1$.) –  Kaveh Feb 9 '11 at 16:44

As a positive answer to your final question, normalization proofs of polymorphic lambda calculi such as the calculus of constructions require at least higher-order arithmetic, and stronger systems (such as the calculus of inductive constructions) are equiconsistent with ZFC plus countably many inaccessibles.

As a negative answer to your final question, Ben-David and Halevi have shown that if $P \not= NP$ is independent of $PA_1$, Peano arithmetic extended with axioms for all universal arithmetic truths, then there is an almost polynomial algorithm $DTIME(n^{\log^{*}(n)})$ for SAT. Furthermore, there are presently no known ways to generate sentences which are independent of $PA$ but not $PA_1$.

More philosophically, do not make the mistake of equating consistency strength with the strength of an abstraction.

The correct way to organize a subject may involve apparently wild set-theoretic principles, even though they may not be strictly necessary in terms of consistency strength. For example, strong collection principles are very useful for stating uniformity properties -- e.g., category theorists end up wanting weak large cardinal axioms to manipulate things like category of all groups as if they were objects. The most famous example is algebraic geometry, whose development makes extensive use of Grothendieck universes, but all of whose applications (such as Fermat's Last Theorem) apparently lie within third-order arithmetic. As a much more trivial example, note that the generic identity and composition operations are not functions, since they are indexed over the whole universe of sets.

On the other hand, sometimes the relationship between consistency strength and abstractness goes in the opposite direction. Consider the relationship between measures and motivic measures. Measures are defined on families of subsets ($\sigma$-algebras) over a set $X$, whereas motivic measures are defined directly on formulas interpreted in $X$. So even though motivic measure generalizes measure, the set-theoretic complexity goes down, since one use of powerset goes away.

EDIT: Logical system A has greater consistency strength than system B, if the consistency of A implies the consistency of B. For example, ZFC has greater consistency strength than Peano arithmetic, since you can prove the consistency of PA in ZFC. A and B have the same consistency strength if they are equiconsistent. As an example, Peano arithmetic is consistent if and only if Heyting (constructive) arithmetic is.

IMO, one of the most amazing facts about logic is that consistency strength boils down to the question "what is the fastest-growing function you can prove total in this logic?" As a result, the consistency of many classes of logics can be linearly ordered! If you have an ordinal notation capable of describing the fastest growing functions your two logics can show total, then you know by trichotomy that either one can prove the consistency of the other, or they are equiconsistent.

But this astonishing fact is also why consistency strength is not the right tool for talking about mathematical abstractions. It is an invariant of a system including coding tricks, and a good abstraction lets you express an idea without tricks. However, we do not know enough about logic to express this idea formally.

-
what is 'consistency strength' ? –  Suresh Venkat Feb 9 '11 at 9:38
That's not what Ben-David and Halevi proved. You overlooked their crucial rider, "using currently available techniques." I interpret their paper as emphasizing how weak our current proof techniques are rather than as saying much about the P = NP question. –  Timothy Chow Feb 9 '11 at 16:28
Thanks for the correction! –  Neel Krishnaswami Feb 9 '11 at 16:40