On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem