Kurt Gödel (1906–1978), a major figure in the history of logic, is best known for his celebrated incompleteness theorem presented in "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" (Monatshefte für Mathematik und Physik 38 [1931]: 173–198) and his associated proof of the impossibility of establishing the consistency of customary formulations of arithmetic by methods formalizable within the systems themselves. In addition to these results (discussed in the entry Gödel's Theorem), Gödel made important contributions to several other branches of logic, and prior to his 1931 paper he had already presented the first completeness proof for the first-order functional calculus (in "Die Völlstandigkeit der Axiome des logischen Funktionkalküls," Monatshefte für Mathematik und Physik 37[1930]: 349–360). Making use of a normal form devised by Thoralf Skolem, Gödel elaborated a proof along lines that were followed by Jacques Herbrand...