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 ?