Circuits and formulas for Clique

Question

Is it correct to say that the Clique Problem is in $P$ iff there exists a family of Boolean circuits $C$ to decide Clique whose sizes are bounded by a polynomial? And based on this question, does that imply that there exists an equivalent set of Boolean formulas $F$ to decide Clique whose sizes are bounded by a polynomial? And if there is such an $F$, would there be correct derivations based on propositional logic axioms from any member of $F$ to the corresponding large naive formula for Clique?

Answer 1

I'm afraid that the answer to all your questions is false:

• There are languages decided by constant size circuits which aren't decidable.
• It is conjectured that $\mathsf{NC^1} \neq \mathsf{P}$.
• It is conjectured that $\mathsf{NP} \neq \mathsf{coNP}$.