Herbrand's Fundamental Theorem: The Historical Facts and their Streamlining

TL;DR

This paper revisits Herbrand's Fundamental Theorem, clarifying its historical development, analyzing its core structure, and demonstrating the proof correction using Heijenoort's generalized rules, with a focus on its significance in predicate logic.

Contribution

It provides a detailed analysis of Herbrand's theorem, incorporating Heijenoort's correction, and offers a didactic example to clarify the proof's inner structure and historical context.

Findings

Heijenoort's generalized rules improve the proof of Herbrand's Theorem.

The correction addresses Herbrand's 'False Lemma' effectively.

Herbrand's theorem is central to predicate logic, with a concise and elegant formulation.

Abstract

Using Heijenoort's unpublished generalized rules of quantification, we discuss the proof of Herbrand's Fundamental Theorem in the form of Heijenoort's correction of Herbrand's "False Lemma" and present a didactic example. Although we are mainly concerned with the inner structure of Herbrand's Fundamental Theorem and the questions of its quality and its depth, we also discuss the outer questions of its historical context and why Bernays called it "the central theorem of predicate logic" and considered the form of its expression to be "concise and felicitous".