Herbrand's Theorem: a short statement and a model-theoretic proof

TL;DR

This paper presents a simplified, self-contained formulation of Herbrand's Theorem along with a model-theoretic proof, enhancing understanding of its role in logical reductions.

Contribution

It introduces a clearer, more accessible statement of Herbrand's Theorem and provides a novel model-theoretic proof of its general form.

Findings

Simplified formulation of Herbrand's Theorem

Model-theoretic proof of the theorem's general version

Enhanced understanding of logical reductions in first-order logic

Abstract

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.