  We establish new, and surprisingly tight, connections between propositional
proof complexity and finite model theory. Specifically, we show that the power
of several propositional proof systems, such as Horn resolution, bounded-width
resolution, and the monomial calculus of bounded degree, can be characterised
in a precise sense by variants of fixed-point logics that are of fundamental
importance in descriptive complexity theory. Our main results are that Horn
resolution has the same expressive power as least fixed-point logic, that
bounded-width resolution captures existential least fixed-point logic, and that
the polynomial calculus with bounded degree over the rationals solves precisely
the problems definable in fixed-point logic with counting. We also study the
bounded-degree polynomial calculus. Over the rationals, it captures fixed-point
logic with counting if we restrict the bit-complexity of the coefficients. For
unrestricted coefficients, we can only say that the bounded-degree polynomial
calculus is at most as powerful as bounded variable infinitary counting logic,
but a precise logical characterisation of its power remains an open problem.
These connections between logics and proof systems allow us to establish
finite-model-theoretic tools for proving lower bounds for the polynomial
calculus over the rationals and also over finite fields.
  This is a corrected version of the paper (arXiv:1802.09377) published
originally on January 23, 2019.
