Jacques Herbrand's thesis "Investigations in proof theory: The properties of true propositions" (or in the original French "Recherches sur la théorie de la démonstration", with the English translation in van Heijenoort's "From Frege to Gödel"), contains Herbrand's Theorem which has had a significant impact in automated theorem proving and the $\varepsilon$-calculus.
Before his untimely death, he submitted "On the consistency of arithmetic" (or in the original French "Sur la non-contradiction de l'arithmétique", also found in "From Frege to Gödel") which is said to prove the consistency of arithmetic by elimination of the induction schema:
Dated "Gottingen, 14 July 1931", this paper was sent by Herbrand for publication (to the Journal fur die reine undangewandte Mathematik) just before he left for a vacation trip in the Alps. The paper was received on 27 July and on that day Herbrand was killed in a fall. [...] Consistency is proved for an arithmetic in which the well-formed formula that can be substituted in the induction schema does not contain any bound variable (or, if it does, does not contain any function but the successor function). Consistency proofs likewise requiring some restriction on the induction axiom schema had been presented by Ackermann (1924) and von Neumann (1927). Herbrand's proof remains relatively simple and straightforward because he has at his disposal his powerful fundamental theorem (1930).
The proofs of Ackermann & von Neumann were discussed in Von Neumann's consistency proof, but not Herbrand's, leading me to my first question:
Question 1: What were the main ideas and differences of Herbrand's work in this paper?
Gentzen-style methods seem to dominate Proof Theory. Therefore, I am also interested in the legacy of Herbrand's consistency proof. The only work I could find developing Herbrand's consistency was in 1970 from Burton Dreben & John Denton's "Herbrand-Style Consistency Proofs" which extends Herbrand's ideas. This brings me to my second question:
Question 2: What were the contributions (if there are any) of Herbrand's proof to Proof Theory? Are there any recent developments on Herbrand's consistency proof?
Outside of Proof Theory, it has been stated in Wilfred Sieg's "Only Two Letters" that Herbrand's ideas played a significant role in the development of general recursive functions and thus Computability theory.
