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.
Keywords: existential completion, doctrine, Herbrand's theorem
2020 MSC: 18C10 (Primary), 03G30, 08B20 (Secondary)
Theory and Applications of Categories, Vol. 45, 2026, No. 23, pp 924-950.
Published 2026-04-28.
TAC Home