Proof and Descriptive Complexity: Two Sides of the Same Coin

 I will try to convince you that some of the central objects of study of proof complexity and of descriptive complexity are, in a precise technical sense, intimately close. Here are some questions I will try to answer: What do Frege proofs and existential pebble games have to do with anything? What are and what do the LP and SDP hierarchies and their associated proof systems have to do with logics with counting quantifiers? How are such connections useful after all? After the required definitional background, I hope to be able to get down to some definite statements (i.e. theorems) and to discuss some of the ideas of the proofs to clarify the extent to which the connection is tight and fruitful.