# An obvious approach to explaining NP != coNP, how far has it been pushed?

A recent question made me think about an obvious approach for circumventing the "algorithm is allowed to do anything" problem, when proving lower bounds. Instead of starting with a simple looking NP-complete problem, start with a powerful looking logical deduction system.

Then try to find a reasonable general term expression problem, such that equality of the terms can be decided by the logical deduction system, and inequality of the term expressions is NP-complete. (For example, Boolean algebra term expressions would work.) Then start to prove that the logical deduction system cannot efficiently prove equality of specific term instances, unless it has access to specific higher order features, like the cut-rule.

And then the goal would be to push up the required higher orders features as far as possible, i.e. beyond the cut-rule towards fully impredicative higher order logic. But already proving that you need the cut-rule would seem like a nice achievement. How far has such an approach to explaining NP!=coNP actually been pushed in the past?

• Note that NP$\neq$coNP implies P$\neq$NP so we don't really expect it to be solved anytime soon. – Kaveh Jan 13 '16 at 1:27
• @Kaveh Note that the described approach doesn't risk to prove NP != coNP, even if it could be pushed towards fully impredicative higher order logic (or extended Frege). First, it always only tries to prove that a certain feature of a proof system is necessary, so it can never be applied to the "most general known" proof system (currently this would be "extended Frege"). Second, the considered term expression problem is not fixed, so the conclusion about the limitations of the proof system won't necessarily also apply to the SAT case (Boolean algebra term expressions). – Thomas Klimpel Jan 13 '16 at 1:54
• Frege + axioms can polynomially simulate any propositional proof system. You don't need any higher order proof system. – Kaveh Jan 13 '16 at 2:02
• @Kaveh Do you mean than for any propositional proof system (including any possible extended propositional Frege system), an appropriate propositional Frege proof system can polynomially simulate it? In that case, I would like to learn more! Or do you just mean that any (reasonable) proof system can be polynomially simulated by an appropriate Frege system (not limited to be propositional)? This would be the sort of "problem" which is circumvented by the approach above. – Thomas Klimpel Jan 15 '16 at 10:57

Not very far. The approach that you are describing is known as proof complexity, and it is covered by several surveys and lecture notes. There are several kinds of proof system being considered:

• Frege systems. These are systems in which a proof consists of a sequence of formulas or circuits (depending on the system), and there is a fixed set of derivation rules.

• Algebraic proof systems such as the Polynomial Calculus and Nullstellensatz. Here each line is a polynomial.

• Cutting planes, in which each line is a linear inequality.

There are also other proof systems such as the Hajos calculus, a proof system for proving that a graph isn't 3-colorable.

We have strong lower bounds for some of these systems, but in the Frege front, the best lower bound is for bounded depth Frege, in which the depth of all lines in the proof is bounded by some constant. This lower bound is similar in some regards to AC0 lower bounds for circuits, but is otherwise more complicated. We have no lower bound for the version in which the depth is bounded but we allow mod $p$ gates; the algebraic methods used to prove lower bounds on circuits don't seem to work, and the problem seems related to derandomizing polynomial identity testing, a notoriously difficult problem in algebraic complexity theory.

The Frege proof system itself has as lines arbitrary formulas, and Extended Frege has arbitrary circuits as lines. It is thought that Extended Frege is stronger than Frege. Other proof systems are conjectured to be stronger than even Extended Frege. It is not clear currently whether there is a "super" proof system, which is optimal up to polynomial factors compared to any proof system. Thus even if we do manage to prove lower bounds for progressively more general proof systems – which is expected to be harder than proving corresponding circuit lower bounds – we wouldn't necessarily be able to prove that NP is different from coNP in this way.

• I think at least some proof complexity theorists conjecture that Extended Frege is super. – Kaveh Jan 13 '16 at 1:30