Proof Complexity and Circuit Lower bound for coNP

Question

I have two questions

(1)Circuit lower bound for coNP

TAUT is a set of formulae such that any formula in TAUT is satisfied for all boolean assignments. UnSAT is the complement problem of SAT.

It is known that if NP$\neq$coNP then P$\neq$ NP, and that solving NP vs coNP problem is harder task than proving circuit lower bound of NP-complete problems.

Is the following statement true?

Proving NP is not equal to coNP by showing a super-poly lower bound of proof size is "harder" task than deriving super-poly circuit lower bounds for a coNP-complete problem such as TAUT or UnSAT.

I think that this is true because NP and coNP has a "symmentric" relation.

(2)Uniform theory of proof complexity

There are two streams of circuit complexity. First one is concrete complexity lower bounds for Non-uniform models like Sipser's PARITY lower bounds for constant depth circuit. Second one is simulation based lower bounds which is intensively argued in a book of Introduction to Circuit Complexity: A Uniform Approach by Vollmer.

Can we construct a simulation based uniform theory of proof systems and deriving structural separatins beween two classes of proof systems ?

Answer 1

For the first question, it depends on what you mean by "harder". If you mean one logically implies the other then yes.

A lowerbound in a deterministic model of computation (containing negation) works also for the complement of the language because it is deciding the language. Therefore a circuit lowerbound for an $\mathsf{NP}$ problem is also a circuit lowerbound for its complement which is in $\mathsf{coNP}$.

(If you mean finding a proof of one is considerable harder than finding a proof of the other then it is a matter of opinion and arguable.)

For the second question, the concept of uniform proof complexity corresponds to theories in bounded arithmetic. You can translate proofs in such theories to propositional proofs using the propositional translation. See Stephen A. Cook and Phuong Nguyen, "Logical Foundations of Proof Complexity", 2010. These theories correspond to the uniform version of propositional proof systems in a similar way that uniform complexity classes like $\mathsf{P}$ are considered to be the uniform version of non-uniform complexity classes like $\mathsf{P/poly}$. There are other nice relations between the uniform and non-uniform proof systems that add justification to this correspondence. (Some ideas goes back to Steve'e original paper "Feasibly Constructive Proofs and the Propositional Calculus" from 1975 paper).

One can define other types of uniform proofs between these two, but it is not clear what you are asking (seems more like a post to solicit opinion about an idea than a question). You can find related stuff in Jan Krajicek's and other peoples' lecture notes on proof complexity.