“An algebraic proof of Herbrand’s theorem”
Giovedì 24 Settembre 2026, ore 15:45 - Sala Riunioni 7B2 - Joshua Wrigley (Université Paris Cité)
Abstract
Herbrand’s theorem asserts that a universal theory, i.e. one whose axioms avoid any use of existential quantification, can only admit constructive proofs of existential statements; that is, to prove an existential statement in a universal theory, we must construct a (finite) set of terms that are the possible witnesses for the statement.
While traditionally a result in the domain of proof theory, Abbadini and Guffanti recently realised that an algebraic proof of Herbrand’s theorem can be provided using quantifier completions of Lawvere doctrines. In this talk, we simplify the argument of Abbadini and Guffanti, and show that a proof of Herbrand’s theorem for Horn logic was implicit in Trotta’s existential completion.
