Circuits and formulas for Clique


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?