In
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
, a Herbrand structure ''S'' is a
structure over a
vocabulary
A vocabulary is a set of familiar words within a person's language. A vocabulary, usually developed with age, serves as a useful and fundamental tool for communication and acquiring knowledge. Acquiring an extensive vocabulary is one of the la ...
σ that is defined solely by the syntactical properties of σ. The idea is to take the symbols of
terms as their values, e.g. the denotation of a constant symbol ''c'' is just "''c''" (the symbol). It is named after
Jacques Herbrand
Jacques Herbrand (12 February 1908 – 27 July 1931) was a French mathematician. Although he died at age 23, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse and Richard Coura ...
.
Herbrand structures play an important role in the foundations of
logic programming
Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic pro ...
.
Herbrand universe
Definition
The ''Herbrand universe'' serves as the universe in the ''Herbrand structure''.
Example
Let , be a first-order language with the vocabulary
* constant symbols: ''c''
* function symbols: ''f''(·), ''g''(·)
then the Herbrand universe of (or ) is .
Notice that the
relation symbols are not relevant for a Herbrand universe.
Herbrand structure
A ''Herbrand structure'' interprets terms on top of a ''Herbrand universe''.
Definition
Let ''S'' be a
structure, with vocabulary σ and universe ''U''. Let ''W'' be the set of all terms over σ and ''W''
0 be the subset of all variable-free terms. ''S'' is said to be a ''Herbrand structure'' iff
#
# for every ''n''-ary function symbol and
# ''c'' = ''c'' for every constant ''c'' in σ
Remarks
# is the Herbrand universe of .
# A Herbrand structure that is a model of a theory ''T'', is called the ''Herbrand model'' of ''T''.
Examples
For a constant symbol ''c'' and a unary function symbol ''f''(.) we have the following interpretation:
*
*
* ''c'' → ''c''
Herbrand base
In addition to the universe, defined in ''Herbrand universe'', and the term denotations, defined in ''Herbrand structure'', the ''Herbrand base'' completes the interpretation by denoting the relation symbols.
Definition
A ''Herbrand base'' is the set of all ground atoms of whose argument terms are the Herbrand universe.
Examples
For a binary relation symbol ''R'', we get with the terms from above:
:
See also
*
Herbrand's theorem
Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). It essentially allows a certain kind of reduction of first-order logic to propositional logic. Although Herbrand originally proved his theorem for ...
*
Herbrandization {{Short description, Proof of Herbrand's theorem
The Herbrandization of a logical formula (named after Jacques Herbrand) is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formul ...
*
Herbrand interpretation
In mathematical logic, a Herbrand interpretation is an interpretation in which all constants and function symbols are assigned very simple meanings. Specifically, every constant is interpreted as itself, and every function symbol is interpreted a ...
Notes
References
* {{cite book
, last1=Ebbinghaus
, first1=Heinz-Dieter
, authorlink1=Heinz-Dieter Ebbinghaus
, last2=Flum
, first2=Jörg
, last3=Thomas
, first3=Wolfgang
, title=Mathematical Logic
, publisher=
Springer
Springer or springers may refer to:
Publishers
* Springer Science+Business Media, aka Springer International Publishing, a worldwide publishing group founded in 1842 in Germany formerly known as Springer-Verlag.
** Springer Nature, a multinationa ...
, isbn=978-0387942582
, year=1996
, url-access=registration
, url=https://archive.org/details/mathematicallogi1996ebbi
Mathematical logic