(logic) The conversion of a formula of first-order logic which involves the following steps: (1) replace free variables with constants, (2) replace any variable bound by a universal quantifier which lies in the scope of an even number of logical negations with a Herbrand function, and (3) replace any variable bound by an existential quantifier which lies in the scope of an odd number of negations with a Herbrand function.

A surname from German.

plural of Herbrand

(logic) The set of all ground terms that may be formed (even recursively) using any of the constants and functions which appear in a given set of formulae. (If there is no constant in that given set of formulae, then designate one default constant as being usable for the aforementioned purpose.)

(logic) A function which replaces a variable bound by a universal quantifier which lies in the scope of an even number of logical negations; such function is a function of the remaining bound variables whose scope contain the given variable (being replaced).

plural of Herbrand universe

plural of Herbrand function

(logic) A fundamental result of mathematical logic, essentially allowing a certain kind of reduction of first-order logic to propositional logic.

(mathematics) A result on the class group of certain number fields, strengthening Ernst Kummer's theorem to the effect that the prime p divides the class number of the cyclotomic field of p-th roots of unity iff p divides the numerator of the n-th Bernoulli number Bₙ for some n, 0 < n < p − 1. The Herbrand–Ribet theorem specifies what, in particular, it means when p divides such an Bₙ.