2025/12/23 by Mariana V. Badano, Badano, Mariana
Mathematics · Computer Science · #History and Theory of Mathematics #Mathematical and Theoretical Analysis #Logic, programming, and type systems
paper · doi:10.48550/arxiv.2512.20496
Herbrand's Theorem is a fundamental result in mathematical logic which provides a reduction of first-order formulas satisfied by a universal class to formulas free of existential quantifiers. In this work, a simpler and self-contained formulation of Herbrand's Theorem is presented, along with a model-theoretic proof of its general version.