  This paper explores the connection between two central results in the proof
theory of classical logic: Gentzen's cut-elimination for the sequent calculus
and Herbrands "fundamental theorem". Starting from Miller's
expansion-tree-proofs, a highly structured way presentation of Herbrand's
theorem, we define a calculus of weakening-free proof nets for (prenex)
first-order classical logic, and give a weakly-normalizing cut-elimination
procedure. It is not possible to formulate the usual counterexamples to
confluence of cut-elimination in this calculus, but it is nonetheless
nonconfluent, lending credence to the view that classical logic is inherently
nonconfluent.
