Proof Complexity and Circuit Lower bound for coNP

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 ?

• Please do not bundle unrelated questions in one post. Also I would suggest having a look at the tips about writing better questions in the FAQ, particularly this one. – Kaveh May 18 '12 at 14:09

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}$.
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).