  A famous theorem of Szemer\'edi asserts that given any density $0 < \delta
\leq 1$ and any integer $k \geq 3$, any set of integers with density $\delta$
will contain infinitely many proper arithmetic progressions of length $k$. For
general $k$ there are essentially four known proofs of this fact; Szemer\'edi's
original combinatorial proof using the Szemer\'edi regularity lemma and van der
Waerden's theorem, Furstenberg's proof using ergodic theory, Gowers' proof
using Fourier analysis and the inverse theory of additive combinatorics, and
Gowers' more recent proof using a hypergraph regularity lemma. Of these four,
the ergodic theory proof is arguably the shortest, but also the least
elementary, requiring in particular the use of transfinite induction (and thus
the axiom of choice), decomposing a general ergodic system as the weakly mixing
extension of a transfinite tower of compact extensions. Here we present a
quantitative, self-contained version of this ergodic theory proof, and which is
``elementary'' in the sense that it does not require the axiom of choice, the
use of infinite sets or measures, or the use of the Fourier transform or
inverse theorems from additive combinatorics. It also gives explicit (but
extremely poor) quantitative bounds.
