In this mini course I will survey some of the basics of bounded arithmetic, as well as its connections to proof and computational complexity. I will focus mainly on the case of polynomial time, starting with Cobham's famous characterisation of polynomial time, thence it's extensions to a quantifier free theory (Cook's PV) and a fragment of arithmetic (Buss' $S^1_2$). I will explain the connection to the Extended Frege system for propositional logic, yielding a uniform-nonuniform correspondence at the level of proof complexity. Finally, I will survey extensions for the polynomial time hierarchy, second order theories, and/or Paris-Wilkie style translations, depending on time available.