Dott. Marco Abbadini (University of Birmingham) will give a seminar on Thursday 24 April 2025 at 10:00 in Sala Riunioni, DipMat.
Title: An algebraic version of Herbrand’s theorem.
Abstract: Herbrand’s theorem is a fundamental result of mathematical logic, which allows a reduction of first-order logic to propositional logic.
In its simplest form, it asserts that an existential statement “exists x P(x)” with P(x) quantifier-free is provable if and only if there are finitely many terms c_1,…, c_n such that “P(c_1) or … or P(c_n)” is provable.
We provide an algebraic version of Herbrand’s theorem. By “algebraic” we mean “in the setting of first-order Boolean doctrines”, a notion that originates in Lawvere’s work and can be seen as the algebraic semantics of classical first-order logic.
Our proof is semantic, i.e. we use models. One thing we find interesting is that our result gives Herbrand’s theorem for the version of classical first-order logic whose semantics is compatible with admitting empty structures; it furthermore shows that Herbrand’s theorem holds for classical many-sorted first-order logic.
0 Comments