<p>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. </p>

<p>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$. </p>

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

<p>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.  </p>

<p>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 <em>down</em>, since one use of powerset goes away.</p>

<p>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. </p>

<p>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.</p>

<p>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 <em>without</em> tricks. However, we do not know enough about logic to express this idea formally. </p>

CC BY-SA 2.5
2011-02-09T09:38:37.037Z
what is 'consistency strength' ?
Suresh Venkat
CC BY-SA 2.5
2011-02-09T16:28:47.410Z
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
CC BY-SA 2.5
2011-02-09T09:31:45.110Z
2011-02-09T18:16:13.210Z
2011-02-09T18:16:13.210Z
Neel Krishnaswami
<p>Yes, the topic has been studied in proof complexity. It is called <em>Bounded Reverse Mathematics</em>. You can find a table containing some reverse mathematics results on page 8 of Cook and Nguyen's book, "<a href="http://www.cs.toronto.edu/~sacook/homepage/book">Logical Foundations of Proof Complexity</a>",  2010. Some of Steve Cook's previous students have worked on similar topics, e.g. Nguyen's thesis, "<a href="http://www.cs.toronto.edu/~pnguyen/studies/thesis.pdf">Bounded Reverse Mathematics</a>", University of Toronto, 2008.</p>

<p>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.</p>

<p>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$).</p>

CC BY-SA 2.5
2011-02-09T16:37:45.087Z
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
CC BY-SA 2.5
2011-02-09T16:44:51.340Z
@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
CC BY-SA 2.5
2011-02-09T12:57:07.663Z
2011-02-09T16:43:00.903Z
2011-02-09T16:43:00.903Z
Kaveh
<p>This question is inspired by a <a href="https://mathoverflow.net/questions/54818/consistency-strength-needed-for-applied-mathematics">similar question</a> 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, <a href="http://en.wikipedia.org/wiki/Reverse_mathematics" rel="noreferrer">reverse mathematics</a> 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. </p>

<p>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?</p>

CC BY-SA 2.5
2011-02-09T06:37:29.990Z
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
CC BY-SA 2.5
2011-02-09T07:46:39.253Z
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
CC BY-SA 2.5
2011-02-09T15:34:30.710Z
I hope that answers/comments to this question will include  references to "reverse complexity theory", of which an example is "What is the largest subset P' of P, such that P' has a provable separation from NP'?". The motivating intuition is one that Ketan Mulmuley has expressed (and maybe others too), that the P includes Turing machines whose properties are utterly mysterious.  For engineering applications, which require that algorithms be validated and verified, it is natural to restrict P to exclude its "mystery members"; thus references in this regard are very welcome.
John Sidles
CC BY-SA 2.5
2011-02-09T16:30:56.173Z
The following question is related: http://cstheory.stackexchange.com/questions/1923/which-interesting-theorems-in-tcs-rely-on-the-axiom-of-choice-or-alternatively 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
CC BY-SA 2.5
2011-02-09T23:02:17.500Z
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
CC BY-SA 2.5
2011-02-11T03:23:48.643Z
I just noticed this, but apparently Lipton asked a similar question in this post: http://rjlipton.wordpress.com/2011/02/03/infinite-objects-and-deep-proofs/ , 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
CC BY-SA 3.0
2014-07-06T19:34:10.417Z
My personal philosophy about mathematics , axiomatic theories , for computational complexity too, and physical reality etc can be partially found in my blog and online-book under construction here http://thedigitalmathematics.blogspot.gr and here http://thenewuniversalattraction.blogspot.gr
Constantine Kyritsis
<cc.complexity-theory><lo.logic><proof-complexity>
Axioms necessary for theoretical computer science
Artem Kaznatcheev
# Axioms necessary for theoretical computer science

(Asked by: username_0 on 2011-02-09)

This question is inspired by a [similar question](https://mathoverflow.net/questions/54818/consistency-strength-needed-for-applied-mathematics) 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](http://en.wikipedia.org/wiki/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?

**Tags:** cc.complexity-theory, lo.logic, proof-complexity

> **Comments:**
> **username_1**: 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).  
> **username_1**: 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  
> **username_2**: I hope that answers/comments to this question will include  references to "reverse complexity theory", of which an example is "What is the largest subset P' of P, such that P' has a provable separation from NP'?". The motivating intuition is one that Ketan Mulmuley has expressed (and maybe others too), that the P includes Turing machines whose properties are utterly mysterious.  For engineering applications, which require that algorithms be validated and verified, it is natural to restrict P to exclude its "mystery members"; thus references in this regard are very welcome.  
> **username_3**: The following question is related: http://cstheory.stackexchange.com/questions/1923/which-interesting-theorems-in-tcs-rely-on-the-axiom-of-choice-or-alternatively 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.  
> **username_4**: 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.  
> **username_0**: I just noticed this, but apparently Lipton asked a similar question in this post: http://rjlipton.wordpress.com/2011/02/03/infinite-objects-and-deep-proofs/ , 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)  
> **username_5**: My personal philosophy about mathematics , axiomatic theories , for computational complexity too, and physical reality etc can be partially found in my blog and online-book under construction here http://thedigitalmathematics.blogspot.gr and here http://thenewuniversalattraction.blogspot.gr  

---

## 2 answers

### Answer by username_8 on 2011-02-09. Score: 24 | Accepted answer

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](http://www.cs.toronto.edu/~sacook/homepage/book)", 2010. Some of Steve Cook's previous students have worked on similar topics, e.g. Nguyen's thesis, "[Bounded Reverse Mathematics](http://www.cs.toronto.edu/~pnguyen/studies/thesis.pdf)", 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$).

> **Comments:**
> **username_3**: 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.  
> **username_8**: @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$.)  

---

### Answer by username_6 on 2011-02-09. Score: 21

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.

> **Comments:**
> **username_7**: what is 'consistency strength' ?  
> **username_3**: 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.  

---

