He introduced recursive functions in about 1932. Herbrand's Theorem was an early result in proof theory. The Herbrand quotient is a type of Euler characteristic, used in homological algebra.