This paper surveys the development of propositional proof complexity and the seminal contributions of Alasdair Urquhart. We focus on the central role of counting principles, and in particular Tseitin's graph tautologies, to most of the key advances in lower bounds in proof complexity. We reflect on a couple of key ideas that Urquhart pioneered: (i) graph expansion as a tool for distinguishing between easy and hard principles, and (ii) ``reductive" lower bound arguments, proving via a simulation theorem that an optimal proof cannot bypass the obvious (inefficient) one.