arXiv · 2508.15518
Existential completions and Herbrand's theorem
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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Joshua L. Wrigley. 2025-08-21. Existential completions and Herbrand's theorem. https://arxiv.org/abs/2508.15518
Cite the original work for its findings. Save a collection to share your selection of sources.