We shall consider some recent results on bounded arithmetic and propositional calculus. Using counting principles as an example we shall explain relations between first order theories, propositional calculus and complexity theory. One of the main technical results tha we shall apply is a lower bound on the degrees of polynomials in Hilbert's Nullstellensatz, which may be of independent interest.
The counting principle ${\rm Count}^n_k$, $k\nequiv 0\mod n$, states that an $n$-0element set cannot be partitioned into $k$-element sets. We shall show that in bounded arithmetic ${\rm Count}^n_k$ does not imply ${\rm Count}^n_m$, if $m$ has a prime divisor which is not a divisor of $k$. When stated in propositional calculus, ${\rm Count}^n_m$ does not have polynomial size bounded depth proofs from ${\rm Count}^n_k$ for such $k,m$.