Existential completions and Herbrand's theorem

TL;DR

This paper presents a new algebraic approach to Herbrand's theorem by constructing free existential completions on presheaves of distributive lattices, simplifying previous proofs and extending to other structures.

Contribution

It introduces a direct method for constructing existential completions on presheaves, providing a new proof of Herbrand's theorem for coherent logic and related structures.

Findings

Constructed the free existential completion on presheaves of distributive lattices.

Derived Herbrand's theorem for coherent logic from the explicit construction.

Extended the approach to presheaves of meet-semilattices and frames.

Abstract

Recently, Abbadini and Guffanti gave an algebraic proof of Herbrand's theorem using a completion for Lawvere doctrines that freely adds existential and universal quantifiers. A more direct argument can be given by only completing with respect to existential quantifiers. We construct the free existential completion on a presheaf of distributive lattices, and deduce Herbrand's theorem for coherent logic from the explicit description. We also discuss the cases involving presheaves of meet-semilattices, due to Trotta, and presheaves of frames.